Return to search

Verification of Parameterized and Timed Systems : Undecidability Results and Efficient Methods

<p>Software is finding its way into an increasing range of devices (phones, medical equipment, cars...). A challenge is to design <i>verification</i> methods to ensure correctness of software. </p><p>We focus on <i>model checking</i>, 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.</p><p><i>Timed systems </i>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.</p><p>A <i>parameterized system</i> contains a variable number of components. The problem is to verify correctness regardless of the number of components. <i>Regular model checking</i> 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.</p><p>Finally, we consider systems which are both timed and parameterized: <i>Timed Petri Nets</i> (<i>TPNs</i>), and <i>Timed Networks</i> (<i>TNs</i>). 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.</p>

Identiferoai:union.ndltd.org:UPSALLA/oai:DiVA.org:uu-6891
Date January 2006
CreatorsDeneux, Johann
PublisherUppsala University, Department of Information Technology, Uppsala : Acta Universitatis Upsaliensis
Source SetsDiVA Archive at Upsalla University
LanguageEnglish
Detected LanguageEnglish
TypeDoctoral thesis, comprehensive summary, text
RelationDigital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, 1651-6214 ; 187

Page generated in 0.0021 seconds