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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, Published 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.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 1579
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-27315DOI: 10.1007/3-540-49059-0_15ISBN: 978-3-540-65703-3 (print)ISBN: 978-3-540-49059-3 (print)OAI: oai:DiVA.org:uu-27315DiVA: diva2:55210
Conference
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

Authority records BETA

Abdulla, Parosh Aziz

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 459 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf