Return to search
## Specification and verification of communicating systems with value passing

The present Thesis addresses the problem of specification and verification of communicating systems with value passing. We assume that such systems are described

in the well-known Calculus of Communicating Systems, or rather, in its value passing

version. As a specification language we propose an extension of the Modal μ-Calculus,

a poly-modal first-order logic with recursion. For this logic we develop a proof system

for verifying judgements of the form b ⊢ Ε : Φ where E is a sequential CCS term

and b is a Boolean assumption about the value variables occurring free in E and Φ.

Proofs conducted in this proof system follow the structure of the process term

and the formula. This syntactic approach makes proofs easier to comprehend and

machine assist. To avoid the introduction of global proof rules we adopt a technique

of tagging fixpoint formulae with all relevant information needed for the discharge

of reoccurring sequents. We provide such tagged formulae with a suitable semantics.

The resulting proof system is shown to be sound in general and complete (relative

to external reasoning about values) for a large class of sequential processes and logic

formulae. We explore the idea of using tags to three different settings: value passing,

extended sequents. and negative tagging. / Graduate

Identifer | oai:union.ndltd.org:uvic.ca/oai:dspace.library.uvic.ca:1828/8287 |

Date | 16 June 2017 |

Creators | Gurov, Dilian Borissov |

Contributors | Kapron, Bruce M., Müller, Hausi A. |

Source Sets | University of Victoria |

Language | English, English |

Detected Language | English |

Type | Thesis |

Rights | Available to the World Wide Web |

Page generated in 0.0019 seconds