О выразительности подхода к построению ПЛК-программ по LTL-спецификации
https://doi.org/10.18255/1818-1015-2015-4-507-520
Аннотация
Об авторах
Е. В. Кузьмин
Ярославский государственный университет им. П.Г. Демидова
Россия
Россия
доктор физ.-мат. наук, доцент, профессор кафедры теоретической информатики
ул. Советская, 14, г. Ярославль, 150000 Россия
Д. А. Рябухин
Ярославский государственный университет им. П.Г. Демидова
Россия
Россия
аспирант
ул. Советская, 14, г. Ярославль, 150000 Россия
В. А. Соколов
Ярославский государственный университет им. П.Г. Демидова
Россия
Россия
доктор физ.-мат. наук, профессор, зав. кафедрой теоретической информатики
ул. Советская, 14, г. Ярославль, 150000 Россия,
Список литературы
1. Кузьмин Е.В., Рябухин Д.А., Соколов В.А., “Моделирование согласованного поведения ПЛК-датчиков”, Моделирование и анализ информационных систем, 21:4 (2014), 75–90; [Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Modeling and Analysis of Information Systems, 21:4 (2014), 75–90, (in Russian).]
2. Рябухин Д.А., Кузьмин Е.В., Соколов В.А., “Построение IL-программ ПЛК по LTL- спецификации”, Моделирование и анализ информационных систем, 21:2 (2014), 26– 38; [Ryabukhin D. A., Kuzmin E. V., Sokolov V. A., “Construction of PLC IL-programs by LTL-specification”, Modeling and Analysis of Information Systems, 21:2 (2014), 26–38, (in Russian).]
3. Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация LD- программ ПЛК по LTL-спецификации”, Моделирование и анализ информационных систем, 20:6 (2013), 78–94; [Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:6 (2013), 78–94, (in Russian).]
4. Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация ПЛК-программ по LTL-спецификации”, Моделирование и анализ информационных систем, 20:4 (2013), 5–22; [Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:4 (2013), 5–22, (in Russian).]
5. Кузьмин Е.В., Соколов В.А., “Моделирование, спецификация и построение программ логических контроллеров”, Моделирование и анализ информационных систем, 20:2 (2013), 104–120; [Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-programs”, Modeling and Analysis of Information Systems, 20:2 (2013), 104–120, (in Russian).]
6. Минский М., Вычисления и автоматы, М.: Мир, 1971; [Minsky M., Computation: Finite and Infinite Machines, Prentice-Hall, Inc., 1967.]
7. Петров И.В., Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования, М.: СОЛОН-Пресс, 2004; [Petrov I.V., Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, M.: SOLON-Press, 2004, (in Russian).]
8. Baier C., Katoen J.-P., Principles of Model Checking, The MIT Press, 2008.
9. Clark E. M., Grumberg O., Peled D. A., Model Checking, The MIT Press, 2001.
10. CoDeSys, Controller Development System, http://www.3s-software.com/.
11. Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD Programs by the LTL Specification”, Automatic Control and Computer Sciences, 48:7 (2014), 424–436.
12. Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-rograms”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563.
13. Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614.
14. Parr E. A., Programmable Controllers. An engineer’s guide, Newnes, 2003.
15. Schroeppel R., A Two Counter Machine Cannot Calculate 2N, Memo 257. Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1972.
16. SMV, The Cadence SMV Model Checker, http://www.kenmcmil.com/smv.html.
Рецензия
Для цитирования:
Кузьмин Е.В., Рябухин Д.А., Соколов В.А. О выразительности подхода к построению ПЛК-программ по LTL-спецификации. Моделирование и анализ информационных систем. 2015;22(4):507-520. https://doi.org/10.18255/1818-1015-2015-4-507-520
For citation:
Kuzmin E.V., Ryabukhin D.A., Sokolov V.A. On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification. Modeling and Analysis of Information Systems. 2015;22(4):507-520. (In Russ.) https://doi.org/10.18255/1818-1015-2015-4-507-520
Просмотров: 975
Послать статью по эл. почте 