uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
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)
Abstract [en]

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 [1], 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 [1]. 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
National Category
Engineering and Technology
URN: 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
Available from: 2008-10-17 Created: 2008-10-17 Last updated: 2013-10-03Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Abdulla, Parosh Aziz
By organisation
Department of Computer Systems
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 211 hits
ReferencesLink to record
Permanent link

Direct link