Algorithmic multiparameterised verification of safety properties : process algebraic approach
1University of Oulu, Faculty of Science, Department of Information Processing Science
2University of Oulu, Infotech Oulu
|Online Access:||PDF Full Text (PDF, 1 MB)|
|Persistent link:|| http://urn.fi/urn:isbn:9789514262524
|Publish Date:|| 2010-09-28
|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 OP-sali (Auditorium L10), Linnanmaa, on 8 October 2010, at 12 noon
Professor Ranko Lazić
Doctor Antti Puhakka
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 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 finite-state verification tasks. The thesis introduces a novel approach to the verification of such infinite specification-system 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 finite-state 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.
Acta Universitatis Ouluensis. A, Scientiae rerum naturalium
© University of Oulu, 2010. This publication is copyrighted. You may download, display and print it for your own personal use. Commercial use is prohibited.