With increase in use formal verification tools and methods distributed systems, it is becoming more challenging to analyse the execution traces generated by tools. This paper presents a method for unification of industrial automation based on IEC 61499 standard. Execution trace system sequence events, where each event represents change state system. allow developers explore safely behavior control software. can be obtained several ways, including monitoring real (or its simulator), or as...

This paper introduces a conceptual framework for complex control algorithms in form of hyperprocess model.To demonstrate the practical value model we describe grammar and translational semantics process-oriented language, known as Reflex or "C with processes".Expressive properties presented notation are shown on an example algorithm design hand dryer device.Finally, give short report about application language results, which have been obtained during its usage.

Reflex is a process-oriented language that provides design of easy-to-maintain control software. The has been successfully used in several safety-critical cyber-physical systems, e. g. software for silicon single crystal growth furnace. Now, the main goal project development support computer aided engineering targeted to application. current issue we discuss this paper creating static verification methods programs. As base most techniques formal semantics, presents semantics form...

Automation systems within nuclear laboratories are intended to work under harsh operating conditions. SPES (Selective Production of Exotic Species) is a research facility currently construction by INFN (Istituto Nazionale di Fisica Nucleare), dedicated the production and study Radioactive Ion Beams (RIBs). Isotopes produced Target Source (TIS) unit, vacuum vessel that must be replaced on regular basis. The highly radioactive environment necessitates deployment set automated unit's remote...

АВТОМАТИЗИРОВАННАЯ ВЕРИФИКАЦИЯ АЛГОРИТМОВ УПРАВЛЕНИЯ СЛОЖНЫМИ ТЕХНОЛОГИЧЕСКИМИ ОБЪЕКТАМИ НА

The process-oriented programming language Reflex is a for cyber-physical systems' (CPS) control software. It based on the formal hyperprocess model. has proved effective in industrial projects. But using difficult due to lack of IDE programs. In this paper, we develop cloud desktop - RIDE. Modularity main principle RIDE architecture. meets needs CPS software development process and allows extending functionality. extensions may provide various functionalities, such as graphical...

We address the formal verification of control software critical systems, i.e., ensuring absence design errors in a system with respect to requirements. Control systems are usually based on industrial controllers, also known as Programmable Logic Controllers (PLCs). A specific feature PLC is scan cycle: 1) inputs read, 2) states change, and 3) outputs written. Therefore, order formally verify PLC, e.g., by model checking, it necessary reason both terms state transitions within cycle larger...

The ever-increasing complexity of industrial control systems generates a demand for reliable development methods. IEC 61499, recent standard, helps to develop complex distributed based on their positive characteristics, namely reusability, reconfigurability, interoperability, and portability. Formal verification techniques, such as model checking, have been proposed ensure the correctness these during design time. However, they do not consider presence environment that can impact application...

RIDE is an integrated development environment for the Reflex language, a process-oriented language designed developing control algorithms cyber-physical systems. was developed based on Eclipse Theia – open source web IDE framework. Despite being technologies such as Node.JS, can not serve application multiple users simultaneously. The paper describes approach configuring server and creating host program that makes hosting public possible. It provides problem analysis, tools frameworks...

This paper concerns a formal four-component dynamic verification model of process-oriented control algorithms, developed for cyber-physical systems (CPS) - support system CPS. It is four interacting extended hyperprocesses. The hyperprocess includes the Message queue data type. introduced approach bases on plant simulator, work scripts management and automatic check algorithm reactions. We used specification simulator behavior, as well test cases management. Test tuning simulation commands...

Онтологический подход к организации шаблонов требований в рамках системы поддержки формальной верификации распределенных программных систем Н.О.Гаранина (Институт информатики им.А.П.Ершова), В.Е.Зюбин автоматики и электрометрии), Т.В.Лях электрометрии) В статье описывается структура онтологии требований, извлекаемых из текстов технической документации

Embedded systems based on small cheap microcontrollers surround all aspects of our lives. Due to inherent concurrency microcontroller software can exhibit complex behavior that is best specified using specialized programming langauges. The IndustrialC language has been successfully used in a number embedded appications and proven useful for specification reactive within the constrained computational capabilities 8-bit microcontrollers. Many microcontroller-based are considered...

The article focuses on evaluation of the applicability existing semantic segmentation algorithms for Duckietown simulator. is an open research project in field autonomously controlled robots. explores classical image algorithms. Their analysis carried out. With help them, we want to make a dataset training neural networks. following was investigated: edge-detection techniques, threshold algorithms, region growing, based clustering, also reviewed networks designed and machine learning...

Process-oriented programming is a natural way to describe control software as set of communicating processes with executable states, that allows speed up its development. The Reflex language one the representatives family process-oriented languages. paper justifies possibility applying model checking method for verification programs using hand dryer case study. study includes specification requirements dryer, in it, result translation program and into input Promela checker SPIN LTL formulas,...

The choice of an adequate notation and subsequent system formalization are the crucial points for design cyber-physical systems (CPSs).Here, appropriate allows explicit specification deterministic behavior specified initial states inputs.We base our study on industrial example (water tank) that comprises nominal as well safety-critical states, focus notation's support to validate/verify safety properties.Several notations (e.g.Matlab/Simulink © ) simulate such a hybrid have been tried based...

Верификация промышленных алгоритмов управления методом Model checking в сочетании с концепцией виртуальных объектов Лях Т.В.(Институт автоматики и электрометрии СО РАН, Новосибирский государственный университет), Зюбин В.Е.(Институт университет) На сегодняшний день текущая практика промышленной автоматизации такова, что тестирование управляющих подавляющем большинстве случаев начинается только при запуске ПО на реальном объекте.В результате проверка алгоритма откладывается до этапа...

With the increase in use of distributed control systems industrial automation, it is becoming more challenging to analyze behavior system evaluate its quality. The lack data coming from during operation also complicates debugging and error finding software. paper presents a quality method IEC 61499 proposed based on combination several techniques: monitoring behavior, recovering missing with simulator, explanation recovered traces by highlighting sequence events that led explored state...

This paper presents and discusses two methods for collecting data from decentralised control applications designed in IEC 61499 architecture. The topic is justified by the growing use of Cloud-based storage presentation services Internet-of-Things systems. Enabling devices with capabilities storing Cloud using web-based analytics great practical importance. Moreover, what most elegant way to configure such streaming an open question, solving which this aims provide state-of-the-art information.

This paper concerns automatic verification of process-oriented control algorithms in cyber-physical systems. We introduce a approach based on plant simulator and present an implementation the using LabVIEW package Reflex language translator.