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.
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