Temporal theories as modularisation units for concurrent system specification

J. Fiadeiro, T. Maibaum

Research output: Contribution to journalArticlepeer-review

87 Citations (Scopus)


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
Issue number3
Publication statusPublished - May 1992


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


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

Cite this