Помимо собственно фиксации программного контракта, формальная спецификация позволяет систематизировать функциональное тестирование (часто называемое тестированием по методу «черного ящика»). Поскольку формальные спецификации строго описывают требования как на входные данные, так и на ожидаемые результаты, функциональных спецификаций достаточно для того, чтобы провести тестирование внешнего поведения системы. Без строгих спецификаций такой систематизированный подход невозможен, поскольку нет данных ни об области допустимых воздействий на целевую систему, ни о критериях оценки полученных результатов – какие из результатов следует трактовать как правильные, какие как ложные. Это является одной из причин того, что большая часть исследований по тестированию посвящена тестированию на основе исходных текстов. Исходные тексты являются строгим описанием структуры реализации, поэтому они представляются подходящим материалом для извлечения тестов (тестовых воздействий) и для оценки полноты тестового покрытия. Однако, в отличие от функциональных спецификаций, на основании изучения исходных текстов нельзя вынести заключения о критериях проверки соответствия реализации ее функциональным требованиям, в частности, о полноте реализации. Еще одно обстоятельство является чрезвычайно важным. Если спецификации формальны, то они могут рассматриваться как «машинно-читаемые». Тем самым появляется предпосылка полностью автоматизировать как генерацию тестов, так и анализ результатов тестирования.
Серьезным направлением в использовании формальных методов в последние десять лет стала «проверка моделей» (model checking). Этот подход демонстрирует компромисс между идеальной мечтой о верификации формальной системы и реальной практикой разработки ПО. Суть похода состоит в построении модели реальной системы и по возможности полной проверке корректности данной модели. Проверка, если возможно, проводится аналитическими методами. Если это невозможно, производится тестирование модели. При этом сложность модели, как правило, выбирается таким образом, чтобы была возможность провести «исчерпывающее» тестирование (exhaustive testing). Слабое место данного подхода – это проблемы построения модели и доказательство того, что модель достаточно содержательна, чтобы на основании модели можно было судить о свойствах реальной системы.
Резюмируя данный краткий обзор позитивных сдвигов в использовании формальных методов в индустриальной разработке ПО, отметим, что сейчас наметилось достаточно четкое разделение методологий и поддерживающих их инструментов, ориентированных на академические исследования и на использование в промышленности ПО. Последние отличаются от первых не только более развитыми средствами поддержки программных проектов, но и средствами, позволяющими перекинуть мостик между спецификациями и собственно целевой системой. К таким средствам в первую очередь относятся компиляторы исполнимых подмножеств языков спецификаций в языки программирования, средства согласования спецификационных и реализационных сущностей, средства, упрощающие конфигурирование целевых и тестовых систем, в которых часть компонентов создается вручную, а часть является результатом генерации из формальных спецификаций. Разнообразие таких возможностей позволяет заключить, что некоторые формальные методологии и наборы их инструментов уже вышли на уровень программных продуктов, и в ближайшее время следует ожидать значительного расширения, как их функциональности, так и масштабов их использования.
Основу применение формальных методов в тестировании программных систем составляет процесс тестирования, верификации супротив функциональных спецификаций, заданных потребителями. Большую сложность составляет процесс извлечения и формализации требований из словесных описаний в стройную систему требований, часто в математическом или ином строгом виде, однозначно описывающую желаемые свойства разрабатываемой системы. Этот процесс по своей сути является построением предварительной модели будущей системы для анализа ее свойств, выявления противоречий в требованиях, уточнения характеристик. В этом аспекте необходимо рассмотреть понятие моделирования.
Однако моделирование как специфическое средство и форма научного познания не является изобретением 19 или 20 века. Достаточно указать на представления Демокрита и Эпикура об атомах, их форме, и способах соединения, об атомных вихрях и ливнях, объяснения физических свойств различных веществ с помощью представления о круглых и гладких или крючковатых частицах, сцепленных между собой. Эти представления являются прообразами современных моделей, отражающих ядерно-электронное строение атома вещества.
20 век принес методу моделирования новые успехи, но одновременно поставил его перед серьезными испытаниями. С одной стороны, кибернетика обнаружила новые возможности и перспективы этого метода в раскрытии общих закономерностей и структурных особенностей систем различной физической природы, принадлежащих к разным уровням организации материи, формам движения. С другой же стороны, теория относительности и в особенности, квантовая механика, указали на неабсолютный, относительный характер механических моделей, на трудности, связанные с моделированием.
Многочисленные факты, свидетельствующие о широком применении метода моделирования в исследованиях, некоторые противоречия, которые при этом возникают, потребовали глубокого теоретического осмысления данного метода познания, поисков его места в теории познания. Этим можно объяснить большое внимание, которое уделяется философами различных стран этому вопросу в многочисленных работах.
Философские аспекты моделирования как метода познания окружающего мира.
Исследование гносеологического значения моделирования должно начинаться с определения понятия "модель".
Слово "модель" произошло от латинского слова "modelium", означает : мера, образ, способ и т.д. Его первоначальное значение было связано со строительным искусством, и почти во всех европейских языках оно употреблялось для обозначения образа или прообраза, или вещи, сходной в каком-то отношении с другой вещью" [1]. По мнению многих авторов ([1],[2],[3]), модель использовалась первоначально как изоморфная теория (после создания Декартом и Ферма аналитической геометрии моделью стало понятие подразумевающее теорию, которая обладает структурным подобием по отношению к другой теории. Две такие теории называются изоморфными, если одна из них выступает как модель другой, и наоборот).
С другой стороны, в таких науках о природе, как астрономия, механика, физика, химия, термин "модель" стал применяться для обозначения того, к чему даннная теория относится или может относиться, того, что она описывает. В.А. Штофф отмечает, что "здесь со словом "модель" связаны два близких, но несколько различных понятия".
Подмоделью в широком смысле понимают мысленно или практически созданную структуру, воспроизводящую часть действительности в упрощенной и наглядной форме. Таковы, в частности представления Анаксимандра о Земле как плоском цилиндре, вокруг которого вращаются наполненные огнем полые трубки с отверстиями. Модель в этом смысле выступает как некоторая идеализация, упрощение действительности, хотя сам характер и степень упрощения, вносимые моделью, могут со временем меняться. В более узком смысле термин "модель" применяют тогда, когда хотят изобразить некоторую область явлений с помощью другой, более хорошо изученной, легче понимаемой. Так, физики 18 века пытались изобразить оптические и электрические явления посредством механических ("планетарная модель атома" - строение атома изображалось как строение солнечной системы).
Таким образом, в этих двух случаях под моделью понимается либо конкретный образ изучаемого объекта, в котором отображаются реальные или предполагаемые свойства, строение и т.д., либо другой объект, реально существующий наряду с изучаемым и сходный с ним в отношении некоторых определенных свойств или структурных особенностей. В этом смысле модель - не теория, а то, что описывается данной теорией - своеобразный предмет данной теории.
Во многих дискуссиях, посвященных гносеологической роли и методологическому значению моделирования, термин "моделирование" употреблялся как синоним познания,теории, гипотезы и т.п. Например, часто модель употребляется как синоним теории в случае, когда теория еще недостаточно разработана, в ней мало дедуктивных шагов, много упрощений, неясностей (физика: термин "модель" может здесь потребляться для обозначения предварительного наброска или варианта будущей теории при условии значительных упрощений, вводимых с целью обеспечения поиска путей, ведущих к построению более точной и совершенной теории.
Иногда этот термин употребляют в качестве синонима любой количественной теории, математического описания. Несостоятельность такого употребления с гносеологической точки зрения, по мнению В.А.IIIтоффа, в том, "что такое словоупотребление не вызывает никаких новых гносеологических проблем, которые были бы специфичны для моделей".
Существенным признаком, отличающим модель от теории (по словам И.Т. Фролова) [4] является не уровень упрощения, не степень абстракции, и следовательно, не количество этих достигнутых абстракций и отвлечений, а способ выражения этих абстракций, упрощений и отвлечений, характерный для модели.
В философской литературе, посвященной вопросам моделирования, предлагаются различные определения модели. А.А. Зиновьев и И.И. Pевзин дают следующее определение: "Пусть X есть некоторое множество суждений, описывающих соотношение элементов некоторых сложных объектов А и В. Пусть Y есть некоторое множество суждений, получаемых путем изучения А и отличных от суждения Х. Пусть есть некоторое множество суждений, относящихся к В и также отличных от Х. Если выводится из конъюнкции Х и Y по правилам логики, то А есть модель В, а В есть оригинал модели."[5] Здесь модель - лишь средство получения знаний, а не сами знания, не гносеологический образ, следовательно, из рассмотрения выпадают идеальные модели (мысленные), т.к. их значение в качестве элементов знания реальных объектов отрицать нельзя. Определение И.Т. Фролова: "Моделирование означает материальное или мысленное имитирование реально существующей системы путем специального конструирования аналогов (моделей), в которых воспроизводятся принципы организации и функционирования этой системы".[4] Здесь в основе мысль, что модель - средство познания, главный ее признак - отображение.