Темпоральные логики для спецификации свойств программных и аппаратных систем
Keywords:
Линейная темпоральная логика, LTL, реагирующие системы (reactive systems), спецификация поведения
Abstract
В статье вводится темпоральная логика линейного времени (LTL), ее формулы объясняются на многочисленных примерах. Объясняется, как свойства поведения дискретных динамических систем, в частности, реагирующих систем (reactive systems) могут быть заданы в этой логике. Статья является изложением одной из глав книги автора «Model checking. Верификация параллельных и распределенных программных систем», которая выходит в издательтве БХВ Петербург.
Published
2014-01-21
How to Cite
Карпов, Ю. (2014). Темпоральные логики для спецификации свойств программных и аппаратных систем. Computer Tools in Education, (2). Retrieved from http://cte.eltech.ru/ojs/index.php/kio/article/view/1174
Issue
Section
Articles
This work is licensed under a Creative Commons Attribution 4.0 International License.
