Using forward reachability analysis for verification of lossy channel systems. (English) Zbl 1073.68675

Abdulla, Parosh Aziz; Collomb-Annichini, Aurore; Bouajjani, Ahmed; Jonsson, Bengt

Form. Methods Syst. Des. 25, No. 1, 39-65 (2004).

Summary: We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called Simple Regular Expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for computing (i) inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can straightforwardly construct an algorithm which explores the set of reachable states of a protocol, in order to check various safety properties. We also show how one can perform model-checking of LTL properties, using a standard automata-theoretic construction. It should be noted that all these methods are by necessity incomplete, even for the class of protocols with lossy channels.
To illustrate the applicability of our methods, we have developed a tool prototype and used the tool for automatic verification of (a parameterized version of) the bounded retransmission protocol.

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q45	Formal languages and automata
68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

model checking; protocol verification; automata; infinite-state systems; simple regular expressions

Software:

TREX; InVeSt