Compositional verification of a distributed real-time arbitration protocol

A distributed real-time arbitration protocol is specified and verified using an assertional method. The formalism is based on classical Hoare triples which have been extended to deal with real-time properties. Tp verify design steps, a compositional proof system has been formulated for these extende...

Full description

Saved in:
Bibliographic Details
Published in:Real-time systems 1994-03, Vol.6 (2), p.173-205
Main Author: Hooman, Jozef
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A distributed real-time arbitration protocol is specified and verified using an assertional method. The formalism is based on classical Hoare triples which have been extended to deal with real-time properties. Tp verify design steps, a compositional proof system has been formulated for these extended triples. The intention of protocol is to resolve contention between a number of concurrent modules that compete to acquire control of a common bus. Therefore our proof method has been adapted to deal with concurrent processes that communicate by means of a common bus. Compositionality makes it possible to verify the required properties of the protocol using only the specifications of the modules. Next we give a top-down derivation of a program implementing a module according to its real-time specification.
ISSN:0922-6443
1573-1383
DOI:10.1007/BF01088595