Time-soundness of time petri nets modelling time-critical systems

Guanjun Liu, Changjun Jiang, Mengchu Zhou

Research output: Contribution to journalArticlepeer-review

22 Scopus citations

Abstract

The correctness of a time-critical system is closely related to the time of responding and performing every event. Our motivation example, alternating bit protocol, and application example, multi-track level crossing with sensors, both demonstrate that some nondeterministic behaviours can take place if the time associated with events is configured inappropriately or some concurrent events are controlled imperfectly in an overlapping period. These nondeterministic behaviours decrease the reliability and/or safety of a time-critical system. Therefore, it is valuable to formalise and check (non)determinacy. Time Petri Nets (TPN) in which the firing of every event is limited to a fix time interval are used to model time-critical systems in this article. We proposes a novel notion for TPN named time-soundness. It guarantees that the system always owns deterministic behaviours after any event is performed no matter when the event is performed. We utilise the notion of bisimulation to prove that the time-soundness can guarantee the behavioural determinacy. We propose an algorithm to check time-soundness, develop the related tool, and do experiments to show the usefulness and effectiveness of our notion and method.

Original languageEnglish (US)
Article number11
JournalACM Transactions on Cyber-Physical Systems
Volume2
Issue number2
DOIs
StatePublished - 2018

All Science Journal Classification (ASJC) codes

  • Control and Optimization
  • Artificial Intelligence
  • Human-Computer Interaction
  • Hardware and Architecture
  • Computer Networks and Communications

Keywords

  • Bisimulation
  • Concurrency
  • Determinism
  • Model checking
  • Time Petri nets
  • Time-critical systems

Fingerprint

Dive into the research topics of 'Time-soundness of time petri nets modelling time-critical systems'. Together they form a unique fingerprint.

Cite this