Abstract
This paper presents a logic, called BOTL (Object-Based Temporal Logic), that facilitates the specification of dynamic and static properties of object-based systems. The logic is based on the branching temporal logic CTL and the Object Constraint Language (OCL), an optional part of the UML standard for expressing static properties over class diagrams The formal semantics of BOIL is defined in terms of a general operational model that is aimed to be applicable to a wide range of object-oriented languages. A mapping of a large fragment of OCL onto BOTL is defined, thus providing a formal semantics to OCL.
Chapter PDF
References
M. Abadi and K.R.M. Leino. A logic of object-oriented programs. In Theory and Practice of Software Development (TAPSOFT), LNCS 1214, pp. 682–696, 1997.
D.S. Andersen, L.H. Pedersen, H. Hüttel and J. Kleist. Objects, types and modal logics. In Foundations of Object-Oriented Languages (FOOL), 1997.
J.-P. Bahsoun, R. El-Baida, and H.-O. Yar. Decision procedure for temporal logic of concurrent objects. In EuroPar’99, LNCS 1685, pp. 13441352, Springer, 1999.
F.S. de Boer. A proof system for the parallel object-oriented language POOL. In Automata, Languages, and Programming (ICALP), LNCS 443, pp. 572–585, Springer 1990.
G. Booch, J. Rumbaugh, and I. Jacobson. The Unified Modeling Language User Guide. Addison-Wesley, 1998.
E.M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs, LNCS 131, pp. 52–71, Springer, 1981.
E.M. Clarke and R. Kurshan. Computer-aided verification. IEEE Spectrum, 33 (6): 61–67, 1996.
E.M. Clarke, O. Grumberg and D. Peled. Model Checking. MIT Press, 1999.
M. Gogolla and M. Richters. On constraints and queries in UML. In The Unified Modeling Language — Technical Aspects and Applications, Physica-Verlag, 1998.
A. Hamie, F. Civello, J. Howse, S. Kent, and R. Mitchell. Reflections on the Object Constraint Language. In The Unified Modeling Language (UML), LNCS, pp. 137–145, Springer, 1998.
A. Hamie, J. Howse, and S. Kent. Interpreting the Object Constraint Language. In Asia Pacific Software Engineering Conference, pp. 288295. IEEE CS Press, 1998.
S.J. Hodges and C. B. Jones. Non-interference properties of a concurrent object-based language: Proofs based on an operational semantics. In Object Orientation with Parallelism and Persistence, pp. 1–22, Kluwer, 1996.
K. Huizing and R. Kuiper and SOOP. Verification of object-oriented programs using class invariants. In Fundamental Approaches to Software Eng. (FASE), LNCS 1783, Springer 2000.
R. Jungclaus, G. Saake, T. Hartmann, and C. Sernadas. TROLL–a language for object-oriented specification of information systems. ACM Trans. on Inf. Sys., 14 (2): 175–211, 1996.
L. Mandel and M. V. Cengarle. On the expressive power of the Object Constraint Language OCL. Technical report, Forschungsinstitut für angewandte Software-Technologie (FAST e.V. ), 1999.
B. Meyer. Eiffel: The Language. Prentice Hall, 1992.
Rational Software Corporation. Object Constraint Language Specification, version 1.1, 1997. (available from www.rational.com/um1).
A. Poetzsch-Heffter and P. Müller. Logical foundations for typed object-oriented languages. In Programming Concepts and Methods (PRO-COMET), pp. 404–424, Kluwer, 1998.
M. Richters and M. Gogolla. On formalizing the UML object constraint language OCL. In Conceptual Modeling (ER’98), LNCS 1507, pp. 449464, Springer, 1998.
J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modeling Language Reference Guide. Addison-Wesley, 1998.
A. Sernadas, C. Sernadas, and J.F. Costa. Object specification logic. J. of Logic and Computation, 5 (5): 603–630, 1995.
J. Wanner and A. Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, 1998.
J. Warmer and A. Kleppe. OCL: The constraint language of the UML. J. of Obj.-Or. Progr., 12(1):10–13and28, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 IFIP International Federation for Information Processing
About this paper
Cite this paper
Distefano, D., Katoen, JP., Rensink, A. (2000). On a Temporal Logic for Object-Based Systems. In: Smith, S.F., Talcott, C.L. (eds) Formal Methods for Open Object-Based Distributed Systems IV. FMOODS 2000. IFIP Advances in Information and Communication Technology, vol 49. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35520-7_16
Download citation
DOI: https://doi.org/10.1007/978-0-387-35520-7_16
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-1018-2
Online ISBN: 978-0-387-35520-7
eBook Packages: Springer Book Archive