×

Compositional verification of asynchronous processes via constraint solving. (English) Zbl 1081.68646

Caires, Luís (ed.) et al., Automata, languages and programming. 32nd international colloquium, ICALP 2005, Lisbon, Portugal, July 11–15, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27580-0/pbk). Lecture Notes in Computer Science 3580, 1239-1250 (2005).
Summary: We investigate the foundations of a constraint-based compositional verification method for infinite-state systems. We first consider an asynchronous process calculus which is an abstract formalization of several existing languages based on the blackboard model. For this calculus we define a constraint-based symbolic representation of finite computations of a compositional model based on traces. The constraint system we use combines formulas of integer arithmetics with equalities over uninterpreted functions in which satisfiability is decidable. The translation is inductively defined via a CLP program. Execution traces of a process can be compositionally obtained from the solutions of the answer constraints of the CLP encoding. This way, the task of compositional verification can be reduced to constraint computing and solving.
For the entire collection see [Zbl 1078.68001].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI