Software and System Modeling Based on a Unified Formal Semantics

  • Manfred Broy
  • Franz Huber
  • Barbara Paech
  • Bernhard Rumpe
  • Katharina Spies
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1526)


Modeling and documentation are two essential ingredients for the engineering discipline of software development. During the last twenty years a wide variety of description and modeling techniques as well as document formats has been proposed. However, often these are not integrated into a coherent methodology with well-defined dependencies between the models and documentations. This hampers focused software development as well as the provision of powerful tool-support. In this paper we present the main issues and outline solutions in the direction of a unified, formal basis for software and system modeling.


Formal Semantic Output Channel Development Step Description Technique External View 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. BBB+85.
    Bauer, F.L., Berghammer, R., Broy, M., Dosch, W., Geiselbrechtinger, F., Gnatz, R., Hangel, E., Hesse, W., Krieg-Brückner, B., Laut, A., Matzner, T., Möller, B., Nickl, F., Partsch, H., Pepper, P., Samelson, K., Wirsing, M., Wössner, H. (eds.): The Munich Project CIP. LNCS, vol. 183. Springer, Heidelberg (1985)zbMATHGoogle Scholar
  2. BBC+96.
    Bjørner, N., Browne, A., Chang, E., Colón, M., Kapur, A., Manna, Z., Sipma, H.B., Uribe, T.E.: STeP: Deductive Algorithmic Verification of Reactive and Real-Time Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)Google Scholar
  3. BBSS97.
    Broy, M., Breitling, M., Scätz, B., Spies, K.: Summary of Case Studies in Focus - Part II. SFB-Bericht 342/24/97 A, Technische Universität München (September 1997)Google Scholar
  4. BCR94.
    Basili, V.R., Caldiera, G., Rombach, H.-D.: Goal Question Metric Paradigm. In: Marciniak, J.J. (ed.) Encyclopedia of Software Engineering, pp. 528–532. John Wiley & Sons, Chichester (1994)Google Scholar
  5. BDD+93.
    Broy, M., Dederichs, F., Dendorfer, C., Fuchs, M., Gritzner, T.F., We-ber, R.: The Design of Distributed Systems - An Introduction to Focus. SFB-Bericht Nr. 342/2-2/92 A, Technische Universität München (January 1993)Google Scholar
  6. BFG+93a.
    Broy, M., Facchi, C., Grosu, R., Hettler, R., Huβmann, H., Nazareth, D., Regensburger, F., Slotosch, O., Stølen, K.: The Requirement and Design Specification Language SPECTRUM, An Informal Introduction, Version 1.0, Part 1. Technical Report TUM-I9312, Technische Universität München (1993)Google Scholar
  7. BFG+94.
    Broy, M., Facchi, C., Grosu, R., Hettler, R., Huβmann, H., Nazareth, D., Regensburger, F., Slotosch, O., Stølen, K.: The Requirement and Design Specification Language Spectrum, An Informal Introduction, Version 1.0, Part 2. Technical Report TUM-I9312, Technische Universität München (1993)Google Scholar
  8. BFG+94.
    Broy, M., Fuchs, M., Gritzner, T.F., Schätz, B., Spies, K., Stølen, K.: Summary of Case Studies in Focus — a Design Method for Distributed Systems. SFB-Bericht 342/13/94 A, Technische Universität München (June 1994)Google Scholar
  9. BGH+97a.
    Breu, R., Grosu, R., Hofmann, C., Huber, F., Krüger, I., Rumpe, B., Schmidt, M., Schwerin, W.: Exemplary and Complete Object Interaction Descriptions. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Proceedings OOPSLA 1997 Workshop on Object-oriented Behavioral Semantics, TUM-I9737 (1997)Google Scholar
  10. BGH+97b.
    Breu, R., Grosu, R., Huber, F., Rumpe, B., Schwerin, W.: Towards a Precise Semantics for Object-Oriented Modeling Techniques. In: Bosch, J., Mitchell, S. (eds.) ECOOP 1997. LNCS, vol. 1357, p. 205. Springer, Heidelberg (1998)Google Scholar
  11. BHH+97.
    Breu, R., Hinkel, U., Hofmann, C., Klein, C., Paech, B., Rumpe, B., Thurner, V.: Towards a Formalization of the Uniied Modeling Language. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 344–366. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  12. BHKS97.
    Broy, M., Hofmann, C., Krueger, I., Schmidt, M.: Using Extended Event Traces to Describe Communication in Software Architectures. In: Proceedings APSEC 1997 and ICSC 1997. IEEE Computer Society, Los Alamitos (1997)Google Scholar
  13. BHS96.
    Broy, M., Huβmann, H., Schätz, B.: Formal Development of Consistent System Specifications. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 248–267. Springer, Heidelberg (1996)Google Scholar
  14. Bie97.
    Biere, A.: Effiziente Modellprüfung des μ-Kalküls mit binären Entscheidungsdiagrammen. PhD thesis, Universität Karlsruhe (1997)Google Scholar
  15. BMS96a.
    Broy, M., Merz, S., Spies, K. (eds.): Dagstuhl Seminar 1994. LNCS, vol. 1169. Springer, Heidelberg (1996)Google Scholar
  16. BMS96b.
    Broy, M., Merz, S., Spies, K.: The RPC-Memory Speciication Problem: A Synopsis. In: [BMS96a], pp. 5–20 (1996)Google Scholar
  17. Bre97.
    Breitling, M.: Formalizing and Verifying TimeWarp with Focus. SFB- Bericht 342/27/97 A, Technische Universität München (1997)Google Scholar
  18. BRJ97.
    Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language for Object-Oriented Development, Version 1.1 (1997)Google Scholar
  19. Bro94.
    Broy, M.: A Functional Rephrasing of the Assumption/Commitment Specification Style. Technical Report TUM-I9417, Technische Universität München (1994)Google Scholar
  20. BS97.
    Broy, M., Stølen, K.: FOCUS on System Development - A Method for the Development of Interactive Systems (1997) ManuscriptGoogle Scholar
  21. CAB+94.
    Coleman, D., Arnold, P., Bodoff, S., Dollin, C., Gilchrist, H., Hayes, F., Jeremaes, P.: Object-Oriented Development - The FUSION Method. Prentice Hall, Englewood Cliffs (1994)Google Scholar
  22. CGR93.
    Craigen, D., Gerhart, S., Ralston, T.: Formal Methods Reality Check: Industrial Usage. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670, pp. 250–267. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  23. DCC92.
    Downs, E., Clare, P., Coe, I.: Structured Systems Analysis and Design Method: Application and Context. Prentice-Hall, Englewood Cliffs (1992)Google Scholar
  24. DHP+98.
    Deifel, B., Hinkel, U., Paech, B., Scholz, P., Thurner, V.: Die Praxis der Softwareentwicklung: Eine Erhebung (1998) (Submitted to publication)Google Scholar
  25. FB97.
    France, R.B., Bruel, J.-M.: Integrated Informal Object-Oriented and Formal Modeling Techniques. In: Kilov, H., Rumpe, B. (eds.) Proceedings ECOOP 1997 Workshop on Precise Semantics for Object-Oriented Modeling Techniques, Technische Universität München, TUM-I9725 (1997)Google Scholar
  26. GJS96.
    Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)zbMATHGoogle Scholar
  27. GKR96.
    Grosu, R., Klein, C., Rumpe, B.: Enhancing the SysLab System Model with State. TUM-I 9631, Technische Universität München (1996)Google Scholar
  28. GKRB96.
    Grosu, R., Klein, C., Rumpe, B., Broy, M.: State Transition Diagrams. TUM-I 9630,Technische Universität München (1996)Google Scholar
  29. GR95.
    Grosu, R., Rumpe, B.: Concurrent Timed Port Automata. TUM-I 9533, Technische Universität München (1995)Google Scholar
  30. HMS+98.
    Huber, F., Molterer, S., Schätz, B., Sltosch, O., Vilbig, A.: Traffic Lights - An AutoFocus Case Study. In: International Conference on Application of Concurrency to System Design. IEEE CS Press, Los Alamitos (1998)Google Scholar
  31. HPSS87.
    Harel, D., Pnueli, A., Schmidt, J.P., Sherman, R.: On the Formal Semantics of Statecharts. In: Proceedings on the Symposium on Logic in Computer Science, pp. 54–64 (1987)Google Scholar
  32. HS97.
    Huber, F., Schätz, B.: Rapid Prototyping with AutoFocus. In: Wolisz, A., Schieferdecker, I., Rennoch, A. (eds.) Formale Beschreibungstech-niken für verteilte Systeme, GI/ITG Fachgespräch 1997, pp. 343–352. GMD Verlag, St. Augustin (1997)Google Scholar
  33. HSS96.
    Huber, F., Schätz, B., Spies, K.: AutoFocus - Ein Werkzeugkonzept zur Beschreibung verteilter Systeme. In: Herzog, U., Hermanns, H. (eds.) Formale Beschreibungstechniken für verteilte Systeme, pp. 165–174, Universität Erlangen-Nürnberg (1996); Arbeitsberichte des Insituts für mathematische Maschinen und Datenverarbeitung, Bd.29, Nr. 9.Google Scholar
  34. Huβ97.
    Huβmann, H. (ed.): Formal Foundations for Software Engineering Methods. LNCS, vol. 1322. Springer, Heidelberg (1997)Google Scholar
  35. Ilo90.
    i-Logix Inc., 22 Third Avenue, Burlington, Mass. 01803, U.S.A. Languages of Statemate (1990)Google Scholar
  36. Int96.
    International Telecommunication Union, Geneva. Message Sequence Charts, ITU-T Recommendation Z.120 (1996)Google Scholar
  37. Jac92.
    Jacobson, I.: Object-Oriented Software Engineering. Addison-Wesley, Reading (1992)zbMATHGoogle Scholar
  38. Jac95.
    Jackson, M.: The World and the Machine. In: ICSE-17, pp. 283–294 (1995)Google Scholar
  39. Jon93.
    Jones, M.P.: An Introduction to Gofer, Manual (1993)Google Scholar
  40. KRB96.
    Klein, C., Rumpe, B., Broy, M.: A Stream-based Mathematical Model for Distributed Information Processing Systems - SysLab system model. In: Naijm, E., Stefani, J.-B. (eds.) FMOODS 1996 Formal Methods for Open Object-based Distributed Systems, pp. 323–338 (1996); ENST France Telecom (1996)Google Scholar
  41. NRS96.
    Nazareth, D., Regensburger, F., Scholz, P.: Mini-Statecharts: A Lean Version of Statecharts. Technical Report TUM-I9610, Technische Universität München (1996)Google Scholar
  42. ORS92.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Veriication System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)Google Scholar
  43. Pau94.
    Paulson, L.C.: Isabelle: A generic theorem prover. LNCS, vol. 828. Springer, Heidelberg (1994)zbMATHCrossRefGoogle Scholar
  44. PR94.
    Paech, B., Rumpe, B.: A New Concept of Reinement Used or Behaviour Modelling with Automata. In: Naftalin, M., Bertrán, M., Denvir, T. (eds.) FME 1994. LNCS, vol. 873. Springer, Heidelberg (1994)Google Scholar
  45. PR97a.
    Paech, B., Rumpe, B.: State Based Service Description. In: Derrick, J. (ed.) Formal Methods for Open Object-based Distributed Systems. Chapman-Hall, Boca Raton (1997)Google Scholar
  46. PR97b.
    Philipps, J., Rumpe, B.: Reinement of Information Flow Architectures. In: Hinchey, M. (ed.) ICFEM 1997 Proceedings, Hiroshima, Japan. IEEE CS Press, Los Alamitos (1997)Google Scholar
  47. PR97c.
    Philipps, J., Rumpe, B.: Stepwise Reinement of Data Flow Architectures. In: Broy, M., Denert, E., Renzel, K., Schmidt, M. (eds.): Software Architectures and Design Patterns in Business Applications. Technische Universität München, TUM-I9746 (1997)Google Scholar
  48. RBP+91.
    Rumbaugh, J., Blaha, M., Premerlani, W., Eddy, F., Lorensen, W.: Object-oriented Modeling and Design. Prentice-Hall, Englewood Cliffs (1991)Google Scholar
  49. Reg94.
    Regensburger, F.: HOLCF: Eine konservative Erweiterung von HOL um LCF. PhD thesis, Technische Universität München (1994)Google Scholar
  50. RK96.
    Rumpe, B., Klein, C.: Automata Describing Object Behavior, pp. 265–287. Kluwer Academic Publishers, Norwell (1996)Google Scholar
  51. Rum96.
    Rumpe, B.: Formal Method for the Development of Distributed Object- Oriented Systems. Herbert Utz Verlag Wissenschaft, PhD thesis, Technische Universität München (1996) (in German)Google Scholar
  52. SDW95.
    Stølen, K., Dederichs, F., Weber, R.: Specification and Refinement of Networks of Asynchronously Communicating Agents using the Assumption/Commitment Paradigm. Formal Aspects of Computing (1995)Google Scholar
  53. SGW94.
    Selic, B., Gulkeson, G., Ward, P.: Real-Time Object-Oriented Modeling. John Wiley and Sons, Chichester (1994)zbMATHGoogle Scholar
  54. Spi94.
    Spies, K.: Funktionale Spezifikation eines Kommunikationsprotokolls. SFB-Bericht 342/08/94 A, Technische Universität Müchen (May 1994)Google Scholar
  55. Spi98.
    Spies, K.: Eine Methode zur formalen Modellierung von Betriebssys-temkonzepten. PhD thesis, Technische Universität Müchen (1998)Google Scholar
  56. Suc95.
    Suchman, L. (ed.): Special Issue on Representations of Work. In: CACM, vol. 38(9) (1995)Google Scholar
  57. Tur93.
    Turner., K.J. (ed.): Using Formal Description Techniques - An Introduction to ESTELLE, LOTOS and SDL. John Wiley & Sons, Chichester (1993)Google Scholar
  58. Wor92.
    Wordsworth, J.B.: Software Development with Z. Addison-Wesley, Reading (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Manfred Broy
    • 1
  • Franz Huber
    • 1
  • Barbara Paech
    • 1
  • Bernhard Rumpe
    • 1
  • Katharina Spies
    • 1
  1. 1.Fakultät für InformatikTechnische Universität München 

Personalised recommendations