Narayanan, Vasumathi K (1997) A stateoriented, partialorder model and logic for distributed systems verification. PhD thesis, Concordia University.

PDF
10MB 
Abstract
A theory of stateoriented, partiallyordered model named, Communicating Minimal prefix machines (CMpms) that represent a fixed set of processes, is presented. Each of these Mpms is a possibly infinite, State Transition System . Communication among a set of Mpms is by synchronization. Enriched by a global, causal dependency relation among the Mpmstates that is partial , the disjoint union of CMpms comprise a sum machine . It is shown that the set of all global states of the product machine of CMpms is obtainable dynamically from the local Mpmstates of the sum machine using the monotonicity property, linking the product machine's global states and the sum machine's local ones. In this sense, the productmachine is generated virtually , simulated by the summachine. More interestingly, it is shown that from every given set of Communicating Finite state machines (CFsms), a truncated (finite) version of a set of CMpms and so a sum machine can be generated in a recursive functional manner. The set of global states of the product machine of CMpms surjectively map onto that of CFsms. Consequently, it is possible to generate all the global states of the latter using the local states of the sum machine composed by a corresponding set of CMpms. The sum machine models true causality and hence true sequence, true concurrency and true choice among local states, as exhibited by the original input CFsms specification without enumerating all the runs of the system nor all the nondeterministic interleavings of each run as opposed to the product machine . A Spatial, temporal logic or spacetime logic named CML (Computational Mpms Logic), is proposed that combines the conventional branching time feature with what is proposed as branching space feature: the latter corresponds to concurrency just as the former to conflicts , as exhibited by the input specification. CML therefore introduces operators to reason about properties of interleavings within each run, orthogonal to the branching time operators, to reason about runs . The logic turns out to be more expressive than the ones in vogue for specifying properties of concurrent systems. In addition, CML coupled with the sum machine model, enables the implementation of a deterministic model checker algorithm to verify the properties of a given CFsm system that is free of exponential complexity caused by the enumeration of runs as well as that of all interleavings within each run.
Divisions:  Concordia University > Faculty of Engineering and Computer Science > Computer Science and Software Engineering 

Item Type:  Thesis (PhD) 
Authors:  Narayanan, Vasumathi K 
Pagination:  xxi, 238 leaves : ill. ; 29 cm. 
Institution:  Concordia University 
Degree Name:  Theses (Ph.D.) 
Program:  Computer Science and Software Engineering 
Date:  1997 
Thesis Supervisor(s):  Li, H. F 
ID Code:  430 
Deposited By:  Concordia University Libraries 
Deposited On:  27 Aug 2009 17:11 
Last Modified:  08 Dec 2010 15:14 
Related URLs: 
Repository Staff Only: item control page