Сравнение с аналогами

Сравнение с аналогами приведено в табл. 1.2.1.

Таблица 1.2.1. Сравнение с аналогами

В столбцах указаны свойства, поддерживаемые соответствующими методами:

1. Темпоральная логика.

2.

3. Поддержка UML-диаграмм Statechart.

4. Поддержка автоматов Stateflow.

5. Интерактивность.

6. Возможность передавать события между параллельными автоматами.

7. Bounded Model Checking(ограниченная проверка моделей).

8. Поддержка автоматов стандарта IEC 61499.

В строках приведены известные инструментальные средства и методы верификации автоматных программ.

1. Unimod. Verifier (http://is.ifmo.ru/verification/Jaminov.pdf) [21].

2. Automata Verificator (http://is.ifmo.ru/papers/automataverificator) [25].

3. FSM Verifier (http://is.ifmo.ru/download/2008-02-25_politech_verification_kurb.pdf) [27].

4. CTL Verifier (http://is.ifmo.ru/download/2008-02-25_politech_verification.pdf) [33].

5. Latella D., Majzik I., Massink M. Automatic verification of a behavioral subset UML stetechart diagrams using the Spin model-checker (http: //home. mit.bme. hu/~maj zik/publicat/fac99.pdf) [7].

6. Васильева К. А., Кузьмин Е. В. Верификация автоматных программ с

использованием LTL // Моделирование и анализ информационных систем. 2007. № 1, с. 3-14.

(http://is.ifmo .ru/verification/_LTL_for_Spin.pdf) [19].

7. Chen C., Sun J., Liu Y., Dong J., Zheng M. Formal Modeling and Validation of Stateflow Diagrams [40].

(http://link.springer.com/article/10.1007%2Fs 10009-012-0235-0#page-1).

8. Miyazawa A., Cavalcanti A. Refinement-based verification of sequential

implementations of Stateflow charts.

(https: //www.academia.edu/3531758/Refinement- based_verification_of_sequential_implementations_of_Stateflow_charts) [39]

9. Pingree P. J., Mikk E., Holzmann G. J., Smith M. H., Dams D. Validation of mission critical software design and implementation using model checking [spacecraft].

(http://ieeexplore.ieee.org/xpl/abstractAuthors.j sp%3Farnumber%3D 1067982 &rct=j&q=&esrc=s&sa=U&ei=OJ8hVPj_D8PmywORpIDQBg&ved=0CBM QFjAA&sig2=w8kMGk_oXI3Ptc6MFdmCNg&usg=AFQjCNHnIrnNTGE8 BmOQVcZ3hQOvPXBQVw) [12].

10. Вяткин В. В., Дубинин В. Н. Верификация приложений IEC 61499 на основе метода Model checking.

(http://cyberleninka.ru/article/n/verifikatsiya-prilozheniy-iec-61499-na- osnove-metoda-model-checking) [38].

Из таблицы 1.2.1 следует, что в настоящее время отсутствует метод верификации автоматных программ, модели которых предложены в третьей главе диссертации.