Skip to Main content Skip to Navigation
Conference papers

Cloud-Based Framework for Practical Model-Checking of Industrial Automation Applications

Abstract : In this paper we address practical aspects of applying the model-checking method for industrial automation systems verification. Several measures are proposed to cope with the high computational complexity of model-checking. To improve scalability of the method, cloud-based verification tools infrastructure is used. Besides, closed-loop plant controller modelling and synchronization of transitions in the SMV (input language for symbolic model checking) model aim at complexity reduction. The state explosion problem is additionally dealt with by using an abstraction of the model of the plant with net-condition event systems, which is then translated to SMV. In addition, bounded model-checking is applied, which helps to achieve results in cases when the state space is too high. The paper concludes with comparison of performance for different complexity reduction methods.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01343467
Contributor : Hal Ifip <>
Submitted on : Friday, July 8, 2016 - 2:56:00 PM
Last modification on : Thursday, November 26, 2020 - 2:56:03 PM

File

336594_1_En_8_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Sandeep Patil, Dmitrii Drozdov, Victor Dubinin, Valeriy Vyatkin. Cloud-Based Framework for Practical Model-Checking of Industrial Automation Applications. 6th Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS), Apr 2015, Costa de Caparica, Portugal. pp.73-81, ⟨10.1007/978-3-319-16766-4_8⟩. ⟨hal-01343467⟩

Share

Metrics

Record views

203

Files downloads

275