Abstract
This paper concerns the problem of building reactive systems in a modular way.
Several institutions have been proposed for the specification of reactive systems throughout the last fifteen years. Based on the institutions, formalisms for the incremental construction of system specifications have been developed. Related problem of modular construction of system implementations has received less attention. This paper is the first attempt to use architectural specifications of Casl for that purpose. The semantics of the architectural specifications is based on the underlying institution. We argue that none of the institutions defined so far for reactive systems is appropriate as a basis for architectural specifications, and therefore we propose another one, better suited for this task.
We also show how to express synchronisation of reactive systems using implementation-building operations of Casl architectural specifications.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This research was sponsored by the EC 5th Framework project AGILE: Architectures for Mobility (IST-2001-32747).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Arrais, M., Fiadeiro, J.L.: Unifying Theories in Different Institutions. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 81–101. Springer, Heidelberg (1996)
Astesiano, E., Zucca, E.: D-oids: a Model for Dynamic Data-Types. Mathematical Structures in Computer Science 5(2), 257–282 (1995)
Baumeister, H., Zamulin, A.: State-Based Extension of Casl. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 3–24. Springer, Heidelberg (2000)
Bidoit, M., Sannella, D., Tarlecki, A.: Architectural specifications in CASL. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 341–357. Springer, Heidelberg (1998)
Cengarle, M.V.: The Temporal Logic Institution, Technical Report 9805, Ludwig-Maximilians-Universität München (1998)
The Common Framework Initiative (CoFI); Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004)
Costa, G., Reggio, G.: Specification of Abstract Dynamic Data Types: A Temporal Logic Approach. Theoretical Computer Science 173(2), 513–554 (1997)
Diaconescu, D., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST series in Computing, vol. 6. World Scientific, Singapore (1998)
Fiadeiro, J.L., Lòpes, A., Wermelinger, M.: A Mathematical Semantics for Architectural Connectors. In: Backhouse, R., Gibbons, J. (eds.) Generic Programming. LNCS, vol. 2793, pp. 190–234. Springer, Heidelberg (2003)
Fiadeiro, J.L., Maibaum, T.: Temporal Theories as Modularisation Units for Concurrent System Specification. Formal Aspects of Computing 4(3), 239–272 (1992)
Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.): Handbook of Logic in Artificial Intelligence and Logic Programming: Epistemic and Temporal Reasoning, vol. 4. Oxford University Press, Oxford (1995)
Goguen, J., Burstall, R.: Institutions: Abstract Model Theory for Specification and Programming. Journal of the ACM 39(1), 95–146 (1992)
Nielsen, M., Winskel, G.: Models for Concurrency. In: Chapter in the Handbook of Logic and the Foundations of Computer Science, vol. 4, pp. 1–148. Oxford University Press, Oxford (1995)
Reggio, G.: Entities: An Instituiton for Dynamic Systems. In: Orejas, F., Ehrig, H., Jantke, K.P., Reichel, H. (eds.) Abstract Data Types 1990. LNCS, vol. 534, pp. 246–265. Springer, Heidelberg (1991)
Reggio, G., Astesiano, E., Choppy, C.: Casl -LTL: A Casl Extension for Dynamic Reactive Systems — Summary. Technical Report DISI-TR-99-34, DISI — Unievrsità di Genova (1999)
Sannella, D., Tarlecki, A.: Building specifications in an arbitrary institution. In: Plotkin, G., MacQueen, D.B., Kahn, G. (eds.) Semantics of Data Types 1984. LNCS, vol. 173, pp. 337–356. Springer, Heidelberg (1984)
Sernadas, A., Sernadas, C., Caleiro, C.: Denotational Semantics of Object Specification. Acta Informatica 35(9), 729–773 (1998)
Tarlecki, A.: Institutions: An Abstract Framework for Formal Specifications. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) Algebraic Foundations of System Specification, ch. 4. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zawłocki, A. (2005). Architectural Specifications for Reactive Systems. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds) Recent Trends in Algebraic Development Techniques. WADT 2004. Lecture Notes in Computer Science, vol 3423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31959-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-31959-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25327-3
Online ISBN: 978-3-540-31959-7
eBook Packages: Computer ScienceComputer Science (R0)