Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

В информатике , формальные спецификации математически на основе методики , цель которых должны помочь с внедрением систем и программного обеспечения. Они используются для описания системы, анализа ее поведения и помощи в ее проектировании путем проверки ключевых свойств, представляющих интерес, с помощью строгих и эффективных инструментов рассуждения. [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. OBJ
    3. Лотос
  • На основе модели
    1. Z
    2. B
    3. VDM
    4. CSP
    5. Сети Петри
    6. TLA +

Примеры [ править ]

Примеры реализации см. По ссылкам в разделе программных инструментов .

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

  • Алгебраическая спецификация
  • Формальные методы
  • Спецификация на основе модели
  • Программная инженерия
  • Язык спецификации
  • Спецификация (технический стандарт)

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

  1. ^ 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 .
  2. ^ a b c d e Годель, М.-К. (1994). «Методы формальной спецификации». Материалы 16-й Международной конференции по программной инженерии . С. 223–227. DOI : 10.1109 / ICSE.1994.296781 . ISBN 978-0-8186-5855-6.
  3. ^ 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.
  4. ^ a b c d Соммервилл, Ян (2009). «Формальная спецификация» (PDF) . Программная инженерия . Проверено 3 февраля 2013 года .
  5. ^ a b c Nummenmaa, Тимо; Тиэнсуу, Алекси; Берки, Элени; Микконен, Томми; Куиттинен, Юсси; Культима, Аннакайса (4 августа 2011 г.). «Поддержка гибкой разработки за счет облегчения естественного взаимодействия пользователя с исполняемыми формальными спецификациями». Примечания по разработке программного обеспечения ACM SIGSOFT . 36 (4): 1–10. DOI : 10.1145 / 1988997.2003643 .
  6. ^ a b van der Poll, John A .; Паула Коце (2002). «Какие эвристики проектирования могут повысить полезность формальной спецификации?» . Труды Ежегодной исследовательской конференции 2002 года Южноафриканского института компьютерных ученых и информационных технологов по обеспечению с помощью технологий . SAICSIT '02: 179–194.
  7. ^ Модель знаний S-Cube: формальная спецификация

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

  • Аргументы в пользу формальной спецификации (технологии) Кориот 2005-07-30
  • Формальная спецификация