uu.seUppsala University Publications

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt146",{id:"formSmash:upper:j_idt146",widgetVar:"widget_formSmash_upper_j_idt146",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt147_j_idt149",{id:"formSmash:upper:j_idt147:j_idt149",widgetVar:"widget_formSmash_upper_j_idt147_j_idt149",target:"formSmash:upper:j_idt147:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

Regular Model CheckingPrimeFaces.cw("AccordionPanel","widget_formSmash_some",{id:"formSmash:some",widgetVar:"widget_formSmash_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_all",{id:"formSmash:all",widgetVar:"widget_formSmash_all",multiple:true});
function selectAll()
{
var panelSome = $(PrimeFaces.escapeClientId("formSmash:some"));
var panelAll = $(PrimeFaces.escapeClientId("formSmash:all"));
panelAll.toggle();
toggleList(panelSome.get(0).childNodes, panelAll);
toggleList(panelAll.get(0).childNodes, panelAll);
}
/*Toggling the list of authorPanel nodes according to the toggling of the closeable second panel */
function toggleList(childList, panel)
{
var panelWasOpen = (panel.get(0).style.display == 'none');
// console.log('panel was open ' + panelWasOpen);
for (var c = 0; c < childList.length; c++) {
if (childList[c].classList.contains('authorPanel')) {
clickNode(panelWasOpen, childList[c]);
}
}
}
/*nodes have styleClass ui-corner-top if they are expanded and ui-corner-all if they are collapsed */
function clickNode(collapse, child)
{
if (collapse && child.classList.contains('ui-corner-top')) {
// console.log('collapse');
child.click();
}
if (!collapse && child.classList.contains('ui-corner-all')) {
// console.log('expand');
child.click();
}
}
PrimeFaces.cw("AccordionPanel","widget_formSmash_responsibleOrgs",{id:"formSmash:responsibleOrgs",widgetVar:"widget_formSmash_responsibleOrgs",multiple:true}); 2005 (English)Doctoral thesis, monograph (Other academic)
##### Abstract [en]

##### 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

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt434",{id:"formSmash:j_idt434",widgetVar:"widget_formSmash_j_idt434",multiple:true});
##### Supervisors

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt440",{id:"formSmash:j_idt440",widgetVar:"widget_formSmash_j_idt440",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt446",{id:"formSmash:j_idt446",widgetVar:"widget_formSmash_j_idt446",multiple:true});
Available from: 2005-02-08 Created: 2005-02-08 Last updated: 2011-02-18Bibliographically approved

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.

isbn
urn-nbn$(function(){PrimeFaces.cw("Tooltip","widget_formSmash_j_idt1144",{id:"formSmash:j_idt1144",widgetVar:"widget_formSmash_j_idt1144",showEffect:"fade",hideEffect:"fade",showDelay:500,hideDelay:300,target:"formSmash:altmetricDiv"});});

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1197",{id:"formSmash:lower:j_idt1197",widgetVar:"widget_formSmash_lower_j_idt1197",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1198_j_idt1200",{id:"formSmash:lower:j_idt1198:j_idt1200",widgetVar:"widget_formSmash_lower_j_idt1198_j_idt1200",target:"formSmash:lower:j_idt1198:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});