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

Fingerprint

Modularization
Concurrent Systems
Specification
Specifications
Unit
Abstract data types
Abstract Data Types
Category Theory
Temporal logic
Reactive Systems
Temporal Logic
Modularity
Morphisms
Object-oriented
Concurrent
Sharing
Diagram
Paradigm
Logic

Keywords

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

Cite this

@article{c8f2b4d876c3461d902fb29d624092bf,
title = "Temporal theories as modularisation units for concurrent system specification",
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.",
keywords = "Modularity, Concurrency, Temporal logic, Reactive systems, Object-Oriented system",
author = "J. Fiadeiro and T. Maibaum",
note = "Copyright 2007 Elsevier B.V., All rights reserved.",
year = "1992",
month = "5",
doi = "10.1007/BF01212304",
language = "English",
volume = "4",
pages = "239--272",
journal = "Formal Aspects of Computing",
issn = "0934-5043",
publisher = "Springer Verlag",
number = "3",

}

Temporal theories as modularisation units for concurrent system specification. / Fiadeiro, J.; Maibaum, T.

In: Formal Aspects of Computing, Vol. 4, No. 3, 05.1992, p. 239-272.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Temporal theories as modularisation units for concurrent system specification

AU - Fiadeiro, J.

AU - Maibaum, T.

N1 - Copyright 2007 Elsevier B.V., All rights reserved.

PY - 1992/5

Y1 - 1992/5

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

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

KW - Modularity

KW - Concurrency

KW - Temporal logic

KW - Reactive systems

KW - Object-Oriented system

U2 - 10.1007/BF01212304

DO - 10.1007/BF01212304

M3 - Article

VL - 4

SP - 239

EP - 272

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 0934-5043

IS - 3

ER -