JUCS - Journal of Universal Computer Science 15(17): 3273-3304, doi: 10.3217/jucs-015-17-3273
Parametric Model-Checking of Stopwatch Petri Nets
expand article infoLouis-Marie Traonouez‡, Didier Lime‡, Olivier H. Roux‡
‡ IRCCyN, Nantes, France

Corresponding author: Louis-Marie Traonouez ( louis-marie.traonouez@irccyn.ec-nantes.fr )

© Louis-Marie Traonouez, Didier Lime, Olivier Roux.
This article is freely available under the J.UCS Open Content License.
Citation: Traonouez L-M, Lime D, Roux OH (2009) Parametric Model-Checking of Stopwatch Petri Nets. JUCS - Journal of Universal Computer Science 15(17): 3273-3304. https://doi.org/10.3217/jucs-015-17-3273
Open Access
Abstract
At the border between control and verification, parametric verification can be used to synthesize constraints on the parameters to ensure that a system verifies given specifications. In this paper we propose a new framework for the parametric verification of time Petri nets with stopwatches. We first introduce a parametric extension of time Petri nets with inhibitor arcs (ITPNs) with temporal parameters and we define a symbolic representation of the parametric state-space based on the classical state-class graph method. Then, we propose semi-algorithms for the parametric modelchecking of a subset of parametric TCTL formulae on ITPNs. These results have been implemented in the tool Romeo and we illustrate them in a case-study based on a scheduling problem.
Keywords
time Petri nets, stopwatches, model-checking, parameters, state-class graph