Cтраница 2
В основе этих методов, разработанных научно-исследовательской группой Массачусетского технологического института ( МТИ), лежат две идеи: математическая модель работы ядра и методология анализа корректности, используемая для верификации при реализации модели. Приведены четыре способа описания ядра: в виде математической модели, формальной спецификации, представления в виде алгоритма и описания машинного языка, который использовался для верификации различных форм описания. [16]
Задача может быть решена машиной только в том случае, если она формально поставлена - если для нее написана формальная спецификация. Последняя должна опираться на некоторую базу знаний. Модель предметной области описывает общую обстановку, в которой возникла задача, а спецификация - содержание задачи. В совокупности они позволяют установить, какие абстрактные связи и зависимости, в каких сочетаниях и в какой последовательности должны быть использованы для решения задачи. [17]
Результатом является то, что в написанных такими программистами программах очень часто используются такие машинно-ориентированные знания, что эти программы становятся непонятными для тех, кто такими знаниями не обладает. Поэтому возникает естественное желание сделать вывод: такие программисты не понимают истинных целей создания используемых ими языков программирования, целей, которые заключаются в том, чтобы сделать возможной точную формальную спецификацию абстрактных машин. [18]
Первый из языков основан на объединении автоматной модели с языком программирования Pascal и добавлении элементов описания архитектурных особенностей протокольных систем. Второй язык основан на математической модели исчисления взаимодействующих систем и абстрактных типах данных. В настоящее время имеется первый опыт получения формальных спецификаций сетевого, транспортного и сеансового уровней на этих языках, причем язык ESTELLE оказался наиболее удобным для описания протокольных стандартов, а язык LOTOS - стандартов сервиса -, предоставляемого протоколами. [19]
Наконец, доказательство ее корректности будет дано в разд. Для установления корректности реализации требуется по меньшей мере формальное доказательство того, что семантика ее модели вычислений эквивалентна семантике языка. В общем случае необходимо также доказать, что формальная спецификация реализации соответствует семантике модели, но это относительно простая задача, если интерпретатор написан на функциональном языке, который сам может отражать семантику модели Следовательно, это доказательство рассматриваться не будет) Доказательство корректности, согласно Плоткину [72], влечет за собой обеспечение формальной семантики работы SECD-машины и затем показывает ее эквивалентность семантике ( 3-редукции Оно дано для энергичной машины, но модификации, требуемые для ленивой версии, достаточно просты. [20]
Предполагается дальнейшее развитие протокольного отладчика. В частности, анализ трассы может быть автоматизирован. Для этого на вход протокольного отладчика будет поступать тестовая последовательность, подготовленная вручную или автоматически из формальной спецификации, а отладчик при обнаружении расхождений тестовой и трассовой последовательностей будет выдавать необходимую разработчику информацию. [21]
Несмотря на значительные результаты, достигнутые группой МФО ИСО, ведутся многочисленные работы по созданию инструментальных комплексов ( ИК) для реализации протоколов, которые, как правило, содержат собственные МФО. Для таких МФО принцип общности играет значительно меньшую роль, а на первое место выдвигаются требования эффективности и адаптации к конкретному окружению. Инструментальные комплексы позволяют описывать стандарты в конкретных условиях и / или создавать специализированные протоколы с последующей трансляцией полученных формальных спецификаций в реализации. Одним из них является комплекс Архитектор, разработанный для реализации протокольных систем на многопроцессорном вычислительном комплексе Эльбрус и использующий язык формального описания ОСА. [22]
Аналитический подход в первую очередь затрагивает тестирование и обоснование программ после того, как они написаны, чтобы повысить их надежность. Он включает традиционные методы отладки программ, средства доказательства правильности программ, различные средства автоматического тестирования. Конструктивный подход использует набор надежных программных средств для разработки надежного ПО, которые принято называть структурным программированием. Этот подход включает построение средств, использующих просмотр сверху вниз и формальные спецификации, и средства кодирования с применением простых управляющих структур. [23]
Модель КОДАСИЛ постоянно развивается, совершенствуются средства формальной спецификации элементов модели, исследуются различные аспекты возможной стандартизации. Эта модель считается наиболее развитой сетевой моделью данных. [24]
Спецификации программ, разработанных на фазе их проектирования, должны точно описывать характер исходных данных и то, что должно быть получено в результате выполнения программы. Отдельные части спецификации могут отражать время выполнения, сложность вычисления, размер массивов, возможные инварианты, контролирующие ход вычислительного процесса. Один из способов спецификации заключается в описании на естественном языке того, что должно быть получено по заданным исходным данным. Однако в этом случае трудно избежать двусмысленностей при разборе их разными специалистами. Естественно, что многие ученые предлагают различные методы формальных спецификаций. [25]
Первые три этапа будем называть проверкой корректности описаний, а последний - верификацией - Под верификацией в традиционном программировании понимается тот факт, что реализация соответствует ее формальной спецификации. Термин верификация может быть применен и в чисто традиционном смысле. Мы не рассматриваем эту сторону верификации, так как она относится к области традиционного программирования, и, кроме того, применение систем автоматической трансляции формальных спецификаций в реализации вообще устраняет необходимость в этом виде анализа. [26]
В самом начале фазы стратегии, если не раньше, должен быть составлен контракт. Многие организации формируют контракт через преобразование цены, предполагающей установку стоимости на товары и услуги для продавца и покупателя, юридически принадлежащих одной организации. Даже для полностью внутренней группы разработки нужно оценить выделяемые ресурсы ( из отдела информационных систем. Дать ответы на эти вопросы до фазы стратегии очень трудно, поскольку нет формальной спецификации на разрабатываемую систему. [27]