Temporal theories as modularisation units for concurrent system specification

J. Fiadeiro, T. Maibaum

Research output: Contribution to journalArticle

84 Citations (Scopus)

Abstract

In this paper, we bring together the use of temporal logic for specifying concurrent systems, in the tradition initiated by A. Pnueli, and the use of tools from category theory as a means for structuring specifications as combinations of theories in the style developed by R. Burstall and J. Goguen. As a result, we obtain a framework in which systems of interconnected components can be described by assembling the specifications of their components around a diagram, using theory morphisms to specify how the components interact. This view of temporal theories as specification units naturally brings modularity to the description and analysis of systems. Moreover, it becomes possible to import into the area of formal development of reactive systems the wide body of specification techniques that have been defined for structuring specifications independently of the underlying logic, and that have been applied with great success in the area of Abstract Data Types. Finally, as a discipline of design, we use the object-oriented paradigm according to which components keep private data and interact by sharing actions, with a view towards providing formal tools for the specification of concurrent objects.
Original languageEnglish
Pages (from-to)239-272
Number of pages34
JournalFormal Aspects of Computing
Volume4
Issue number3
DOIs
Publication statusPublished - May 1992

Keywords

  • Modularity
  • Concurrency
  • Temporal logic
  • Reactive systems
  • Object-Oriented system

Fingerprint Dive into the research topics of 'Temporal theories as modularisation units for concurrent system specification'. Together they form a unique fingerprint.

Cite this