Temporal theories as modularisation units for concurrent system specification

Formal Aspects of Computing - 1992
José Luiz Fiadeiro1, Tom Maibaum1
1Department of Computing, Imperial College of Science, Technology and Medicine, London, UK SW7 2BZ#TAB#

Tóm tắt

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.

Từ khóa


Tài liệu tham khảo

Barr M. and Wells C.: Category Theory for Computing Science Prentice-Hall International 1990.

Barringer H.: The Use of Temporal Logic in the Compositional Specification of Concurrent Systems. In Temporal Logics and their Applications A. Galton (ed.) Academic Press 1987.

Barringer H. and Kuiper R.: Hierarchical Development of Concurrent Systems in a Temporal Framework. In Seminar on Concurrency S. Brookes A. Roscoe and G. Winskel (eds) LNCS 197 Springer-Verlag pp. 35–61 1984.

Burstall R. and Goguen J.: Putting Theories Together to Make Specifications. In Proc. Fifth International Joint Conference on Artificial Intelligence R. Reddy (ed.) pp. 1045–1058 1977.

Burstall R. and Goguen J.: An Informal Introduction to Specifications using Clear. In The Correctness Problem in Computer Science R. Boyer and J. Moore (eds) Academic Press pp. 185–213 1981.

Costa J. -F. and Sernadas A.: Process Models within a Categorial Framework Research Report INESC 1991.

deRoever W.: The Quest for Compositionality — a Survey of Assertion-Based Proof Systems for Concurrent Programs. Part 1: Concurrency Based on Shared Variables. In Formal Models in Programming E. Neuhold and G. Chroust (eds) North-Holland pp. 181–205 1985.

Ehrich H.-D. and Sernadas A.: Algebraic View of Implementing Objects over Objects. In Stepwise Refinement of Distributed Systems: Models Formalisms Correctness W. deRoever (ed.) Springer-Verlag 1989.

Ehrich H.-D. Sernadas A. and Sernadas C: From Data Types to Object Types. Journal of Information Processing and Cybernetics (1990).

Ehrig H. and Mahr B.: Fundamentals of Algebraic Specification 1: Equations and Initial Semantics Springer-Verlag 1985.

Enderton H. B.: A Mathematical Introduction to Logic Academic Press 1972.

Fiadeiro J. and Maibaum T.: Towards Object Calculi Research Report Imperial College 1989.

Fiadeiro J. and Maibaum T.: Describing Structuring and Implementing Objects. In Foundations of Object-Oriented Languages J. deBakker W. deRoever and G. Rozenburg (eds) Springer-Verlag 1990.

Fiadeiro J. and Sernadas A.: Structuring Theories on Consequence. In Recent Trends in Data Type Specification D. Sannella and A. Tarlecki (eds) LNCS 332 Springer-Verlag pp. 44–72 1988.

10.1093/logcom/1.2.187

Fiadeiro J. Sernadas C. Maibaum T. and Saake G.: Proof-Theoretic Semantics of Object-Oriented Specification Constructs. In Object-Oriented Databases: Analysis Design and Construction W. Kent S. Khosla and R. Meersman (eds) North-Holland 1990.

Fiadeiro J. Sernadas A. Costa J. -F. and Maibaum T.: (Terminal) Process Semantics of Temporal Logic Specifications Research Report Imperial College 1991.

Gergely T., 1988, Technical Report

10.1109/MC.1986.1663146

Goguen J. A Categorical Manifesto. Technical Report PRG-72 Programming Research Group University of Oxford March 1989.

Goguen J. and Burstall R.: Introducing Institutions. In Proc. Logics of Programming Workshop E. Clarke and D. Kozen (eds) LNCS 164 Springer-Verlag pp. 221–256 1984.

Goguen J. and Ginali S.: A Categorical Approach to General Systems Theory. In Applied General Systems Research G. Klir (ed.) Plenum pp. 257–270 1978.

Hennessy M.: Algebraic Theory of Processes MIT Press 1988.

Hoare C. A. R.: Communicating Sequential Processes Prentice-Hall 1985.

Lamport L.: Specifying Concurrent Program Modules ACM TOPLAS 6 (2) (1983).

Maibaum T.: Rôle of abstraction in program development. In Information Processing '86 H.-J. Kugler (ed.) North-Holland pp. 135–142 1986.

Maibaum T., 1989, Design Structures, private communication

Manna Z. and Pnueli A. Verification of Concurrent Programs: The Temporal Framework. In The Correctness Problem in Computer Science R. Boyer and J. Moore (eds) Academic Press pp. 215–273 1981.

10.1145/355602.361309

Pnueli A.: The Temporal Logic of Programs. In Proc. 18th Annual Symposium on Foundations of Computer Science IEEE 45–57 1977.

Pnueli A.: Specification and Development of Reactive Systems. In Information Processing 86 H.-J. Kugler (ed.) North-Holland pp. 845–858 1986.

Sannella D. and Burstall R.: Structured Theories in LCF. In Proc. 8th Colloquium on Trees in Algebra and Programming G. Ausiello and M. Protasi (eds) LNCS 159 Springer-Verlag pp. 377–391 1983.

Sannella D., 1988, Building Specifications in an Arbitrary Institution, Information and Control, 76, 165

Sernadas A. Sernadas C. and Ehrich H.-D.: Object-Oriented Specification of Databases: An Algebraic Approach. In Proc. 13th VLDB Conference P. Hammersley (ed.) Morgan Kaufmann pp. 107–116 1987.

Sernadas A. Fiadeiro J. Sernadas C. and Ehrich H.-D.: Abstract Object Types: A Temporal Perspective. In Temporal Logic in Specification B. Banieqbal H. Barringer and A. Pnueli (eds) LNCS 398 Springer-Verlag pp. 324–349 1989.

Sernadas A. Fiadeiro J. Sernadas C. and Ehrich H.-D.: The Basic Building Blocks of Information Systems. In Information Systems Concepts: An In-depth Analysis . E. Falkenberg and P. Lindgreen (eds) North-Holland pp. 225–246 1989.

Veloso P. and Pequeno T.: Interpretations between Many-Sorted Theories. Proc. 2nd Brasilian Colloquium on Logic 1978.

Thông tin
Thông tin xuất bản

Formal Aspects of Computing

Thông tin tác giả