• Construction of CFC-programs b...

*Result*: Construction of CFC-programs by LTL-specification ; Построение CFC-программ ПЛК по LTL-спецификации

Title:
Construction of CFC-programs by LTL-specification ; Построение CFC-программ ПЛК по LTL-спецификации
Authors:
D. A. Ryabukhin, E. V. Kuzmin, V. A. Sokolov, Д. А. Рябухин, Е. В. Кузьмин, В. А. Соколов
Source:
Modeling and Analysis of Information Systems; Том 23, № 2 (2016); 173-184 ; Моделирование и анализ информационных систем; Том 23, № 2 (2016); 173-184 ; 2313-5417 ; 1818-1015
Publisher Information:
Yaroslavl State University
Publication Year:
2016
Collection:
Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Subject Terms:
CFC-диаграммы, construction and verification of PLC-programs, LTL-specification, CFC-diagrams, построение и верификация ПЛК-программ, LTL-спецификация
Document Type:
*Academic Journal* article in journal/newspaper
File Description:
application/pdf
Language:
Russian
Relation:
https://www.mais-journal.ru/jour/article/view/327/318; Кузьмин Е.В., Рябухин Д.А., Соколов В.А., “О выразительности подхода к построению ПЛК-программ по LTL-спецификации”, Моделирование и анализ информационных систем, 22:4 (2015), 507–520; [Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “On the Expressiveness of the Approach to Constructing PLC-programs by LTLSpecification”, Modeling and Analysis of Information Systems, 22:4 (2015), 507–520, (in Russian).]; КузьминЕ.В.,РябухинД.А.,СоколовВ.А.,“Моделированиесогласованногоповедения ПЛК-датчиков”, Моделирование и анализ информационных систем, 21:4 (2014), 75–90; [KuzminE.V.,RyabukhinD.A.,SokolovV.A.,“ModelingaConsistentBehavior of PLC-Sensors”, Modeling and Analysis of Information Systems, 21:4 (2014), 75–90, (in Russian).]; Рябухин Д. А., Кузьмин Е. В., Соколов В. А., “ Построение 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).]; Кузьмин Е. В., Соколов В. А., Рябухин Д. А., “ Построение и верификация LDпрограмм ПЛК по LTL-спецификации”, Моделирование и анализ информационных систем,20:6(2013),78–94; [KuzminE.V.,SokolovV.A.,RyabukhinD.A.,“Construction and Verification of PLC LD-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:6 (2013), 78–94, (in Russian).]; Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация ПЛКпрограмм по 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).]; КузьминЕ.В.,СоколовВ.А.,“Моделирование,спецификацияипостроениепрограмм логических контроллеров”, Моделирование и анализ информационных систем, 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).]; Baier C., Katoen J.-P., Principles of Model Checking, The MIT Press, 2008.; Clark E. M., Grumberg O., Peled D. A., Model Checking, The MIT Press, 2001.; CoDeSys, Controller Development System, http://www.3s-software.com/.; Kuzmin E.V., Sokolov V.A., Ryabukhin D.A., “Construction and Verification of PLCPrograms by LTL-Specification”, Automatic Control and Computer Sciences, 49:7 (2015), 453–465.; 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.; KuzminE.V.,SokolovV.A.,“Modeling,SpecificationandConstructionofPLC-programs”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563.; Kuzmin E.V., Ryabukhin D.A., Sokolov V.A., “Modeling a Consistent Behavior of PLCSensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614.; SMV, The Cadence SMV Model Checker, http://www.kenmcmil.com/smv.html.; Wardana A., Development of Automatic Program Verification for Continious Function Chart based on Model Checking, Kassel university press GmbH.; Ovataman T., Aral A., Polat D., Unver A. O., “An overview of model checking practices on verification of PLC software”, Software and Systems Modeling, 2014.; PakonenA.,MatasniemiT.,LahtinenJ.,KarhelaT.,“AtoolsetformodelcheckingofPLC software”, Proceedings of 18th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA2013, Cagliari, Italy, 2013.; Parr E. A., Programmable Controllers. An engineer’s guide, Newnes, 2003.; Петров И.В., Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования, М.: СОЛОН-Пресс, 2004; [Petrov I.V., Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, M.: SOLON-Press, 2004, (in Russian).]
DOI:
10.18255/1818-1015-2016-2-173-184
Availability:
https://www.mais-journal.ru/jour/article/view/327
https://doi.org/10.18255/1818-1015-2016-2-173-184
Rights:
Authors who publish with this journal agree to the following terms:Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access). ; Авторы, публикующие статьи в данном журнале, соглашаются на следующее:Авторы сохраняют за собой авторские права и предоставляют журналу право первой публикации работы, которая после публикации автоматически лицензируется на условиях Creative Commons Attribution License , которая позволяет другим распространять данную работу с обязательным сохранением ссылок на авторов оригинальной работы и оригинальную публикацию в этом журнале.Авторы имеют право размещать их работу в сети Интернет (например в институтском хранилище или персональном сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению и большему количеству ссылок на данную работу (См. The Effect of Open Access).
Accession Number:
edsbas.2C6A5193
Database:
BASE

*Further Information*

*This article continues a cycle of papers, which describe an approach to construction and verification of discrete PLC-programs by an LTL-specification. The approach provides a possibility of PLC-program correctness analysis by the model checking method. For the specification of the program behavior the linear-time temporal logic LTL is used. The correctness analysis of an LTL specification is performed automatically by the symbolic model checking tool Cadence SMV. Previously it was shown how ST-, LDand IL-programs are constructed by a correct (with verified program properties) LTL-specification. In this article a technology of CFC-program construction by an LTL-specification is described. The language CFC (Continuous Function Chart) is a variation of FBD (Function Block Diagram). FBD is a graphical language for microcircuits. CFC provides a possibility of free allocation of program components and connections on a screen. The approach to construction of CFC-programs is shown by an example. PLC-program representation on CFC within the approach to programming by LTL-specification differs from other representations. It gives the visualisation of a data flow from inputs to outputs. Influence and dependence between variables is explicitly shown during program execution within one PLC working cycle. In fact, CFC-program is a scheme of PLC-program data flow. ; Статья продолжает серию работ, посвященных подходу к построению и верификации «дискретных» программ логических контроллеров (ПЛК) по LTL-спецификации. Этот подход обеспечивает возможность анализа корректности программ логических контроллеров с помощью метода проверки модели (Model Checking). В рамках подхода в качестве языка спецификации программного поведения используется язык темпоральной логики LTL. Анализ корректности LTL-спецификации относительно программных свойств производится автоматически с помощью программного средства символьной проверки модели Cadence SMV. Ранее было показано, каким образом по корректной (проверенной на корректность относительно ...*