Abstract
It is increasingly recognised that non-functional requirements should be considered at the earliest stages of system development. Unified modelling language (UML), as a standard, should therefore include notation to capture such requirements. Among these, timing has received considerable attention by the modelling community with several timed extensions of UML diagrams, a UML profile and tools. However, timing constraints are, generally, not captured in a satisfactory way during design. We propose to use UML's object constraint language (OCL) for this purpose, and provide a simple time enriched liveness template for OCL. We describe the benefits of using this template.
Having verification in mind, several logic-based formalisms could be chosen to underly OCL. We consider a novel real-time logic of knowledge, and argue why logics of knowledge are useful and promising in this context. We illustrate our approach with a distributed real-time system. Future work and further benefits of the knowledge-based framework are discussed at the end of the paper.
Similar content being viewed by others
References
Alur, R.: Timed automata. In: 11th International Conference on Computer-Aided Verification, LNCS, vol. 1633, pp. 8–22. Springer (1999)
Alur, R., Henzinger, T.: Logics and models of real time: A survey. In: de Bakker, J., Huizing, K., de Roever, W.-P., Rozenberg, G. (eds.), Real time: Theory and practice, LNCS, vol. 600, pp. 74–106. Springer (1992)
Benerecetti, M., Spalazzi, L., Tacconi, S.: Verification of the SSL/TLS protocol using a model checkable logic of belief and time. In: Anderson, S., Bologna, S., Felici, M. (eds.), Proceedings of SAFECOMP'02, LNCS, vol. 2434, pp. 126–138. Springer (2002)
Bradfield, J., Küster-Filipe, J., Stevens, P.: Enriching OCL using observational mu-calculus. In: Kutsche, R.-D., Weber, H. (eds.), In: Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE), Grenoble, France, April 2002, LNCS, vol. 2306, pp. 203–217. Springer (2002)
Burns, A., Wellings, A.: Real-time systems: Specification, verification and analysis. In: Advanced Fixed Priority Schedulling, pp. 32–65. Prentice-Hall (1996)
Cengarle, M., Knapp, A.: Towards OCL/RT. In: Eriksson, L.-H., Lindsay, P. (eds.), Formal Methods—Getting IT Right, International Symposium on Formal Methods Europe, LNCS, vol. 2391, pp. 389–408. Springer (2002)
Conrad, S., Turowski, K.: Temporal OCL: Meeting specifications demands for business components. In: Siau, K., Halpin, T. (eds.), Unified Modeling Language: Systems Analysis, Design, and Development Issues, pp. 151–165. IDEA Group Publishing (2001)
Douglass, B.P.: Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison-Wesley, Boston, MA, USA (1999)
Firley, T., Huhn, M., Diethers, K., Gehrke, T., Goltz, U.: Timed sequence diagrams and tool-based analysis—a case study. In: The Second International Conference on The Unified Modeling Language, Beyond the Standard (UML'99), LNCS, vol. 1723, pp. 645–660. Springer (October 1999)
Flake, S., Mueller, W.: An OCL extension for real-time constraints. In: Clark, T., Warmer, J. (eds.), Object Modeling with the OCL, LNCS, vol. 2263, pp. 150–171. Springer (2002)
Flake, S., Mueller, W.: Formal semantics of static and temporal state-oriented OCL constraints. Softw. Syst. Model. 2(3), 164–186 (October 2003)
Graf, S., Ober, I., Ober, Iu.: Timed annotations with UML. In: Proceedings of the International Workshop on Specification and Validation of UML models for Real Time and Embedded Systems (SVERTS 2003) (2003)
Halpern, J.Y., Vardi, M.Y.: The complexity of reasoning about knowledge and time, i: lower bounds. J. Comput. Syst. Sci. 38(1), 195–237 (1989)
Halpern, J.Y.: Reasoning about uncertainty. The MIT Press, Cambridge, Massachusetts, USA (2003)
Harel, D., Marelly, R.: Playing with Time: On the Specification and Execution of Time-Enriched LSCs. In: 10th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS'02) October 11–16, 2002, Fort Worth, Texas, pp. 193–202 (2002)
Harel, D., Marelly, R.: Come, Let's Play: Scenario-based Programming Using LSCs and the Play-Engine. Springer, New York, USA (2003)
Klein, M.H., Ralya, T., Pollack, B., Obenza, R., Harbour, M.G.: A Practitioner's Handbook for Real-Time Analysis. Kluwer Academic Publishers, Norwell, MA, USA (1993)
Kleppe, A., Warmer, J.: Extending OCL to include actions. In: Kent, S., Evans, A. (eds.), UML'2000—The Unified Modeling Language: Advancing the Standard, Third International Conference, York, UK, October 2–6, 2000, volume 1939 of LNCS, pp. 440–450. Springer (2000)
Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: Proceedings of 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, LNCS, vol. 2469, pp. 395–416. Springer (2002)
Küster-Filipe, J., Anderson, S.: Using OCL for expressing temporal validity constraints. In: Proceedings of the International Workshop on Specification and Validation of UML models for Real Time and Embedded Systems (SVERTS 2003) (2003)
Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2):134–152, (1997)
OMG: UML Profile for Modelling Quality of Service and Fault Tolerance Characteristics and Mechanisms, August 2002. Initial submission, available to members at www.omg.org
OMG: UML 2.0 OCL Specification. OMG Adopted Specification, document ad/03-10-14, available at www.uml.org (2003)
OMG: UML 2.0 Superstructure Draft Adopted Specification. OMG document ptc/03-08-02, available at http://www.uml.org (August 2003)
OMG: Unified Modeling Language Specification version 1.5 (March 2003) OMG document available at http://www.omg.org
OMG: UML Profile for Schedulability, Performance and Time, version 1.1, January 2005. OMG document available at http://www.omg.org
Ramakrishnan, S., McGregor, J.: Extending OCL to support temporal operators. In: Ulrich, A. (ed.), ICSE'99 Workshop on Testing Distributed Component-based Systems, Los Angeles, California, USA (May 1999)
Saksena, M.: Real-time systems design: A temporal perspective. In: Proceedings of the IEEE Canadian Conference on Electrical and Computer Engineering (May 1998)
Segala, R., Gawlick, R., Søgaard-Andersen J., Lynch, N.: Liveness in timed and untimed systems. In: Proceedings of ICALP'94, LNCS, vol. 820, pp. 166–177 (1994)
Ziemann, P., Gogolla, M.: An OCL extension for formulating temporal constraints. Technical Report 1/03, Fachbereich Mathematik und Informatik, Universität Bremen, Germany (2003)
Author information
Authors and Affiliations
Corresponding author
Additional information
Work reported here was supported by the EPSRC grants GR/R16891 and GR/N13999.
Rights and permissions
About this article
Cite this article
Küster-Filipe, J., Anderson, S. On a time enriched OCL liveness template. Int J Softw Tools Technol Transfer 8, 156–166 (2006). https://doi.org/10.1007/s10009-005-0210-0
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-005-0210-0