Runtime Verification of Timed Petri Nets

@inproceedings {1444,
	title = {Runtime Verification of Timed Petri Nets},
	booktitle = {International Workshop on Petri Nets and Software Engineering (PNSE)},
	year = {2024},
	month = {07/2024},
	publisher = {CEUR Workshop Proceedings},
	organization = {CEUR Workshop Proceedings},
	address = {Geneva, Switzerland},
	abstract = {<p>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{\textquoteright}s hospital.</p>
},
	keywords = {Runtime verification, TeSSLa, Timed Petri Net},
	url = {https://ceur-ws.org/Vol-3730/paper07.pdf},
	author = {Jos{\'e} Requeno and Elena G{\'o}mez-Mart{\'\i}nez and Hannes Kallwies and Melanie Haustein and Martin Leucker and Volker Stolz and Patrick St{\"u}nkel}
}