Abstract
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.
| Identifer | oai:union.ndltd.org:oulo.fi/oai:oulu.fi:isbn978-951-42-6252-4 |
| Date | 28 September 2010 |
| Creators | Siirtola, A. (Antti) |
| Publisher | University of Oulu |
| Source Sets | University of Oulu |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/doctoralThesis, info:eu-repo/semantics/publishedVersion |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess, © University of Oulu, 2010 |
| Relation | info:eu-repo/semantics/altIdentifier/pissn/0355-3191, info:eu-repo/semantics/altIdentifier/eissn/1796-220X |
Page generated in 0.0021 seconds