Формальная спецификация

В информатике — это математически обоснованные методы , формальные спецификации целью которых является помощь в реализации систем и программного обеспечения. Они используются для описания системы, анализа ее поведения и помощи в ее проектировании путем проверки ключевых свойств, представляющих интерес, с помощью строгих и эффективных инструментов рассуждения. ^[1]^[2] Эти спецификации формальны в том смысле, что у них есть синтаксис, их семантика находится в пределах одной области, и их можно использовать для вывода полезной информации. ^[3]

Мотивация [ править ]

С каждым десятилетием компьютерные системы становятся все более мощными и, как следствие, оказывают все большее влияние на общество. По этой причине необходимы более совершенные методы, помогающие в разработке и внедрении надежного программного обеспечения. Признанные инженерные дисциплины используют математический анализ в качестве основы для создания и проверки конструкции продукта. Формальные спецификации являются одним из таких способов достижения надежности разработки программного обеспечения, как когда-то предсказывалось. Другие методы, такие как тестирование, чаще используются для повышения качества кода. ^[1]

Использует [ править ]

Учитывая такую спецификацию , можно использовать формальные методы проверки, чтобы продемонстрировать, что проект системы верен с точки зрения его спецификации. Это позволяет пересмотреть неправильные конструкции системы до того, как будут сделаны какие-либо крупные инвестиции в фактическую реализацию. Другой подход заключается в использовании вероятно правильных шагов уточнения для преобразования спецификации в проект, который в конечном итоге преобразуется в правильную по конструкции реализацию .

Важно отметить, что формальная спецификация не является реализацией, а скорее может использоваться для разработки реализации . Формальные спецификации описывают, что должна делать система, а не то, как она должна это делать.

Хорошая спецификация должна обладать некоторыми из следующих атрибутов: адекватная, внутренне непротиворечивая, недвусмысленная, полная, удовлетворительная, минимальная. ^[3]

Хорошая спецификация будет иметь: ^[3]

Конструктивность, управляемость и эволюционируемость
Удобство использования
Коммуникабельность
Мощный и эффективный анализ

Одна из основных причин интереса к формальным спецификациям заключается в том, что они обеспечивают возможность проверки реализаций программного обеспечения. ^[2] Эти доказательства могут использоваться для подтверждения спецификации, проверки правильности проекта или для доказательства того, что программа удовлетворяет спецификации. ^[2]

Ограничения [ править ]

Проект (или реализация) никогда не может быть объявлен «правильным» сам по себе. Оно может быть только «правильным по отношению к заданной спецификации». Правильно ли формальная спецификация описывает решаемую задачу – это отдельный вопрос. Это также трудный вопрос для решения, поскольку в конечном итоге он касается проблемы построения абстрактных формальных представлений неформальной конкретной проблемной области , и такой шаг абстракции не поддается формальному доказательству. Однако можно подтвердить достоверность спецификации, доказав «проблемные» теоремы , касающиеся свойств, которые, как ожидается, будет демонстрировать спецификация. Если они верны, эти теоремы укрепляют понимание спецификатором спецификации и ее связи с базовой проблемной областью. Если нет, то спецификацию, вероятно, необходимо изменить, чтобы лучше отражать понимание предметной области теми, кто участвует в разработке (и реализации) спецификации.

Формальные методы разработки программного обеспечения не получили широкого распространения в промышленности. Большинство компаний не считают экономически эффективным применять их в процессах разработки программного обеспечения. ^[4] Это может быть по разным причинам, вот некоторые из них:

Время
- Высокие первоначальные затраты при низкой измеримой прибыли.
Гибкость
- Многие компании-разработчики программного обеспечения используют гибкие методологии , ориентированные на гибкость. Предварительная формальная спецификация всей системы часто воспринимается как нечто противоположное гибкости. Тем не менее, есть некоторые исследования преимуществ использования формальных спецификаций при «гибкой» разработке. ^[5]
Сложность
- Они требуют высокого уровня математических знаний и аналитических навыков, чтобы понимать и эффективно их применять. ^[5]
- Решением этой проблемы могла бы стать разработка инструментов и моделей, которые позволяют реализовать эти методы, но скрывают лежащую в их основе математику. ^[2]^[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]

алгебраический
На основе модели
1. С
2. Б
3. ВДМ
4. CSP
5. Сети Петри
6. ТЛА+

См. также [ править ]

Ссылки [ править ]

^ Перейти обратно: ^а ^б Хиеронс, Р.М.; Богданов К.; Боуэн, Япония ; Кливленд, Р.; Деррик, Дж.; Дик, Дж.; Георге, М.; Харман, М .; Капур, К.; Краузе, П.; Люттген, Г.; Саймонс, AJH; Вилкомир, SA ; Вудворд, MR; Зедан, Х. (2009). «Использование формальных спецификаций для поддержки тестирования». Обзоры вычислительной техники ACM . 41 (2): 1. CiteSeerX 10.1.1.144.3320 . дои : 10.1145/1459352.1459354 . S2CID 10686134 .
^ Перейти обратно: ^а ^б ^с ^д ^Это Годель, М.-К. (1994). «Методы формальной спецификации». Материалы 16-й Международной конференции по программной инженерии . стр. 223–227. дои : 10.1109/ICSE.1994.296781 . ISBN 978-0-8186-5855-6 . S2CID 60740848 .
^ Перейти обратно: ^а ^б ^с ^д ^Это ^ж ^г ^час ^я ^дж ^к ^л ^м ^н ^О Ламсверде, А.В. (2000). «Формальная спецификация». Материалы конференции о будущем программной инженерии - ICSE '00 . стр. 147–159. дои : 10.1145/336512.336546 . ISBN 978-1581132533 . S2CID 4657483 .
^ Перейти обратно: ^а ^б ^с ^д Соммервилл, Ян (2009). «Формальная спецификация» (PDF) . Программная инженерия . Проверено 3 февраля 2013 г.
^ Перейти обратно: ^а ^б ^с Нумменмаа, Тимо; Тиенсуу, Алекси; Берки, Элени; Микконен, Томми; Куиттинен, Юсси; Култима, Аннакаиса (4 августа 2011 г.). «Поддержка гибкой разработки путем облегчения естественного взаимодействия пользователей с исполняемыми формальными спецификациями». Заметки по разработке программного обеспечения ACM SIGSOFT . 36 (4): 1–10. дои : 10.1145/1988997.2003643 . S2CID 2139235 .
^ Перейти обратно: ^а ^б ван дер Полл, Джон А.; Паула Коце (2002). «Какие эвристики проектирования могут повысить полезность формальной спецификации?» . Материалы ежегодной исследовательской конференции Южноафриканского института компьютерных наук и информационных технологов 2002 года по вопросам расширения возможностей посредством технологий . SAICSIT '02: 179–194. ISBN 9781581135961 .
^ Модель знаний S-Cube: формальная спецификация

Внешние ссылки [ править ]

г. Архивировано 21 октября 2005 г. в Wayback Machine компанией Coryoth, 30 июля 2005

[a9-hierons-1] Перейти обратно: ^а ^б Хиеронс, Р.М.; Богданов К.; Боуэн, Япония ; Кливленд, Р.; Деррик, Дж.; Дик, Дж.; Георге, М.; Харман, М .; Капур, К.; Краузе, П.; Люттген, Г.; Саймонс, AJH; Вилкомир, SA ; Вудворд, MR; Зедан, Х. (2009). «Использование формальных спецификаций для поддержки тестирования». Обзоры вычислительной техники ACM . 41 (2): 1. CiteSeerX 10.1.1.144.3320 . дои : 10.1145/1459352.1459354 . S2CID 10686134 .

[p223-gaudel-2] Перейти обратно: ^а ^б ^с ^д ^Это Годель, М.-К. (1994). «Методы формальной спецификации». Материалы 16-й Международной конференции по программной инженерии . стр. 223–227. дои : 10.1109/ICSE.1994.296781 . ISBN 978-0-8186-5855-6 . S2CID 60740848 .

[lamsweerde-roadmap-3] Перейти обратно: ^а ^б ^с ^д ^Это ^ж ^г ^час ^я ^дж ^к ^л ^м ^н ^О Ламсверде, А.В. (2000). «Формальная спецификация». Материалы конференции о будущем программной инженерии - ICSE '00 . стр. 147–159. дои : 10.1145/336512.336546 . ISBN 978-1581132533 . S2CID 4657483 .

[Ch_27_Formal_spec-4] Перейти обратно: ^а ^б ^с ^д Соммервилл, Ян (2009). «Формальная спецификация» (PDF) . Программная инженерия . Проверено 3 февраля 2013 г.

[p14-nummenmaasen-5] Перейти обратно: ^а ^б ^с Нумменмаа, Тимо; Тиенсуу, Алекси; Берки, Элени; Микконен, Томми; Куиттинен, Юсси; Култима, Аннакаиса (4 августа 2011 г.). «Поддержка гибкой разработки путем облегчения естественного взаимодействия пользователей с исполняемыми формальными спецификациями». Заметки по разработке программного обеспечения ACM SIGSOFT . 36 (4): 1–10. дои : 10.1145/1988997.2003643 . S2CID 2139235 .

[p179-vanderpoll-6] Перейти обратно: ^а ^б ван дер Полл, Джон А.; Паула Коце (2002). «Какие эвристики проектирования могут повысить полезность формальной спецификации?» . Материалы ежегодной исследовательской конференции Южноафриканского института компьютерных наук и информационных технологов 2002 года по вопросам расширения возможностей посредством технологий . SAICSIT '02: 179–194. ISBN 9781581135961 .

[7] Модель знаний S-Cube: формальная спецификация

[1]

[2]

[3]

[4]

[5]

[6]

[7]