Development and Verification of Dependable Software of Cyber-Physical Systems using Time-aware Computations [Elektronisk resurs]
-
Drozdov, Dmitrii (författare)
-
Vyatkin, Valeriy (preses)
-
Patil, Sandeep (preses)
-
Lobov, Andrei (opponent)
-
Dependable Communication and Computation Systems (medarbetare)
-
Luleå tekniska universitet Institutionen för system- och rymdteknik (utgivare)
- ISBN 9789177909019
- Publicerad: Luleå : Luleå University of Technology, 2021
- Engelska.
-
Serie: Doctoral thesis / Luleå University of Technology 1 jan 1997 → …, 1402-1544 1402-1544
-
Läs hela texten
-
Läs hela texten
- Relaterad länk:
-
http://www.ltu.se/ (Värdpublikation)
Sammanfattning
Ämnesord
Stäng
- Wired and wireless networking is becoming a necessary part of industrial control systems’ design and is one of the reasons that required a new cyber-physical approach to modelling. The phenomenon observed in cyber-physical systems (CPS) is a variety of cross-dependencies and influences between physical processes, computational devices and communications, which needs to be taken into account at the design and verification stage. Since most of the systems' functionality nowadays is implemented via software, the ability of software to be agnostic to the mentioned cross-influences is of high importance. This work introduces a concept called time-aware computations (TAC), which, instead of aiming at determinism, that is very expensive in distributed systems, aims at adaptability and robustness. It is based on the event-timestamping mechanism and is intended to let the developer handle each communication delay case individually thus minimizing its impact on functional properties of the automation system. It allows the controller to take into account actual point-to-point delay of the measured sensor readings, and adjust the control reaction accordingly, instead of trying to put the upper bound on it and wait for the maximum possible delay time. In industrial automation, the function block architecture of the IEC 61499 standard is increasingly used for modelling complex distributed automation systems. It is based on the concepts of event-driven block diagrams, and originally was created as a new programming paradigm for industrial automation controllers, but as a number of recent studies show, it also allows (and has been used) for modelling of CPS composed of physical processes combined with control and communication. The second major co-contribution of this work is a formal model of IEC 61499-based systems with timestamps that allows for modelling and verification of control logic (and closed-loop models) designed with TAC approach in mind. This would also allow for application of model-driven design methodologies later down the road. Third contribution is a software tool-chain that aims to greatly reduce the engineering work when applying formal verification to the designed systems. The proposed contributions' feasibility and effectiveness are demonstrated on a number of case studies.
Ämnesord
- Natural Sciences (hsv)
- Computer and Information Sciences (hsv)
- Computer Sciences (hsv)
- Naturvetenskap (hsv)
- Data- och informationsvetenskap (hsv)
- Datavetenskap (datalogi) (hsv)
- Engineering and Technology (hsv)
- Electrical Engineering, Electronic Engineering, Information Engineering (hsv)
- Computer Systems (hsv)
- Teknik och teknologier (hsv)
- Elektroteknik och elektronik (hsv)
- Datorsystem (hsv)
- Dependable Communication and Computation Systems (ltu)
- Kommunikations- och beräkningssystem (ltu)
Genre
- government publication (marcgt)
Indexterm och SAB-rubrik
- Abstract state machines
- CPS
- formal semantics
- formal verification
- IEC 61499
- time-aware computations
Inställningar
Hjälp
Titeln finns på 1 bibliotek.
Ange som favorit