Abstract
We study a logic adapted for the purpose of specifying component based systems with support for run time reconfiguration. In particular, we analyse some institutional properties of this logic, related to compositional reasoning in specifications.
The logic is an adaptation of the Manna-Pnueli logic, a first-order temporal logic originally proposed to describe reactive systems. We present our variant in detail, and motivate the required extensions by showing how reconfigurable systems can be specified and how reasoning can be carried out in the presence of these properties. Some issues regarding the use of STeP for proof support are discussed.
This work was partially supported by the Engineering and Physical Sciences Research Council of the UK, Grant Nr. GR/N00814.
On leave from Departamento de Computacion, FCEFQyN, Universidad Nacional de Río Cuarto, Río Cuarto, Cordoba, Argentina.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and Z. Manna, Nonclausal Deduction in First-Order Temporal Logic, Journal of the ACM 37(2):279–317, 1990.
N. Aguirre and T. Maibaum, A Temporal Logic Approach to the Specification of Reconfigurable Component-Based Systems, in Proceedings of the 17th International Conference Automated Software Engineering ASE 2002, Edinburgh, United Kingdom, IEEE Press, 2002.
N. Aguirre and T. Maibaum, A Logical Basis for the Specification of Reconfigurable Component-Based Systems, in Proceedings of Fundamental Approaches to Software Engineering FASE 2003, Warsaw, Poland, LNCS 2621, Springer, 2003.
R. Allen and D. Garlan, Formalizing Architectural Connection, in Proceedings ICSE’ 94, Sorrento, Italy, 1994.
M. Barr and C. Wells, Category Theory for Computing Science, Third Edition, Les Publications CRM, 1999.
N. Bjorner, A. Browne, M. Colon, B. Finkbeiner, Z. Manna, H. Sipma and T. Uribe, Verifying Temporal Properties of Reactive Systems: a STeP Tutorial, in Formal Methods in System Design, vol 16, 2000.
H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science, Springer, Berlin, 1985.
J. Fiadeiro, On the Emergence of Properties in Component-Based Systems, in Proceedings of AMAST’96, M. Wirsing and M. Nivat (eds), LNCS 1101, Springer-Verlag, 1996.
J. Fiadeiro and T. Maibaum, Temporal Theories as Modularisation Units for Concurrent System Specification. Formal Aspects of Computing, vol. 4, No. 3, Springer-Verlag, 1992.
J. Fiadeiro and A. Sernadas, Structuring Theories on Consequence, in D. Sannella and A. Tarlecki (eds), Recent Trends in Data Type Specification, LNCS 332, Springer-Verlag, 1988.
D. Garlan, Software Architecture: A Roadmap, in The Future of Software Engineering, A. Filkenstein (ed), ACM Press, 2000.
D. Garlan, R. Monroe and D Wile, ACME: An Architecture Description Interchange Language, in Proc. of CASCON’97, 1997.
J. Goguen and R. Burstall, Institutions: Abstract Model Theory for Specification and Programming, Journal of the ACM 39(1):95–146, ACM Press, 1992.
P. Inverardi and A. Wolf, Formal Specification and Analysis of Software Archite-tures using the Chemical Abstract Machine, IEEE Transactions in Software Engineering, 1995.
Z. Manna and A. Pnueli, Verification of Concurrent Programs: A Temporal Proof System, Technical Report No. STAN-G-83-967, Department of Computer Science, Stanford University, 1983.
Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, 1991.
Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems — Safety —, Springer, 1995.
N. Medvidovic, ADLs and Dynamic Architecture Changes, in Proceedings of the Second Int. Software Architecture Workshop (ISAW-2), 1996.
N. Medvidovic and R. Taylor, A Framework for Classifying and Comparing Architecture Description Languages, In ESEC-FSE’97, 1997.
B. Meyer, Object-Oriented Software Construction, Second Edition, Prentice-Hall International, 2000.
J. Ostroff, Temporal Logic for Real-Time Systems, Advanced Software Development Series, Research Studies Press Ltd, John Wiley and Sons, 1989.
D. Parnas, A Technique for Software Module Specification with Examples, in Communications of the ACM, 15(5), 1972.
D. Parnas, On the Criteria to be Used in Decomposing Systems into Modules, in Communications of the ACM, 15(12), 1972.
M. Wermelinger, A. Lopes and J. Fiadeiro, A Graph Based Architectural (Re)configuration Language, in ESEC/FSE’01, V. Gruhn (ed), ACM Press, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Aguirre, N., Maibaum, T. (2003). Some Institutional Requirements for Temporal Reasoning on Dynamic Reconfiguration of Component Based Systems. In: Dershowitz, N. (eds) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39910-0_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-39910-0_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21002-3
Online ISBN: 978-3-540-39910-0
eBook Packages: Springer Book Archive