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
On-the-fly analysis of systems with unbounded, lossy FIFO channels
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
1998 (English)In: Computer Aided Verification: Proceedings of 10th International Conference, CAV'98 / [ed] Alan J. Hu, Moshe Y. Vardi, 1998, Vol. 1427, 305-318 p.Conference paper, Published paper (Refereed)
Abstract [en]

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 (i) computing 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 of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.

Place, publisher, year, edition, pages
1998. Vol. 1427, 305-318 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 1427
Keyword [en]
finite state machines, unreliable channels, programs
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-27321DOI: 10.1007/BFb0028754ISBN: 978-3-540-64608-2 (print)ISBN: 978-3-540-69339-0 (print)OAI: oai:DiVA.org:uu-27321DiVA: diva2:55216
Conference
10th International Conference, CAV'98 Vancouver, BC, Canada, June 28 – July 2, 1998
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
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: 372 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