Форум Сообщества Аналитиков
Общий раздел => Для всех => Тема начата: Tim от 19 Января 2015, 17:20:54
-
Кто-нибудь пробовал писать формальные спецификации (http://en.wikipedia.org/wiki/Formal_specification) на языках типа Z (http://en.wikipedia.org/wiki/Z_notation), EventB (http://en.wikipedia.org/wiki/B-Method), Alloy (http://en.wikipedia.org/wiki/Alloy_%28specification_language%29) и т.п.? Мне кажется, что в последнее время наблюдается рост интереса индустрии к этой теме, особенно в областях связанных с security и safety, например:
- seL4 (http://sel4.systems) - ядро операционой системы, реализация которого формально верифицирована на соответствие спецификации с помощью Isabelle (http://en.wikipedia.org/wiki/Isabelle_%28proof_assistant%29);
- проекты (http://alloy.mit.edu/alloy/citations/case-studies.html), использующие Alloy;
- проекты (http://wiki.event-b.org/index.php/Industrial_Projects), использующие EventB.
Меня в первую очередь заинтересовало то, что автоматизированными средствами можно проверять непротиворечивость и корректность спецификаций, выявляя ошибки на ранних стадиях жизнного цикла и снижая трудозатраты на поддержание в актуальном состоянии меняющихся системных и компонентных требований. А что думаете вы по поводу формальной спецификации?
-
сообщение устарело