| Abstract |
|
A technique for the verification of concurrent parametric
timed systems is presented. In the systems under study,
each action has a bounded delay where the bounds are either
constants or parameters. Given a safety property, the
analysis computes automatically a set of constraints on the
parameters sufficient to guarantee the property. The main
contribution is an innovative representation of the parametric
timed state space based on bit-vectors. Experimental results
from the domain of timed circuits show that this representation
improves both CPU time and memory usage with
respect to another parametric approach, convex polyhedra.
|
Additional Information
|
Citation:
Robert Clarisó, Jordi Cortadella,
"Verification of Concurrent Systems with Parametric Delays Using Octahedra,"
acsd,
pp. 122-131,
Fifth International Conference on Application of Concurrency to System Design (ACSD'05),
2005
|