Hae:

Oulun yliopiston väitöskirjat

ALGORITHMIC MULTIPARAMETERISED VERIFICATION OFSAFETY PROPERTIES, ACTA UNIVERSITATIS OULUENSIS A Scientiae Rerum Naturalium 560

ISBN-13:	978-951-42-6251-7
Kieli:	englanti
Kustantaja:	Oulun yliopisto
Oppiaine:	Luonnontieteet
Painosvuosi:	2010
Sidosasu:	pehmeäkantinen
Sijainti:	Print Tietotalo
Sivumäärä:	168
Tekijät:	SIIRTOLA ANTTI

20.00 €

Due to increasing amount of concurrency, systems have become difficult to design and analyse.In this effort, formal verification, which means proving the correctness of a system, has turned outto be useful. Unfortunately, the application domain of the formal verification methods is oftenindefinite, tools are typically unavailable, and most of the techniques do not suit especially wellfor the verification of software systems. These are the questions addressed in the thesis. A typical approach to modelling systems and specifications is to consider them parameterisedby the restrictions of the execution environment, which results in an (infinite) family of finite-stateverification tasks. The thesis introduces a novel approach to the verification of such infinitespecification-system families represented as labelled transition systems (LTSs). The key idea is toexploit the algebraic properties of the correctness relation. They allow the correctness of largesystem instances to be derived from that of smaller ones and, in the best case, an infinite family offinite-state verification tasks to be reduced to a finite one, which can then be solved using existingtools. The main contribution of the thesis is an algorithm that automates the reduction method. Aspecification and a system are given as parameterised LTSs and the allowed parameter values areencoded using first order logic. Parameters are sets and relations over these sets, which aretypically used to denote, respectively, identities of replicated components and relationshipsbetween them. Because the number of parameters is not limited and they can be nested as well,one can express multiply parameterised systems with a parameterised substructure, which is anessential property from the viewpoint of modelling software systems. The algorithm terminates onall inputs, so its application domain is explicit in this sense. Other proposed parameterisedverification methods do not have both these features. Moreover, some of the earlier results on theverification of parameterised systems are obtained as a special case of the results presented here. Finally, several natural and significant extensions to the formalism are considered, and it isshown that the problem becomes undecidable in each of the cases. Therefore, the algorithm cannotbe significantly extended in any direction without simultaneously restricting some other aspect.

Takaisin