Modeling and verification of temporal properties in cyber-physical systems

摘要

Cyber-physical systems (CPS) enable the development of complex real-world applications through the integration of computational and physical processes. The resulting processes are usually constrained by hard timing and physical requirements. These requirements are of paramount importance and must be handled at the different steps of the CPS process life cycle: from modeling until execution. Business Process Modeling Notation (BPMN) enables us to model processes in general. Even if BPMN provides a rich notation to cater for relevant features of process modeling, its capabilities are limited to capturing specific CPS processes properties, particularly physical and temporal properties. On the other hand, it is necessary to verify these properties to ensure that CPS can operate in a provably correct manner. In this paper, we focus on the problem of modeling and verifying CPS processes according to physical and temporal properties. To do so, we first propose to extend BPMN to handle specific CPS processes. Based on this extension, we propose a verification approach which relies on a constraint satisfaction model to check the consistency of the considered properties.