Skip to main content
SpringerLink
Log in

“UML–ising” Formal Techniques

  • Chapter
Integration of Software Specification Techniques for Applications in Engineering

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3147))

Abstract

This invited paper presents a number of correlated specifications of example railway system problems. They use a variety of partially or fully integrated formal specification. The paper thus represents a mere repository of what we consider interesting case studies.

The existence of the Unified Modeling Language [10,67,36,20] has caused, for one reason or another, the research community to try formalise one or another facet of UML. In this paper we report on another way to achieve what UML attempts to achieve: Broadness of application, convenience of notation, and multiplicity of views. Whether these different UML views are unified, integrated, correlated or merely co–located is for others to dispute. We also seek to support multiple views, but are also in no doubt that there must be sound, well defined relations between such views.

We thus report on ways and means of integrating formal techniques such as RAISE (RSL) [58,59], Petri Nets [56,62,37,61,41], Message and Live Sequence Charts [42,43,44,64,13], Statecharts [23,24,26,27], RAISE with Timing (TRSL) [18,45,46], and TRSL with Duration Calculus [79,30]. In this way one achieves a firm foundation for combined uses of these formal development techniques, one that can be believably deployed for as wide a spectrum, or even a wider spectrum of software (and hardware) development, as, respectively than UML.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.-R.: The B Book: Assigning Programs to Meanings. Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  2. Andersen, S., Holmslykke, S.: “UML–ised” Formal Tools for the RAISE Tool Set. M.Sc. Thesis Project, Department of Computer Science and Engineering, Institute of Informatics and Mathematical Modelling, Technical University of Denmark, Building 322, Richard Petersens Plads, DK–2800 Kgs.Lyngby, Denmark, 2004–2005 2003. Pre–MSc Thesis project: Spring 2004 Lyngby; main M.Sc. Thesis Project Fall/Winter 2004/2005 UNU–IIST Macau / NUS Singapore

    Google Scholar 

  3. Anot, A.J.: Using Z Specification for Railway Interlocking Safety. Periodica Polytechnica. Transport Engineering Series vol. 28(1-2), pp. 39–53, Department of Information and Safety Systems Faculty of Electrical Engineering University of Zilina, Vel’ký diel, Zilina 010 26, Slovak Republic (2000)

    Google Scholar 

  4. Berthelot, G., Petrucci, L.: Specification and validation of a concurrent system: an educational project. International Journal on Software Tools for Technology Transfer 3(4), 372–381 (2001); Special section on the practical use of high-level Petri Nets

    MATH  Google Scholar 

  5. Billington, J., Janczura, C.: Removing Deadlock from a Railway Network Specification. In: Australian Engineering Mathematics Conference (AEMC 1996), Sydney, Australia, July 1996, pp. 193–200 (1996) (Australian Engineering Mathematical Society ?)

    Google Scholar 

  6. Bjørner, D.: Formal Software Techniques in Railway Systems. In: Schnieder, E. (ed.) 9th IFAC Symposium on Control in Transportation Systems, Technical University, Braunschweig, Germany, June 13-15, pp. 1–12 (2000), VDI/VDE-Gesellschaft Mess– und Automatisieringstechnik, VDI-Gesellschaft für Fahrzeug– und Verkehrstechnik (invited talk)

    Google Scholar 

  7. Bjørner, D.: Dynamics of Railway Nets: On an Interface between Automatic Control and Software Engineering. In: Tsugawa, S., Aoki, M. (eds.) CTS 2003: 10th IFAC Symposium on Control in Transportation Systems, Oxford, UK, August 4-6, Elsevier Science Ltd, Amsterdam (2003), Symposium held at Tokyo, Japan

    Google Scholar 

  8. Bjørner, D., George, C.W., Prehn, S.: Computing Systems for Railways — A Rôle for Domain Engineering. Relations to Requirements Engineering and Software for Control Applications. In: Kraemer, B., Petterson, J.C. (eds.) Integrated Design and Process Technology, P.O.Box 1299, Grand View, Texas 76050-1299, USA, June 24-28 (2002), Society for Design and Process Science

    Google Scholar 

  9. Bjørner, D., George, C.W., Prehn, S.: Scheduling and Rescheduling of Trains. In: Hinchey, M.G., Bowen, J.P. (eds.) Industrial Strength Formal Methods in Practice, ch. 8, pp. 157–184. Springer, London (1999), FACIT

    Google Scholar 

  10. Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading (1998)

    Google Scholar 

  11. Büssow, R., Geisler, R., Klar, M.: Specifying safety-critical embedded systems with Statecharts and Z: A case study. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 71–87. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. CCITT. CCITT Recommendation Z.120: Message Sequence Chart (MSC) (1992)

    Google Scholar 

  13. Damm, W., Harel, D.: LSCs: Breathing life into Message Sequence Charts. Formal Methods in System Design 19, 45–80 (2001); Early version appeared as Weizmann Institute Tech. Report CS98-09 (April 1998); An abridged version appeared in Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-based Distributed Systems (FMOODS 1999), pp. 293–312. Kluwer, Dordrecht (1999)

    Article  MATH  Google Scholar 

  14. Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. Technical Report TRCF-97-2, Universität Oldenburg (1997)

    Google Scholar 

  15. Fitzgerald, J., Larsen, P.G.: Software System Design: Formal Methods into Practice. Cambridge University Press, The Edinburgh Building (1997) (to appear)

    Google Scholar 

  16. Funes, A., George, C.W.: Formal Foundations in RSL for UML Class Diagrams. Research Report 253, UNU/IIST, P.O. Box 3058, Macau. In: Favre, L. (ed.) Published as chapter VIII Formalizing UML Class Diagrams of UML and the Unified Process (May 2002)

    Google Scholar 

  17. Galloway, A.: Integrated Formal Methods. PhD thesis, University of Teeside (1996)

    Google Scholar 

  18. George, C.W., Xia, Y.: An Operational Semantics for Timed RAISE. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1008–1027. Springer, Heidelberg (1999)

    Google Scholar 

  19. Grieskamp, W., Heiseland, M., Dörr, H.: Specifying embedded systems with Statecharts and Z: An agenda for cyclic software components. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 88–106. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  20. Object Management Group. OMG Unified Modelling Language Specification. OMG/UML, http://www.omg.org/uml/ , version 1.5 edition (March 2003), www.omg.org/cgi-bin/doc?formal/03-03-01

  21. Hansen, K.M.: Validation of a railway interlocking model. In: Naftalin, M., Bertrán, M., Denvir, T. (eds.) FME 1994. LNCS, vol. 873, pp. 582–601. Springer, Heidelberg (1994)

    Google Scholar 

  22. Hansen, K.M.: Linking Safety Analysis to Safety Requirements. PhD thesis, Department of Computer Science, Technical University of Denmark, Building 344, DK-2800 Lyngby, Denmark (August 1996)

    Google Scholar 

  23. Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  24. Harel, D.: On visual formalisms. Communications of the ACM 33(5), 514–530 (1988)

    Article  MathSciNet  Google Scholar 

  25. Harel, D., Gery, E.: Executable object modeling with Statecharts. IEEE Computer 30(7), 31–42 (1997)

    Google Scholar 

  26. Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., Trakhtenbrot, M.B.: STATEMATE: A working environment for the development of complex reactive systems. Software Engineering 16(4), 403–414 (1990)

    Article  Google Scholar 

  27. Harel, D., Naamad, A.: The STATEMATE semantics of Statecharts. ACM Transactions on Software Engineering and Methodology (TOSEM) 5(4), 293–333 (1996)

    Article  Google Scholar 

  28. Haxthausen, A., Gjaldbæk, T.: Modelling and Verification of Interlocking Systems for Railway Lines. In: 10th IFAC Symposium on Control in Transportation Systems, Tokyo, Japan, August 4-6 (2003)

    Google Scholar 

  29. Haxthausen, A.: Some approaches for integration of specification techniques (2000) (invited extended abstract)

    Google Scholar 

  30. Haxthausen, A., Xia, Y.: Linking DC together with TRSL. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 25–44. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  31. Heymans, P., Bontemps, Y.: Turning high-level Live Sequence Charts into automata. In: Systa, T., Zundorf, A. (eds.) Proceedings of the First International Workshop on Scenarios and State Machines (SCESM) (ICSE 2002 workshop) (2002)

    Google Scholar 

  32. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  33. Hoare, C.A.R.: Communicating Sequential Processes. C.A.R. Hoare Series in Computer Science.International. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  34. ITU-T. ITU-T Recommendation Z.120: Message Sequence Chart (MSC) (1996)

    Google Scholar 

  35. ITU-T. ITU-T Recommendation Z.120: Message Sequence Chart (MSC) (1999)

    Google Scholar 

  36. Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Addison-Wesley, Reading (1999)

    Google Scholar 

  37. Jensen, K.: Coloured Petri Nets – Basic Concepts, Analysis Methods and Practical Use, Basic Concepts. EATCS Monographs on Theoretical Computer Science, vol. 1. Springer, Heidelberg (1992)

    Google Scholar 

  38. Kindler, E., Reisig, W., Volzer, H., Walter, R.: Petri net based verification of distributed algorithms: An example. Formal Aspects of Computing 9(4), 409–424 (1997)

    Article  MATH  Google Scholar 

  39. King, T.: Formalising British Rail’s Signalling Rules. In: Naftalin, M., Bertrán, M., Denvir, T. (eds.) FME 1994. LNCS, vol. 873, pp. 45–54. Springer, Heidelberg (1994)

    Google Scholar 

  40. Klose, J., Wittke, H.: An automata based interpretation of Live Sequence Charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 512–527. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  41. Kristensen, L.M., Christensen, S., Jensen, K.: The practitioner’s guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer 2(2), 98–132 (1998)

    Article  MATH  Google Scholar 

  42. Ladkin, P.B., Leue, S.: Analysis of Message Sequence Charts. Technical Report IAM 92-013, Institute for Informatics and Applied Mathematics, University of Berne, Bern, Switzerland (1992)

    Google Scholar 

  43. Ladkin, P.B., Leue, S.: What do Message Sequence Charts mean? In: FORTE, pp. 301–316 (1993)

    Google Scholar 

  44. Ladkin, P.B., Leue, S.: Interpreting Message Flow Graphs. Formal Aspects of Computing 7(5), 473–509 (1995)

    Article  MATH  Google Scholar 

  45. Li, L., He, J.: A denotational semantics of Timed RSL using Duration Calculus. Research Report 168, UNU/IIST, P.O.Box 3058, Macau (1999); Published in Proceedings of The Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA 1999), pp. 492-503. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  46. Li, L., He, J.: Towards a denotational semantics of Timed RSL using Duration Calculus. Research Report 161, UNU/IIST, P.O.Box 3058, Macau (April 1999); Accepted for publication by Chinese Journal of Advanced Software Research

    Google Scholar 

  47. Lindegaard, M.P., Viuf, P., Haxthausen, A.: Modelling Railway Interlocking Systems. In: Proceedings of the 9th IFAC Symposium on Control in Transportation Systems 2000, Braunschweig, Germany, June 13-15, pp. 211–217 (2000)

    Google Scholar 

  48. Madsen, C.K.: Integration of Specification Techniques. M.Sc. Thesis Project, Department of Computer Science and Engineering, Institute of Informatics and Mathematical Modelling, Technical University of Denmark, Building 322, Richard Petersens Plads, DK–2800 Kgs.Lyngby, Denmark, November 30 (2003)

    Google Scholar 

  49. Madsen, C.K.: Study of Graphical and Temporal Specification Techniques. Pre–Thesis Project, Department of Computer Science and Engineering, Institute of Informatics and Mathematical Modelling, Technical University of Denmark, Building 322, Richard Petersens Plads, DK–2800 Kgs.Lyngby, Denmark (June 2003)

    Google Scholar 

  50. Mauw, S., Reniers, M.A.: An algebraic semantics of basic Message Sequence Charts. The Computer Journal 37(4), 269–277 (1994)

    Article  Google Scholar 

  51. Milner, R.: Communication and Concurrency. C.A.R. Hoare Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  52. Morley, M.J.: Modelling British Rail’s Interlocking Logic: Geographic Data Correctness. Technical Report ECS-LFCS-91-186, University of Edinburgh (1991)

    Google Scholar 

  53. Morley, M.J.: Safety in railway signalling data: A behavioural analysis. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 465–474. Springer, Heidelberg (1994)

    Google Scholar 

  54. Morley, M.J.: Safety Assurance in Interlocking Design. PhD thesis, University of Edinburgh (1996)

    Google Scholar 

  55. Morley, M.J.: Safety-level communication in railway interlockings. Science of Computer Programming 29(1-2), 147–170 (1997)

    Article  Google Scholar 

  56. Petri, C.A.: Kommunikation mit Automaten. Bonn: Institut für Instrumentelle Mathematik, Schriften des IIM Nr. 2 (1962)

    Google Scholar 

  57. Pěnička, M., Strupchanska, A.K., Bjørner, D.: Train Maintenance Routing. In: Tarnai, G., Schnieder, E. (eds.) FORMS 2003: Symposium on Formal Methods for Railway Operation and Control Systems, Conf. held at Techn.Univ. of Budapest, Hungary, Germany, L’Harmattan Hongrie, May 15-16 (2003)

    Google Scholar 

  58. RAISE Language Group. The RAISE Specification Language. BCS Practitioner Series. Prentice Hall Int. (1992)

    Google Scholar 

  59. RAISE Method Group. The RAISE Development Method. BCS Practitioner Series. Prentice Hall Int. (1995)

    Google Scholar 

  60. Reggio, G., Repetto, L.: Casl-Chart: A combination of Statecharts and of the algebraic specification language Casl. Technical Report DISI-TR-00-2, DISI, Università di Genova (2000)

    Google Scholar 

  61. Reisig, W.: Elements of Distributed Algorithms: Modelling and Analysis with Petri Nets. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  62. Reisig, W.: A Primer in Petri Net Design. Springer, Heidelberg (1992)

    MATH  Google Scholar 

  63. Reniers, M.: Static semantics of Message Sequence Charts (1995)

    Google Scholar 

  64. Reniers, M.A.: Syntax requirements of Message Sequence Charts. In: Braek, R., Sarma, A. (eds.) Proceedings of the 7th SDL Forum (1995)

    Google Scholar 

  65. Rhode, M.-G.: Semantic Integration of Heterogeneous Software Specifications. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)

    Google Scholar 

  66. Roscoe, A.W.: Theory and Practice of Concurrency. C.A.R. Hoare Series in Computer Science. Prentice-Hall, Englewood Cliffs (1997)

    Google Scholar 

  67. Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley, Reading (1998)

    Google Scholar 

  68. Schneider, S.: Concurrent and Real–time Systems — The CSP Approach, January 2000. Worldwide Series in Computer Science. John Wiley & Sons, Ltd., Baffins Lane (2000)

    Google Scholar 

  69. Simpson, A.C., Woodcock, J.C.P., Davies, J.W.: The mechanical verification of Solid State Interlocking geographic data. In: Groves, L., Reeves, S. (eds.) Proceedings of Formal Methods Pacific, Wellington, New Zealand, July 9-11, pp. 223–242. Springer, Heidelberg (1997)

    Google Scholar 

  70. Spivey, J.M.: Understanding Z: A Specification Language and its Formal Semantics, January 1988. Cambridge Tracts in Theoretical Computer Science, vol. 3. Cambridge University Press, Cambridge (1988)

    MATH  Google Scholar 

  71. Strupchanska, A.K., Pěnička, M., Bjørner, D.: Railway Staff Rostering. In: FORMS 2003: Symposium on Formal Methods for Railway Operation and Control Systems, L’Harmattan Hongrie, May 15-16 (2003)

    Google Scholar 

  72. van der Aalst, W.M.P., Odijk, M.A.: Analysis of railway stations by means of interval timed colored Petri Nets. Real-Time Systems 9(3), 241–263 (1995)

    Article  Google Scholar 

  73. Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML, October 13, p. 144. Addison-Wesley Publ. Co., Reading (1998), ASIN: 0201379406, Paperback

    Google Scholar 

  74. Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA, 2nd edn., p. 240. August 29, Addison-Wesley Publ. Co., Reading (2003) ISBN: 0321179366, Paperback

    Google Scholar 

  75. Weber, M.: Combining Statecharts and Z for the design of safety-critical control systems. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 307–326. Springer, Heidelberg (1996)

    Google Scholar 

  76. Woodcock, J.C.P., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science (1996)

    Google Scholar 

  77. Woodcock, J.C.P., Hughes, A.: Unifying theories of parallel programming. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 24–37. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  78. Yi, W.: A Calculus of Real Time Systems. PhD thesis, Department of Computer Sciences, Chalmers University of Technology, Göteborg, Sweden (1991)

    Google Scholar 

  79. Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real–time Systems. Monographs in Theoretical Computer Science. An EATCS Series–Verlag. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  80. Zhou, C., Hoare, C.A.R., Ravn, A.P.: A Calculus of Durations. Information Proc. Letters 40(5) (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science and Engineering Dept., Informatics and Mathematical Modelling Inst., Technical University of Denmark, DK–2800, Kgs.Lyngby, Denmark

    Dines Bjørner, Anne E. Haxthausen & Steffen Holmslykke

  2. Director ai., UNU/IIST, P.O.Box 3058, Macau SAR, China

    Chris W. George

  3. Rovsing A/S, Dyregårdsvej 2, DK–2740, Skovlunde, Denmark

    Christian Krog Madsen

  4. Faculty of Transportation, Czech Technical University, Na Florenci 25, CZ-11000, Prague 1, The Czech Republic

    Martin Pěnička

Authors
  1. Dines Bjørner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Chris W. George
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Anne E. Haxthausen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Christian Krog Madsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Steffen Holmslykke
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Martin Pěnička
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technische Universität Berlin, Germany

    Hartmut Ehrig

  2. OFFIS e.V., Escherweg 2, 26121, Oldenburg, Germany

    Werner Damm

  3. Department of Applied Computer Science, Catholic University of Eichstätt-Ingolstadt,  

    Jörg Desel

  4. Fraunhofer ISST Berlin, Germany

    Martin Große-Rhode

  5. Lehrstuhl für Softwaretechnik und Programmiersprachen Institut für Informatik, Universität Augsburg, 86135, Augsburg, Germany

    Wolfgang Reif

  6. Institute for Traffic Safety and Automation Engineering, Technical University of Braunschweig, Braunschweig, Germany

    Eckehard Schnieder

  7. Institute of Industrial Manufacturing and Management (IFF), University of Stuttgart, Nobelstrasse 12, D-70569, Stuttgart, Germany

    Engelbert Westkämper

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Bjørner, D., George, C.W., Haxthausen, A.E., Madsen, C.K., Holmslykke, S., Pěnička, M. (2004). “UML–ising” Formal Techniques. In: Ehrig, H., et al. Integration of Software Specification Techniques for Applications in Engineering. Lecture Notes in Computer Science, vol 3147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27863-4_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27863-4_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23135-6

  • Online ISBN: 978-3-540-27863-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation