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