Runtime Verification of Timed Petri Nets

Abstract

Timed Petri net (TPN) is a type of Petri net for modeling concurrent systems that incorporates time durations as first-class citizens. This paper provides a means for analyzing TPN by runtime verification, a lightweight verification approach where a single run of a system is monitored. In particular, we assume the discrete-time semantics of TPN. We propose a TPN module for the definition and analysis of a TPN in the runtime verification framework TeSSLa, which is composed of the TeSSLa language, an interpreter, and a dedicated hardware monitor for online real-time analysis with minimal intrusion. The TeSSLa interpreter receives the definition of the TPN, the properties to analyze, and a set of execution traces and outputs an evaluation report. Our solution provides an efficient and user-friendly approach for the runtime verification of concurrent systems that are described by a high-level modeling language. For a practical evaluation of the approach, we have used parts of the library to model and analyze the workflow for examining specimens within the pathology department of Bergen’s hospital.