Runtime Verification of Timed Petri Net Product Lines

Abstract

Petri Net Product Line (PNPL) is a type of Petri net focusing on the variability of reconfigurable industrial pipelines. This paper defines Timed Petri Net Product Lines (TPNPL), which incorporate time duration to PNPL as first-class citizens. TPNPLs rely on Coloured Petri Nets (CPN) for the notion of time. Additionally, we provide means for analysing TPNPL by runtime verification. The runtime verification features are implemented on top of the TeSSLa framework, which is composed by a TeSSLa language and interpreter. The TeSSLa interpreter receives the simulation of a TPNPL as a set of execution traces, the properties to analyse formalised in the TeSSLa language, and outputs an evaluation report. We update Titan, a modelling framework for the analysis of PNPL in Eclipse, in order to support the new features. To this end, Titan provides an automatic transformation of TPNPL into CPN, runs the CPN Tools engine for the simulation process, and forwards the execution traces and properties to the TeSSLa framework. Titan transparently coordinates all these steps.