В информатике , формальные спецификации математически на основе методики , цель которых должны помочь с внедрением систем и программного обеспечения. Они используются для описания системы, анализа ее поведения и помощи в ее проектировании путем проверки ключевых свойств, представляющих интерес, с помощью строгих и эффективных инструментов рассуждения. [1] [2] Эти спецификации являются формальными в том смысле, что они имеют синтаксис, их семантика укладывается в один домен и их можно использовать для вывода полезной информации. [3]
Мотивация [ править ]
С каждым прошедшим десятилетием компьютерные системы становились все более мощными и, как следствие, оказывали большее влияние на общество. Из-за этого необходимы более совершенные методы для помощи в разработке и внедрении надежного программного обеспечения. Установленные инженерные дисциплины используют математический анализ в качестве основы для создания и проверки дизайна продукта. Формальные спецификации - это один из способов добиться этого с точки зрения надежности программного обеспечения, как это было предсказано ранее. Другие методы, такие как тестирование , чаще используются для повышения качества кода. [1]
Использует [ редактировать ]
Имея такую спецификацию , можно использовать формальные методы проверки , чтобы продемонстрировать правильность проекта системы по отношению к ее спецификации. Это позволяет пересмотреть неправильные конструкции системы до того, как будут сделаны какие-либо крупные инвестиции в фактическую реализацию. Другой подход заключается в использовании, вероятно, правильных шагов уточнения для преобразования спецификации в проект, который в конечном итоге преобразуется в реализацию, правильную по конструкции .
Важно отметить, что формальная спецификация не является реализацией, а может использоваться для разработки реализации . Формальные спецификации описывают, что должна делать система, а не то, как она должна это делать.
Хорошая спецификация должна иметь некоторые из следующих атрибутов: адекватная, внутренне непротиворечивая, недвусмысленная, полная, удовлетворяющая, минимальная [3]
Хорошая спецификация будет содержать: [3]
- Конструктивность, управляемость и эволюционируемость
- Удобство использования
- Коммуникабельность
- Мощный и эффективный анализ
Одна из основных причин интереса к формальным спецификациям заключается в том, что они обеспечат возможность проверки программных реализаций. [2] Эти доказательства могут использоваться для проверки спецификации, проверки правильности дизайна или для доказательства того, что программа удовлетворяет спецификации. [2]
Ограничения [ править ]
Дизайн (или реализация) никогда не может быть объявлен «правильным» сам по себе. Он может быть только «правильным по отношению к заданной спецификации». Правильно ли формальная спецификация описывает решаемую проблему - это отдельный вопрос. Это также трудная проблема для решения, поскольку в конечном итоге она касается проблемы построения абстрактных формальных представлений неформальной конкретной предметной области , и такой этап абстракции не поддается формальному доказательству. Тем не менее, можно проверить спецификацию, доказав теоремы о «вызове».относительно свойств, которые, как ожидается, будут продемонстрированы в спецификации. Если они верны, эти теоремы укрепляют понимание спецификацией спецификации и ее взаимосвязи с основной областью проблемы. В противном случае спецификацию, вероятно, необходимо изменить, чтобы лучше отразить понимание предметной области тех, кто участвует в создании (и реализации) спецификации.
Формальные методы разработки программного обеспечения не получили широкого распространения в промышленности. Большинство компаний не считают рентабельным применять их в своих процессах разработки программного обеспечения. [4] Это может быть по разным причинам, в том числе:
- Время
- Высокая начальная стоимость запуска при низкой измеримой прибыли
- Гибкость
- Многие софтверные компании используют гибкие методологии , ориентированные на гибкость. Формальная спецификация всей системы заранее часто воспринимается как противоположность гибкости. Однако есть некоторые исследования преимуществ использования формальных спецификаций при «гибкой» разработке [5]
- Сложность
- Ограниченная сфера применения [3]
- Они не отражают свойства, представляющие интерес для всех участников проекта [3]
- Они плохо справляются с указанием пользовательских интерфейсов и взаимодействия с пользователем [4]
- Не рентабельно
- Это не совсем так, поскольку они ограничили их использование только основными частями критических систем, они показали свою рентабельность [4]
Другие ограничения: [3]
- Изоляция
- Онтологии низкого уровня
- Плохое руководство
- Плохое разделение проблем
- Плохая обратная связь с инструментом
Парадигмы [ править ]
Формальные методы спецификации существовали в различных областях и в различных масштабах в течение довольно долгого времени. [6] Реализации формальных спецификаций будут различаться в зависимости от того, какую систему они пытаются моделировать, как они применяются и на каком этапе жизненного цикла программного обеспечения они были введены. [2] Эти типы моделей можно разделить на следующие парадигмы спецификации:
- Спецификация на основе истории [3]
- поведение на основе системных историй
- утверждения интерпретируются с течением времени
- Спецификация на основе состояний [3]
- поведение на основе состояний системы
- серия последовательных шагов (например, финансовая транзакция)
- такие языки, как Z , VDM или B, полагаются на эту парадигму [3]
- Спецификация на основе переходов [3]
- поведение, основанное на переходах из состояния в состояние системы
- лучше всего использовать с реактивной системой
- такие языки, как диаграммы состояний, PROMELA, STeP-SPL, RSML или SCR, полагаются на эту парадигму [3]
- Функциональная спецификация [3]
- определить систему как структуру математических функций
- OBJ, ASL, PLUSS, LARCH, HOL или PVS полагаются на эту парадигму [3]
- Операционная спецификация [3]
- ранние языки, такие как Пейсли , GIST, сети Петри или алгебры процессов, полагаются на эту парадигму [3]
В дополнение к вышеупомянутым парадигмам существуют способы применения определенных эвристик, которые помогают улучшить создание этих спецификаций. В упомянутой здесь статье лучше всего обсуждается эвристика, используемая при разработке спецификации. [6] Они делают это, применяя подход « разделяй и властвуй» .
Программные инструменты [ править ]
Z обозначение является примером ведущего формального языка спецификаций . Другие включают язык спецификации (VDM-SL) Венского метода разработки и нотацию абстрактных машин (AMN) B-метода . В области веб-сервисов формальная спецификация часто используется для описания нефункциональных свойств [7] ( качество обслуживания веб-сервисов ).
Вот некоторые инструменты: [4]
- Алгебраический
- Лиственница
- OBJ
- Лотос
- На основе модели
- Z
- B
- VDM
- CSP
- Сети Петри
- TLA +
Примеры [ править ]
Примеры реализации см. По ссылкам в разделе программных инструментов .
См. Также [ править ]
- Алгебраическая спецификация
- Формальные методы
- Спецификация на основе модели
- Программная инженерия
- Язык спецификации
- Спецификация (технический стандарт)
Ссылки [ править ]
- ^ a b Hierons, RM; Богданов, К .; Bowen, JP ; Cleaveland, R .; Деррик, Дж .; Дик, Дж .; Георге, М .; Харман, М .; Капур, К .; Krause, P .; Lüttgen, G .; Саймонс, AJH; Вилкомир, С.А .; Вудворд, MR; Зедан, Х. (2009). «Использование формальных спецификаций для поддержки тестирования». ACM Computing Surveys . 41 (2): 1. CiteSeerX 10.1.1.144.3320 . DOI : 10.1145 / 1459352.1459354 .
- ^ a b c d e Годель, М.-К. (1994). «Методы формальной спецификации». Материалы 16-й Международной конференции по программной инженерии . С. 223–227. DOI : 10.1109 / ICSE.1994.296781 . ISBN 978-0-8186-5855-6.
- ^ a b c d e f g h i j k l m n o Ламсверде, А. В. (2000). «Формальная спецификация». Материалы конференции о будущем программной инженерии - ICSE '00 . С. 147–159. DOI : 10.1145 / 336512.336546 . ISBN 978-1581132533.
- ^ a b c d Соммервилл, Ян (2009). «Формальная спецификация» (PDF) . Программная инженерия . Проверено 3 февраля 2013 года .
- ^ a b c Nummenmaa, Тимо; Тиэнсуу, Алекси; Берки, Элени; Микконен, Томми; Куиттинен, Юсси; Культима, Аннакайса (4 августа 2011 г.). «Поддержка гибкой разработки за счет облегчения естественного взаимодействия пользователя с исполняемыми формальными спецификациями». Примечания по разработке программного обеспечения ACM SIGSOFT . 36 (4): 1–10. DOI : 10.1145 / 1988997.2003643 .
- ^ a b van der Poll, John A .; Паула Коце (2002). «Какие эвристики проектирования могут повысить полезность формальной спецификации?» . Труды Ежегодной исследовательской конференции 2002 года Южноафриканского института компьютерных ученых и информационных технологов по обеспечению с помощью технологий . SAICSIT '02: 179–194.
- ^ Модель знаний S-Cube: формальная спецификация
Внешние ссылки [ править ]
- Аргументы в пользу формальной спецификации (технологии) Кориот 2005-07-30
- Формальная спецификация