Разработка и автоматическая верификация параллельных автоматных программ
Ключевые слова:
автоматы, параллельные автоматные программы, верификация, проверка моделей, линейная темпоральная логика, SpinАннотация
Рассмотрен комплексный подход к разработке и верификации параллельных автоматных программ, в которых иерархические автоматы могут реализовываться в разных потоках и взаимодействовать друг с другом. Предложен интерактивный подход к верификации параллельных автоматных программ при помощи инструментального средства Spin, который включает в себя автоматическое построение модели на языке Promela, приведение LTL-формулы в формат, определяемый инструментальным средством Spin, и построение контрпримера в терминах автоматов.
Опубликован
18-10-2013
Как цитировать
Лукин, М. А., & Шалыто, А. А. (2013). Разработка и автоматическая верификация параллельных автоматных программ. Информационно-управляющие системы, (5), 3–50. извлечено от https://i-us.ru/index.php/ius/article/view/13674
Выпуск
Раздел
Программные и аппаратные средства
