Towards an integrated tool support for the analysis of IOPT Nets using the Spin Model Checker

Abstract

This paper presents a model translation to allow automatic simulation and verification of controller models for cyber-physical systems. The models are constructed using IOPT nets, a non-autonomous Petri nets class. Those models are then translated into Promela models to be executed by the Spin model checker, a widely used open-source software verification tool. Three illustrative examples are presented: one autonomous model and two non-autonomous models. As future work, it is foreseen the integration with the freely available IOPT-Tools framework.