Name
Abstract | ||
|---|---|---|
We address the verification problem of FIFO channel systems by applying the symbolic analysis principle. Communication protocols can be modelled by a finite set of finite-state machines (CFSMs) that communicate between each other by exchanging messages via unbounded FIFO channels/queues.A Finite Union of Deterministic Finite Automata (FUDFA) is used to represent (possibly) infinite set of queue contents.Quite a few operations needed to symbolically analyze such systems can be implemented on the union of DFAs in polynomial time.The advantage gained by this approach is that the inclusion between finite unions DFAs can be checked efficiently. We show that FUDFAs can be used for the forward and backward reachability analysis of the systems.It also lifts this approach for the case of a protocol with n queues.We use this fact to define a generic reachability analysis semi-algorithm parameterized by a set of cycles 驴.Given a set of configuration, this semi-algorithm performs a least fix-point calculation to construct the set of its successors (or prdecessors). At each step, the search is acclerated by considering the cycles in 驴 as additional "meta-transitions", an approach adopted similar in nature to that proposed by Boigelot and Godefroid. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1109/SEFM.2004.40 | SEFM |
Keywords | Field | DocType |
reachability analysis,communication protocol,symbolic verification,finite unions dfas,fifo channel system,symbolic analysis principle,finite union,finite set,infinite systems,deterministic finite automata,unbounded fifo channel,generic reachability analysis semi-algorithm,fixed point,formal verification,finite state machine,queueing theory,polynomial time,symbolic analysis,dfa,finite automata | Finite set,FIFO (computing and electronics),Deterministic finite automaton,Computer science,Reachability,Theoretical computer science,Finite-state machine,Infinite set,Queueing theory,Formal verification | Conference |
ISBN | Citations | PageRank |
0-7695-2222-X | 1 | 0.37 |
References | Authors | |
0 | 1 | |