Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 15 / Issue 17

available in:   PDF (391 kB) PS (369 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-015-17-3273


Parametric Model-Checking of Stopwatch Petri Nets

Louis-Marie Traonouez (IRCCyN, France)

Didier Lime (IRCCyN, France)

Olivier H. Roux (IRCCyN, France)

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: model-checking, parameters, state-class graph, stopwatches, time Petri nets

Categories: D.2.2, D.2.4