Advertisement

Specification and Formal Verification of Temporal Properties of Production Automation Systems

  • Stephan Flake
  • Wolfgang Müller
  • Ulrich Pape
  • Jürgen Ruf
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3147)

Abstract

This article describes our approach for the specification and verification of production automation systems with real-time properties. We focus on the graphical MFERT notation and RT-OCL (Real-Time Object Constraint Language) for the specification of state-oriented real-time properties. RT-OCL is an extension of the Object Constraint Language (OCL) that is part of the Unified Modeling Language (UML). We introduce the formal semantics of RT-OCL based on a formal model of UML Class and State Diagrams and provide a mapping to temporal logics. The applicability of our approach is demonstrated by the case study of a manufacturing system with automated guided vehicles.

Keywords

Model Check Temporal Logic Object Constraint Language Abstract Syntax Temporal Logic Formula 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Baar, T., Hähnle, R.: An Integrated Metamodel for OCL Types. In: France, R., Rumpe, B., Bruel, J.-M., Moreira, A., Whittle, J., Ober, I. (eds.) OOPSLA 2000 Workshop Refactoring the UML: In Search of the Core, Minneapolis, MN, USA (2000)Google Scholar
  2. 2.
    Bradfield, J.C., Küster Filipe, J., Stevens, P.: Enriching OCL Using Observational Mu-Calculus. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 203–217. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Brockmeyer, U., Wittich, G.: Tamagotchis Need Not Die — Verification of STATEMATE Designs. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 217–231. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. 4.
    Burmester, S., Flake, S., Giese, H., Schäfer, W., Tichy, M.: Towards the Compositional Verification of Real-Time UML Designs. In: Inverardi, P., Paakki, J. (eds.) Joint 9th European Software Engineering Conference (ESEC) and 11th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE-11), Helsinki, Finland, September 2003, pp. 38–47. ACM Press, New York (2003)Google Scholar
  5. 5.
    Cengarle, M.V., Knapp, A.: Towards OCL/RT. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 389–408. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Cheng, A.: Petri Nets, Traces, and Local Model Checking. In: Algebraic Methodology and Software Technology, pp. 322–337 (1995)Google Scholar
  7. 7.
    Clark, A., Warmer, J. (eds.): Object Modeling with the OCL. LNCS, vol. 2263. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  9. 9.
    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, USA (2001)Google Scholar
  10. 10.
    Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001)zbMATHCrossRefGoogle Scholar
  11. 11.
    Dangelmaier, W., Warnecke, H.-J.: Fertigungslenkung: Planung und Steuerung des Ablaufs der diskreten Fertigung. Springer, Heidelberg (1997)Google Scholar
  12. 12.
    Dangelmaier, W., Wiedenmann, H.: Modell der Fertigungssteuerung, 1st edn. Beuth Verlag GmbH, Berlin (1993)Google Scholar
  13. 13.
    Distefano, D., Katoen, J.-P., Rensink, A.: On a Temporal Logic for Object-Based Systems. In: Smith, S., Talcott, C. (eds.) Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000), Stanford, CA, USA, September 2000, pp. 305–326. Kluwer Academic Publishers, Dordrecht (2000)Google Scholar
  14. 14.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: 21st International Conference on Software Engineering (ICSE 1999), Los Angeles, CA, USA, May 1999, pp. 411–420. ACM Press, New York (1999)CrossRefGoogle Scholar
  15. 15.
    Feyerabend, K., Josko, B.: A Visual Formalism for Real Time Requirement Specifications. In: Rus, T., Bertrán, M. (eds.) AMAST-ARTS 1997, ARTS 1997, and AMAST-WS 1997. LNCS, vol. 1231, pp. 156–168. Springer, Heidelberg (1997)Google Scholar
  16. 16.
    Flake, S.: Modeling and Verification of Manufacturing Systems: A Domain-Specific Formalization of UML. In: Hamza, M. (ed.) 7th IASTED International Conference on Software Engineering and Applications (SEA 2003), Los Angeles, CA, USA, November 2003, pp. 580–586. ACTA Press, Calgary (2003)Google Scholar
  17. 17.
    Flake, S.: UML-Based Specification of State-oriented Real-time Properties. PhD thesis, Faculty of Computer Science, Electrical Engineering and Mathematics, Paderborn University, Shaker Verlag, Aachen, Germany (December 2003)Google Scholar
  18. 18.
    Flake, S.: Towards the Completion of the Formal Semantics of OCL 2.0. In: Estivill-Castro, V. (ed.) 27th Australasian Computer Science Conference (ACSC 2004), Dunedin, New Zealand, January 2004. Australian Computer Science Communications, vol. 26, pp. 73–82. Australian Computer Science Society, Sydney (2004)Google Scholar
  19. 19.
    Flake, S., Müller, W.: An OCL Extension for Real-Time Constraints. In: Clark and Warmer [7], pp. 150–171Google Scholar
  20. 20.
    Flake, S., Müller, W.: Specification of Real-Time Properties for UML Models. In: Sprague Jr., R. (ed.) 35th Hawaii International Conference on System Sciences (HICSS-35), Big Island, HI, USA, January 2002, IEEE Computer Society Press, Los Alamitos (2002)Google Scholar
  21. 21.
    Flake, S., Müller, W.: Expressing Property Specification Patterns with OCL. In: The 2003 International Conference on Software Engineering Research and Practice (SERP 2003), Las Vegas, NV, USA, June 2003, pp. 595–601. CSREA Press, Las Vegas (2003)Google Scholar
  22. 22.
    Flake, S., Müller, W.: Formal semantics of static and temporal state-oriented OCL constraints. Software and Systems Modeling (SoSyM) 2(3), 164–186 (2003)CrossRefGoogle Scholar
  23. 23.
    Flake, S., Müller, W., Ruf, J.: Structured English for Model Checking Specification. In: Waldschmidt, K., Grimm, C. (eds.) Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Frankfurt/M., Germany, February 2000, pp. 251–262. VDE Verlag, Berlin (2000)Google Scholar
  24. 24.
    Holt, A., Klein, E.: A Semantically-Derived Subset of English for Hardware Verification. In: 37th Annual Meeting of the Association for Computational Linguistics (ACL 1999), University of Maryland, College Park, MD, USA, June 1999, pp. 451–456 (1999)Google Scholar
  25. 25.
    Ivner, A., Högström, J., Johnston, S., Knox, D., Rivett, P.: Response to the UML2.0 OCL RfP, Version 1.6 (Submitters: Boldsoft, Rational, IONA, Adaptive Ltd., et al.). OMG Document ad/03-01-07 (January 2003), ftp://ftp.omg.org/pub/-docs/ad/03-01-07.pdf
  26. 26.
    Janssen, W., Mateescu, R., Mauw, S., Fennema, P., van der Stappen, P.: Model Checking for Managers. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 92–107. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  27. 27.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Springer International Journal of Software Tools for Technology Transfer 1(1+2) (1997)Google Scholar
  28. 28.
    OMG, Object Management Group. UML 2.0 OCL Final Adopted Specification. OMG Document ptc/03-10-14 (October 2003), ftp://ftp.omg.org/pub/docs/ptc/-03-10-14.pdf
  29. 29.
    OMG, Object Management Group. Unified Modeling Language 1.5 Specification. OMG Document formal/03-03-01 (March 2003), ftp://ftp.omg.org/pub/-docs/formal/03-03-01.pdf
  30. 30.
    Ramakrishnan, S., McGregor, J.: Extending OCL to Support Temporal Operators. In: 21st International Conference on Software Engineering (ICSE 1999), Workshop on Testing Distributed Component-Based Systems, Los Angeles, CA, USA (May 1999)Google Scholar
  31. 31.
    Richters, M.: A Precise Approach to Validating UML Models and OCL Constraints. PhD thesis, Universität Bremen, Bremen, Germany, Logos Verlag, Berlin, BISS Monographs, No. 14 (2002)Google Scholar
  32. 32.
    Richters, M., Gogolla, M.: OCL: Syntax, Semantics, and Tools. In: Clark and Warmer [7], pp. 42–68Google Scholar
  33. 33.
    Rosenblum, D.: Formal Methods and Testing: Why State-Of-The-Art is not State- Of-The-Practise. In: ISSTA 1996/FMSP 1996 Panel Summary. ACM SIGSOFT Software Engineering Notes 21(4) (July 1996)Google Scholar
  34. 34.
    Roubtsova, E.E., van Katwijk, J., Toetenel, W., de Rooij, R.C.: Real-Time Systems: Specification of Properties in UML. In: 7th Annual Conference of the Advanced School for Computing and Imaging (ASCI 2001), Het Heijderbos, Heijen, The Netherlands, May/June 2001, pp. 188–195 (2001)Google Scholar
  35. 35.
    Ruf, J.: Techniken zur Modellierung und Verifikation von Echtzeitsystemen. PhD thesis, Universität Karlsruhe, Karlsruhe, Germany (March 2000) (in German)Google Scholar
  36. 36.
    Ruf, J.: RAVEN: Real-Time Analyzing and Verification Environment. Journal on Universal Computer Science (J.UCS) 7(1), 89–104 (2001)zbMATHGoogle Scholar
  37. 37.
    Ruf, J., Kropf, T.: Symbolic Model Checking for a Discrete Clocked Temporal Logic with Intervals. In: Cerny, E., Probst, D. (eds.) Correct Hardware Design and Verification Methods (CHARME 1997), 9th IFIP WG 10.5 Advanced Research Working Conference, Montreal, Canada, October 1997, pp. 146–166. Chapman and Hall, Boca Raton (1997)Google Scholar
  38. 38.
    Ruf, J., Kropf, T.: Modeling and Checking Networks of Communicating Real- Time Systems. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 265–279. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  39. 39.
    Ruf, J., Kropf, T., Weiss, R.: Modeling and Formal Verification of Production Automation Systems. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 541–566. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  40. 40.
    Schneider, U.: Ein formales Modell und eine Klassifikation für die Fertigungssteuerung – Ein Beitrag zur Systematisierung der Fertigungssteuerung. PhD thesis, Heinz Nixdorf Institut, HNI-Verlagsschriftenreihe, Band 16, Paderborn, Germany (1996) (in German)Google Scholar
  41. 41.
    Sendall, S., Strohmeier, A.: Specifying Concurrent System Behavior and Timing Constraints Using OCL and UML. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 391–405. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  42. 42.
    Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Reading (1999)Google Scholar
  43. 43.
    Warmer, J., Kleppe, A.: The Object Constraint Language – Getting Your Models Ready for MDA, 2nd edn. Object Technology Series. Addison-Wesley, Reading (2003)Google Scholar
  44. 44.
    Westkämper, E., Höpf, M., Schaeffer, C.: Holonic Manufacturing Systems (HMS) – Test Case 5. In: Proceedings of Holonic Manufacturing Systems, Lake Tahoe, CA, USA (February 1994)Google Scholar
  45. 45.
    Ziemann, P., Gogolla, M.: An Extension of OCL with Temporal Logic. In: Jürjens, J., Cengarle, M., Fernandez, E., Rumpe, B., Sandner, R. (eds.) Critical Systems Development with UML – Proceedings of the UML 2002 Workshop, Technische Universität München, Institut für Informatik, Munich, Germany, pp. 53–62 (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Stephan Flake
    • 1
  • Wolfgang Müller
    • 1
  • Ulrich Pape
    • 2
  • Jürgen Ruf
    • 3
  1. 1.Universität PaderbornPaderbornGermany
  2. 2.Heinz Nixdorf InstitutPaderbornGermany
  3. 3.IBM Deutschland Entwicklung GmbHBöblingenGermany

Personalised recommendations