A Coloured Petri Net approach to model and analyze safety-critical interactive systems

Jaidka, Sapna; Reeves, Steve; Bowen, Judy

doi:10.1109/APSEC48747.2019.00054

Files

Camera-ReadyVersionAPSEC.pdf

Accepted version, 584.6Kb

DOI

10.1109/APSEC48747.2019.00054

Citation

Export citation

Jaidka, S., Reeves, S., & Bowen, J. (2019). A Coloured Petri Net approach to model and analyze safety-critical interactive systems. In Proceedings of 2019 26th Asia-Pacific Software Engineering Conference (APSEC) (pp. 347–354). Washington, DC, USA: IEEE. https://doi.org/10.1109/APSEC48747.2019.00054

Permanent Research Commons link: https://hdl.handle.net/10289/13631

Abstract

To gain confidence in safety-critical interactive systems, formal modelling and analysis plays a vital role. The aim of this paper is to use Coloured Petri Nets to model and analyze safety-critical interactive systems. We present a technique to construct a single Coloured Petri Net model of the user interface, interaction and functionality of safety-critical interactive systems and then analyze the achieved Coloured Petri Net model using a state space analysis method. There are several reasons for using Coloured Petri Nets. Coloured Petri Nets provides a graphical representation and hierarchical structuring mechanism, and a state space verification technique, which allows querying the state space to investigate behaviours of a system. There are several tools that supports Coloured Petri Nets including the CPN Tool which helps in building CPN models and allows simulation and analysis using state spaces. The technique to model and analyze safety-critical interactive systems is illustrated using a simplified infusion pump example.

Date

2019

Type

Conference Contribution

Publisher

IEEE

Rights

This is an author’s accepted version of an article published in the Proceedings of 2019 26th Asia-Pacific Software Engineering Conference (APSEC). © 2019 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE

Collections

Computing and Mathematical Sciences Papers [1413]