Меню
Публикации
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Главный редактор
НИКИФОРОВ
Владимир Олегович
д.т.н., профессор
Партнеры
УДК 004.4’242
Клебанов А.А., Шалыто А.А.
Читать статью полностью
Аннотация
ПРИМЕНЕНИЕ ШАБЛОНОВ ТРЕБОВАНИЙ К ФОРМАЛЬНОЙ СПЕЦИФИКАЦИИ И ВЕРИФИКАЦИИ АВТОМАТНЫХ ПРОГРАММ
Читать статью полностью
Аннотация
Верификация на модели (model checking) является глубоко проработанной технологией проверки корректности программного обеспечения, однако при этом она недостаточно широко используется на практике. Одной из причин является сложность составления формальных требований на языке темпоральных логик. В настоящей работе описывается подход для записи верифицируемых требований на подмножестве естественного языка в контексте автоматного программирования. В частности, приводится анализ применимости шаблонов требований к формальной спецификации автоматных программ, а также описывается грамматика для вывода требований.
Ключевые слова:
автоматное программирование, верификация на модели, темпоральные логики
