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
Networks of Identical Multi-Clock Timed Processes
Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology.
Article in journal (Refereed) Submitted
Identifiers
URN: urn:nbn:se:uu:diva-94526OAI: oai:DiVA.org:uu-94526DiVA: diva2:168402
Available from: 2006-05-12 Created: 2006-05-12Bibliographically approved
In thesis
1. Verification of Parameterized and Timed Systems: Undecidability Results and Efficient Methods
Open this publication in new window or tab >>Verification of Parameterized and Timed Systems: Undecidability Results and Efficient Methods
2006 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Software is finding its way into an increasing range of devices (phones, medical equipment, cars...). A challenge is to design verification methods to ensure correctness of software.

We focus on model checking, an approach in which an abstract model of the implementation and a specification of requirements are provided. The task is to answer automatically whether the system conforms with its specification.We concentrate on (i) timed systems, and (ii) parameterized systems.

Timed systems can be modeled and verified using the classical model of timed automata. Correctness is translated to language inclusion between two timed automata representing the implementation and the specification. We consider variants of timed automata, and show that the problem is at best highly complex, at worst undecidable.

A parameterized system contains a variable number of components. The problem is to verify correctness regardless of the number of components. Regular model checking is a prominent method which uses finite-state automata. We present a semi-symbolic minimization algorithm combining the partition refinement algorithm by Paige and Tarjan with decision diagrams.

Finally, we consider systems which are both timed and parameterized: Timed Petri Nets (TPNs), and Timed Networks (TNs). We present a method for checking safety properties of TPNs based on forward reachability analysis with acceleration. We show that verifying safety properties of TNs is undecidable when each process has at least two clocks, and explore decidable variations of this problem.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2006. 29 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 187
Keyword
Parameterized Systems, Timed Systems, Symbolic Model Checking, Forward Reachability, Acceleration, Robust Languages, Language Universality, Automata Minimization, Bisimulation
Identifiers
urn:nbn:se:uu:diva-6891 (URN)91-554-6574-9 (ISBN)
Public defence
2006-06-02, Häggsalen, Ångström Laboratory, Polacksbacken, Lägerhyddsvägen 1, Uppsala, 10:00
Opponent
Supervisors
Available from: 2006-05-12 Created: 2006-05-12 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Information Technology

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

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