Verification of Concurrent Systems with Parametric Delays Using Octahedra

Issue title: The Fourth Special Issue on Applications of Concurrency to System Design (ACSD05)

Article type: Research Article

Authors: Clarisó, Robert | Cortadella, Jordi

Affiliations: Universitat Oberta de Catalunya, Spain. E-mail: rclariso@uoc.edu | Universitat Politècnica de Catalunya, Spain. E-mail: jordi.cortadella@upc.edu

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 that is 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 the efficiency of the verification significantly with a small impact on the accuracy of the derived constraints.

Keywords: Formal Verification, Abstract Interpretation, Parametric Timed Systems

Journal: Fundamenta Informaticae, vol. 78, no. 1, pp. 1-33, 2007