Verification of concurrent systems with parametric delays using octahedra
Document typeConference report
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Rights accessOpen Access
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.
CitationClarisó, R.; Cortadella, J. Verification of concurrent systems with parametric delays using octahedra. A: International Conference on Application of Concurrency to System Design. "Fifth International Conference on Application of Concurrency to System Design, ACSD 2005: 7-9 June 2005, St. Malo, France: proceedings". Institute of Electrical and Electronics Engineers (IEEE), 2005, p. 122-131.