Breadcrumb

 
 

A state-oriented, partial-order model and logic for distributed systems verification

Title:

A state-oriented, partial-order model and logic for distributed systems verification

Narayanan, Vasumathi K (1997) A state-oriented, partial-order model and logic for distributed systems verification. PhD thesis, Concordia University.

[img]
Preview
PDF
10Mb

Abstract

A theory of state-oriented, partially-ordered 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 Mpm-states 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 Mpm-states 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 product-machine is generated virtually , simulated by the sum-machine. 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 space-time 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 13:11
Last Modified:08 Dec 2010 10:14
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Document Downloads

More statistics for this item...

Concordia University - Footer