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
Regular Model Checking
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2005 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

A major current challenge in the area of program verification is to extend its applicability to infinite-state systems. A system can be infinite-state because it operates on unbounded data structures, such as queues, stacks, integers, etc., or because its description is parameterized by the number of components inside the system.

In this thesis, we apply the framework of regular model checking for algorithmic verification of infinite-state systems. In regular model checking, system states are represented by words over a finite alphabet and the transition relation by a regular length-preserving relation on words. The contributions can be divided into three categories: acceleration techniques, specification, and implementation.

The aim of acceleration techniques is to consider arbitrarily long execution sequences. This is usually done by computing the transitive closure: the effect of applying a transition relation an arbitrary number of times. We give several novel algorithms for computing the transitive closure. The algorithms are general in the sense that they are not dependent on the type of data structure or if a parameterized system is considered. Hence, they unify several previous techniques based on regular sets. We develop a theoretical framework to explain the algorithms and prove their correctness. Using the new algorithms, we can automatically verify several examples of parameterized and infinite-state systems. While computing transitive closures is not possible in general, we give a sufficient condition under which our algorithms terminate.

We extend the so-called automata-theoretic approach and define the logic LTL(MSO) used for specification of systems. The logic is an extension of propositional linear temporal logic with the added ability to reason about words of arbitrary length. We show how to transform formulas in this extended logic into a suitable form for the verification algorithms. Using the logic, we can express parameterized fairness and liveness properties.

Finally, we describe in detail an implementation of regular model checking. It includes an automata package implemented using BDDs, a symbolic representation of finite sets. We evaluate the algorithms for computing transitive closures by verifying several examples of parameterized and infinite-state systems.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis , 2005. , 149 p.
Series
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 60
Keyword [en]
formal methods, model checking, verification, regular sets
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-4793ISBN: 91-554-6137-9 (print)OAI: oai:DiVA.org:uu-4793DiVA: diva2:165795
Public defence
2005-03-02, Häggsalen, Ångström Laboratory, Lägerhyddsvägen 1, Uppsala, 13:00
Opponent
Supervisors
Available from: 2005-02-08 Created: 2005-02-08 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text
Buy this publication >>

By organisation
Division of Computer SystemsComputer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 1471 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