Verification of declarative LTL-specification of control programs behavior

Verification of declarative LTL-specification of control programs behavior

The article continues the series of works on development and verification of control programs based on LTL-specifications of a special type. Previously, it was proposed a declarative LTL-specification, which allows describing the behavior of control programs and building program code based on it in...

Full description

Bibliographic Details
Main Authors: Maxim V. Neyzov, Egor V. Kuzmin
Format: Article
Language:English
Published: Yaroslavl State University 2024-06-01
Series:Моделирование и анализ информационных систем
Subjects:
control software
plc program
declarative ltl-specification
imperative ltl-specification
complete transition system
pseudo-complete transition system
state space
model checking
nuxmv verifier
smv-specification
bisimulation equivalence
bisimulation
Online Access:https://www.mais-journal.ru/jour/article/view/1849

Internet

https://www.mais-journal.ru/jour/article/view/1849

Similar Items