Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol
1999 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: Proceddings of TACAS'99 / [ed] W. Rance Cleaveland, 1999, Vol. 1579, 208-222 p.Conference paper (Refereed)
We consider the problem of verifying automatically infinite- state systems that are systems of finite machines that communicate by exchanging messages through unbounded lossy fifo channels. In a previous work , we proposed an algorithmic approach based on constructing a symbolic representation of the set of reachable configurations of a system by means of a class of regular expressions (SREs). The construction of such a representation consists of an iterative computation with an acceleration technique which enhances the chance of convergence. This technique is based on the analysis of the effect of iterating control loops. In the work we present here, we experiment our approach and show how it can be effectively applied. For that, we developed a tool prototype based on the results in . Using this tool, we provide an automatic verification of (the parameterized version of) the Bounded Retransmission Protocol.
Place, publisher, year, edition, pages
1999. Vol. 1579, 208-222 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 1579
Engineering and Technology
IdentifiersURN: urn:nbn:se:uu:diva-27315DOI: 10.1007/3-540-49059-0_15ISBN: 978-3-540-65703-3ISBN: 978-3-540-49059-3OAI: oai:DiVA.org:uu-27315DiVA: diva2:55210
5th International Conference, TACAS’99 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS’99 Amsterdam, The Netherlands, March 22–28, 1999