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

    • Fulltext


        Click here to view fulltext PDF

      Permanent link:

    • Keywords


      Compositional methods for concurrency; real-time applications; distributed computing

    • 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.

    • Author Affiliations


      J J M Hooman1 W P de Roever2

      1. Department of Mathematics and Computing Science, Eindhoven University of Technology, P.O. Box 513, Eindhoven - 5600 MB, The Netherlands
      2. Institute für Informatik and Praktische Mathematik II, Christian-Albrechts-Universität zu Kiel, Preusserstrasse 1-9, Kiel 1 - 2300, Germany
    • Dates

  • Sadhana | News

    • Editorial Note on Continuous Article Publication

      Posted on July 25, 2019

      Click here for Editorial Note on CAP Mode

© 2021-2022 Indian Academy of Sciences, Bengaluru.