An introduction to compositional methods for concurrency and their application to real-time

J.J.M. Hooman, W.P. Roever, de

Research output: Contribution to journalArticleAcademicpeer-review

2 Citations (Scopus)
90 Downloads (Pure)

Abstract

Formal methods to specify and verify concurrent programs with synchronous message passing are discussed. We stress the development towards compositional methods, i.e. methods in which the specification of a compound program can be inferred from specifications of its constituents without reference to the internal structure of those parts. Compositionality enables verification during the process of (top-down) design — the derivation of correct programs — instead of the more familiar a-posteriori verification based on already completed program codes. We sketch the transition from non-compositional towards compositional methods for concurrent programs, indicating the main principles behind compositionality. Having achieved a compositional framework based on classical Hoare triples, we discuss extensions to achieve a convenient formalism to specify and verify reactive systems that have an intensive interaction with their environment. Next this Hoare-style framework is adapted to specify and verify real-time properties, and a compositional proof method is formulated for real-time distributed computing. Compositional reasoning during top-down development of a real-time program is illustrated by an example concerning a watchdog timer.
Original languageEnglish
Pages (from-to)29-73
JournalSadhana : Academy Proceedings in Engineering Sciences (Indian Academy of Sciences)
Volume17
Issue number1
DOIs
Publication statusPublished - 1992

Fingerprint Dive into the research topics of 'An introduction to compositional methods for concurrency and their application to real-time'. Together they form a unique fingerprint.

  • Cite this