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

Direct link
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
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.
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 187
Parameterized Systems, Timed Systems, Symbolic Model Checking, Forward Reachability, Acceleration, Robust Languages, Language Universality, Automata Minimization, Bisimulation
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
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
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

Total: 150 hits
ReferencesLink to record
Permanent link

Direct link