УДК004.4’242

ПРИМЕНЕНИЕ ШАБЛОНОВ ТРЕБОВАНИЙ К ФОРМАЛЬНОЙ СПЕЦИФИКАЦИИ И ВЕРИФИКАЦИИ АВТОМАТНЫХ ПРОГРАММ

Клебанов А. А., Шалыто А. А.


Читать статью полностью 

Аннотация

Верификация на модели (model checking) является глубоко проработанной технологией проверки корректности программного обеспечения, однако при этом она недостаточно широко используется на практике. Одной из причин является сложность составления формальных требований на языке темпоральных логик. В настоящей работе описывается подход для записи верифицируемых требований на подмножестве естественного языка в контексте автоматного программирования. В частности, приводится анализ применимости шаблонов требований к формальной спецификации автоматных программ, а также описывается грамматика для вывода требований.


Ключевые слова:

автоматное программирование, верификация на модели, темпоральные логики

Информация 2001-2017 ©
Научно-технический вестник информационных технологий, механики и оптики.
Все права защищены.

Яндекс.Метрика