Model Checking of Mobile Systems and Diagnosability of Weakly-Fair Systems (2015)
The full text of this thesis is available from the Newcastle University Library website: https://theses.ncl.ac.uk/dspace/handle/10443/3059
Germanos, V., School of Computing Science, University of Newcastle upon Tyne
This thesis consists of two independent contributions. The first deals with model checking of reference passing systems, and the second considers diagnosability under the weak fairness assumption. Reference passing systems, like mobile and reconfigurable systems, are everywhere nowadays. The common feature of such systems is the possibility to form dynamic logical connections between the individual modules. However, such systems are very difficult to verify, as their logical structure is dynamic. Traditionally, decidable fragments of -Calculus, e.g. the well-known Finite Control Processes (FCP), are used for formal modelling of reference passing systems. Unfortunately, FCPs allow only "global" concurrency between processes, and thus cannot naturally express scenarios involving "local" concurrency inside a process. This thesis proposes Extended Finite Control Processes (EFCP), which are more convenient for practical modelling. Moreover, an almost linear translation of EFCPs to FCPs is developed, which enables efficient model checking of EFCPs. In partially observed systems, diagnosis is the task of detecting whether or not the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property, stating that in any possible execution an occurrence of a fault can eventually be diagnosed. In this thesis, diagnosability is considered under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever - it must eventually either fire or be disabled. A major flaw in a previous approach to WF-diagnosability in the literature is identified and corrected, and an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking is presented.