Active Learning of Formal Plant Models For Cyber-Physical Systems

As the world becomes more and more automated, the degree of cyber-physical systems involvement cannot be overestimated. A large part of them are safety-critical, thus, it is especially important to ensure their correctness before start of operation or reconfiguration. For this purpose the model chec...

Full description

Saved in:
Bibliographic Details
Main Authors: Ovsiannikova, Polina, Chivilikhin, Daniil, Ulyantsev, Vladimir, Stankevich, Andrey, Zakirzyanov, Ilya, Vyatkin, Valeriy, Shalyto, Anatoly
Format: Conference Proceeding
Language:English
Subjects:
Automata
Computational modeling
Context modeling
Correlation
Cyber-physical systems
Input variables
Model checking
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:As the world becomes more and more automated, the degree of cyber-physical systems involvement cannot be overestimated. A large part of them are safety-critical, thus, it is especially important to ensure their correctness before start of operation or reconfiguration. For this purpose the model checking approach should be used since it allows rigorously proving system correctness by checking all possible states. To ensure the compliance of controller-plant properties with system requirements, the closed-loop verification approach should be chosen, which requires not only a formal model of the controller, but also a formal model of the plant. In this paper we propose an approach for constructing formal models of context-free deterministic plants automatically using active learning algorithms. The case study shows its successful application to plant model generation for the elevator cyber-physical system.
ISSN:2378-363X
DOI:10.1109/INDIN.2018.8471924