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
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, July 8, 2016 - 2:56:00 PM
Last modification on : Thursday, October 14, 2021 - 5:08:02 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



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⟩



Record views


Files downloads