Algorithmic multiparameterised verification of safety properties : process algebraic approach 

Author:  Siirtola, Antti^{1,2} 
Organizations: 
^{1}University of Oulu, Faculty of Science, Department of Information Processing Science ^{2}University of Oulu, Infotech Oulu 
Format:  ebook 
Version:  published version 
Access:  open 
Online Access:  PDF Full Text (PDF, 1 MB) 
Persistent link:  http://urn.fi/urn:isbn:9789514262524 
Language:  English 
Published: 
2010

Publish Date:  20100928 
Thesis type:  Doctoral Dissertation 
Defence Note:  Academic dissertation to be presented with the assent of the Faculty of Science of the University of Oulu for public defence in OPsali (Auditorium L10), Linnanmaa, on 8 October 2010, at 12 noon 
Reviewer: 
Professor Ranko Lazić Doctor Antti Puhakka 
Description: 
AbstractDue 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 out to be useful. Unfortunately, the application domain of the formal verification methods is often indefinite, tools are typically unavailable, and most of the techniques do not suit especially well for 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 parameterised by the restrictions of the execution environment, which results in an (infinite) family of finitestate verification tasks. The thesis introduces a novel approach to the verification of such infinite specificationsystem families represented as labelled transition systems (LTSs). The key idea is to exploit the algebraic properties of the correctness relation. They allow the correctness of large system instances to be derived from that of smaller ones and, in the best case, an infinite family of finitestate verification tasks to be reduced to a finite one, which can then be solved using existing tools. The main contribution of the thesis is an algorithm that automates the reduction method. A specification and a system are given as parameterised LTSs and the allowed parameter values are encoded using first order logic. Parameters are sets and relations over these sets, which are typically used to denote, respectively, identities of replicated components and relationships between 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 an essential property from the viewpoint of modelling software systems. The algorithm terminates on all inputs, so its application domain is explicit in this sense. Other proposed parameterised verification methods do not have both these features. Moreover, some of the earlier results on the verification 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 is shown that the problem becomes undecidable in each of the cases. Therefore, the algorithm cannot be significantly extended in any direction without simultaneously restricting some other aspect. see all

Series: 
Acta Universitatis Ouluensis. A, Scientiae rerum naturalium 
ISSNE:  1796220X 
ISBN:  9789514262524 
ISBN Print:  9789514262517 
Issue:  560 
Subjects:  
Copyright information: 
© University of Oulu, 2010. This publication is copyrighted. You may download, display and print it for your own personal use. Commercial use is prohibited. 