Modelling and verifying time‐aware processes for cyber‐physical environments. Issue 1 (1st February 2019)

• Record Type: Journal Article
• Authors: Graja, Imen; Kallel, Slim; Guermouche, Nawal; Cheikhrouhou, Saoussen; Hadj Kacem, Ahmed
• Is Part Of: IET software. Volume 13:Issue 1(2019)
• Page Start: 36
• Page End: 48
• Publication Date: 2019-02-01
• Subjects: business data processing -- program verification -- formal specification -- formal verification; cyber-physical environments -- verifying time-aware processes -- consistent inter-CPS processes -- involved CPS processes -- collaborative time-aware CPS processes -- modelling rich CPS processes -- model business processes -- BPMN -- business process modelling notation -- expressive models -- rich models -- CPS life cycle development -- important steps -- physical properties -- particularly time-related properties -- capabilities -- software properties -- cyber-physical systems; Computer software -- Periodicals; Software engineering -- Periodicals; 005.1
• DOI: 10.1049/iet-sen.2018.5034
• Languages: English
• ISSNs: 1751-8806

Abstract

Abstract : Cyber‐physical systems (CPSs) are characterized by a multitude of physical and software. Particularly time‐related properties are of paramount importance and they can impact the behaviour of these systems. Designing and verifying CPS while tackling time‐related and physical properties are very important steps in the CPS life cycle development. Indeed, it is necessary to capture and characterize the different features and their dependencies with time through expressive models. Then, these models must be verified to prove their correctness. Existing process modelling languages such as business process modelling notation (BPMN) has been widely used to model business processes. However, BPMN lacks several features for modelling rich CPS processes such as those related to time and physical properties. In this study, the authors propose a verification framework for collaborative time‐aware CPS processes. In this context, they propose to extend BPMN to support the various CPS concepts and properties. Based on this extension, they propose a consistency verification approach, which aims to verify that the time‐related and physical properties associated with each process do not give rise to conflicts. Finally, they propose a compatibility verification approach, which aims to verify that the set of involved CPS processes form consistent inter‐CPS processes.