A formal approach to object-oriented software engineering. (English) Zbl 1001.68024
Summary: We show how formal specifications can be integrated into one of the current pragmatic object-oriented software development methods. Jacobson’s “object-oriented software engineering” process is combined with object-oriented algebraic specifications by extending object and interaction diagrams with formal annotations. The specifications are based on Meseguer’s rewriting logic and are written in a meta-level extension of the language Maude by process expressions. As a result any such diagram can be associated with a formal specification, proof obligations ensuring invariant properties can be automatically generated, and the refinement relations between documents at different abstraction levels can be formally stated and proved.
MSC:
| 68N19 | Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) |
| 68Q42 | Grammars and rewriting systems |
Keywords:
integrated formal software engineering; OOSE; rewriting logic; Maude; reflection; process algebraSoftware:
MaudeReferences:
| [1] | Achatz, K.; Schulte, W., A formal OO method inspired by Fusion and Object-Z, (Bowen, J. P.; Hinchey, M. G.; Till, D., Proc. 10th Internat. Conf. on Z Users, Lecture Notes in Computer Science, Vol. 1212 (1997), Springer: Springer Berlin), 92-111 |
| [2] | Astesiano, E.; Cerioli, M.; Reggio, G., Plugging data constructs into paradigm-specific languagestowards an application to UML, (Rus, T., Proc. 8th Internat. Conf. on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, Vol. 1816 (2000), Springer: Springer Berlin), 273-292 · Zbl 0983.68524 |
| [3] | Astesiano, E.; Mascari, G.; Reggio, G.; Wirsing, M., On the parameterized algebraic specification of concurrent processes, (Ehrig, H.; Floyd, C.; Nivat, M.; Thatcher, J. W., TAPSOFT’85, Vol. 1, Lecture Notes in Computer Science, Vol. 185 (1985), Springer: Springer Berlin), 342-358 · Zbl 0563.68018 |
| [4] | Baeten, J. C.M.; Weijland, W. P., Process Algebra (1990), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0716.68002 |
| [5] | Bergstra, J. A.; Klop, J. W., Algebra of communicating processes with abstraction, Theoret. Comput. Sci., 37, 77-121 (1985) · Zbl 0579.68016 |
| [6] | Booch, G., Object-Oriented Analysis and Design: With Applications (1999), Addison-Wesley: Addison-Wesley Reading, MA |
| [7] | Borovansky, P.; Kirchner, C.; Kirchner, H.; Moreau, P.-E.; Vittek, M., ELANa logical framework based on computational systems, (Meseguer, J., Proc. 1st Internat. Workshop on Rewriting Logic and Its Applications, Electronic Notes in Theoretical Computer Science, Vol. 4 (1996), Elsevier: Elsevier Amsterdam), 35-50 · Zbl 0912.68091 |
| [8] | E. Brinksma (Ed.), LOTOS: a formal description technique based on the temporal ordering of observational behaviour, Technical Report Dis 8807, ISO, 1987.; E. Brinksma (Ed.), LOTOS: a formal description technique based on the temporal ordering of observational behaviour, Technical Report Dis 8807, ISO, 1987. |
| [9] | M. Clavel, Reflection in general logics and in rewriting logic with applications to the Maude language, Ph.D. Thesis, Universidad de Navarra, 1998.; M. Clavel, Reflection in general logics and in rewriting logic with applications to the Maude language, Ph.D. Thesis, Universidad de Navarra, 1998. |
| [10] | M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martı́-Oliet, J. Meseguer, J. Quesada, Maude: Specification and Programming in Rewriting Logic. Manual, Computer Science Laboratory, SRI, 1999. http://maude.csl.sri.com/manual; M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martı́-Oliet, J. Meseguer, J. Quesada, Maude: Specification and Programming in Rewriting Logic. Manual, Computer Science Laboratory, SRI, 1999. http://maude.csl.sri.com/manual |
| [11] | M. Clavel, J. Meseguer, Internal strategies in a reflective logic, in: B. Gramlich, H. Kirchner (Eds.), Proc. CADE 14 Workshop on Strategies in Automated Deduction, Townsville, 1997, pp. 1-12.; M. Clavel, J. Meseguer, Internal strategies in a reflective logic, in: B. Gramlich, H. Kirchner (Eds.), Proc. CADE 14 Workshop on Strategies in Automated Deduction, Townsville, 1997, pp. 1-12. |
| [12] | Coleman, D.; Arnold, P.; Bodoff, S.; Dollin, C.; Gilchrist, H.; Hayes, F.; Jeremaes, P., Object-Oriented Development — The Fusion Method (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ |
| [13] | Cook, S.; Daniels, J., Designing Object Systems — Object-Oriented Modelling With Syntropy (1994), Prentice-Hall: Prentice-Hall New York · Zbl 0841.68029 |
| [14] | M. Dodani, R. Rupp, Integrating formal methods with object-oriented methodologies, in: M. Wirsing (Ed.), ICSE-17 Workshop on Formal Methods Applications in Software Engineering Practice, Seattle, 1995, pp. 212-219.; M. Dodani, R. Rupp, Integrating formal methods with object-oriented methodologies, in: M. Wirsing (Ed.), ICSE-17 Workshop on Formal Methods Applications in Software Engineering Practice, Seattle, 1995, pp. 212-219. |
| [15] | F. Durán, A reflective module algebra with applications to the Maude language, Ph.D. Thesis, Universidad de Málaga, 1999.; F. Durán, A reflective module algebra with applications to the Maude language, Ph.D. Thesis, Universidad de Málaga, 1999. |
| [16] | Ehrich, H.-D.; Gogolla, M.; Sernadas, A., Objects and their specification, (Bidoit, M.; Choppy, C., Recent Trends in Data Type Specification, Lecture Notes in Computer Science, Vol. 655 (1993), Springer: Springer Berlin), 40-65 |
| [17] | R.B. France, B. Rumpe (Eds.), Proc. 2nd Internat. Conf. on UML, Lecture Notes in Computer Science, Vol. 1723, Springer, Berlin, 1999.; R.B. France, B. Rumpe (Eds.), Proc. 2nd Internat. Conf. on UML, Lecture Notes in Computer Science, Vol. 1723, Springer, Berlin, 1999. |
| [18] | Hartel, P.; Denker, G.; Kowsari, M.; Krone, M.; Ehrich, H.-D., Information systems modelling with TROLL: formal methods at work, Inform. Systems, 22, 2/3, 79-99 (1997) |
| [19] | Hußmann, H., Formal Foundations for Software Engineering Methods, Lecture Notes in Computer Science, Vol. 1322 (1997), Springer: Springer Berlin |
| [20] | Jacobson, I.; Booch, G.; Rumbaugh, J., The Unified Software Development Process (1999), Addison-Wesley: Addison-Wesley Reading, MA |
| [21] | Jacobson, I.; Christerson, M.; Jonsson, P.; Övergaard, G., Object-Oriented Software Engineering — a Use Case Driven Approach (1993), Addison-Wesley: Addison-Wesley Wokingham, England |
| [22] | Kemmerer, R. A., Integrating formal methods into the development process, IEEE Software, 7, 5, 37-50 (1990) |
| [23] | Kim, S.-K.; Carrington, D., Formalizing the UML class diagram using object-Z, (France, R. B.; Rumpe, B., Proc. 2nd Internat. Conf. on UML, Lecture Notes in Computer Science, Vol. 1723 (1999), Springer: Springer Berlin), 83-98 |
| [24] | http://www.pst.informatik.uni-muenchen.de/\~knapp/foose.html; http://www.pst.informatik.uni-muenchen.de/\~knapp/foose.html |
| [25] | Knapp, A., A Formal Semantics for UML Interactions, (France, R. B.; Rumpe, B., Proc. 2nd Internat. Cont. on UML, Lecture Notes in Computer Science, Vol. 1723 (1999), Springer: Springer Berlin), 116-130 |
| [26] | Lano, K., Formal Object-Oriented Development, Formal Approaches to Computing and Information Technology (1995), Springer: Springer London |
| [27] | K. Lano, R.B. France, J.-M. Bruel, A semantic comparison of Fusion and Syntropy, Object Oriented Systems 6 (1999) 43-72 (http://compscinet.dcs.kcl.ac.uk/OO; K. Lano, R.B. France, J.-M. Bruel, A semantic comparison of Fusion and Syntropy, Object Oriented Systems 6 (1999) 43-72 (http://compscinet.dcs.kcl.ac.uk/OO · Zbl 0979.68021 |
| [28] | Lechner, U., Object-oriented specifications of distributed systems in the \(μ\)-calculus and Maude, (Meseguer, J., Proc. 1st Internat. Workshop on Rewriting Logic and Its Applications, Electronic Notes in Theoretical Computer Science, Vol. 4 (1996), Elsevier: Elsevier Amsterdam), 384-403 |
| [29] | Lechner, U.; Lengauer, C.; Nickl, F.; Wirsing, M., (Objects + concurrency) & reusability — a proposal to circumvent the inheritance anomaly, (Cointe, P., Proc. European Conf. on Object-Oriented Programming ’96, Lecture Notes in Computer Science, Vol. 1098 (1996), Springer: Springer Berlin), 232-247 |
| [30] | Mauw, S., An algebraic specification of process algebra, including two examples, (Wirsing, M.; Bergstra, J. A., Algebraic Methods: Theory, Tools and Applications, Lecture Notes in Computer Science, Vol. 394 (1989), Springer: Springer Berlin), 507-554 |
| [31] | Meseguer, J., A Logical theory of concurrent objects and its realization in the Maude language, (Agha, G. A.; Wegner, P.; Yonezawa, A., Research Directions in Concurrent Object-Oriented Programming (1991), MIT Press: MIT Press Cambridge, MA and London), 341-389 |
| [32] | Meseguer, J., Membership algebra as a logical framework for equational specifications, (Presicce, F. P., Select. Papers 12th Internat. Workshop on Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science, Vol. 1376 (1998), Springer: Springer Berlin), 18-61 · Zbl 0903.08009 |
| [33] | Meseguer, J.; Talcott, C. L., A partial order event model for concurrent objects, (Baeten, J. C.M.; Mauw, S., Proc. 10th Internat. Conf. on Concurrency Theory, Lecture Notes in Computer Science, Vol. 1664 (1999), Springer: Springer Berlin), 415-430 · Zbl 0939.68084 |
| [34] | S. Nakajima, K. Futatsugi, An object-oriented modeling method for algebraic specifications in CafeOBJ, in: W.R. Adrion (Ed.), Proc. 19th Internat. Conf. on Software Engineering, 1997, pp. 34-44.; S. Nakajima, K. Futatsugi, An object-oriented modeling method for algebraic specifications in CafeOBJ, in: W.R. Adrion (Ed.), Proc. 19th Internat. Conf. on Software Engineering, 1997, pp. 34-44. |
| [35] | Object Management Group, Unified modeling language specification, Version 1.3, Technical Report, OMG, 1999, http://cgi.omg.org/cgi-bin/doc?ad/99-06-08; Object Management Group, Unified modeling language specification, Version 1.3, Technical Report, OMG, 1999, http://cgi.omg.org/cgi-bin/doc?ad/99-06-08 |
| [36] | Övergaard, G., A formal approach to collaborations in the unified modeling language, (France, R. B.; Rumpe, B., Proc. 2nd Internat. Cont. on UML, Lecture Notes in Computer Science, Vol. 1723 (1999), Springer: Springer Berlin), 99-115 |
| [37] | Reggio, G., Entitiesan institution for dynamic systems, (Ehrig, H.; Jantke, K. P.; Orejas, F.; Reichel, H., Recent Trends in Data Type Specification, Lecture Notes in Computer Science, Vol. 534 (1991), Springer: Springer Berlin), 244-265 |
| [38] | Reggio, G.; Repetto, L., CASL-CHARTa combination of statecharts and the algebraic specification language CASL, (Rus, T., Proc. 8th Internat. Conf. on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, Vol. 1816 (2000), Springer: Springer Berlin), 243-272 · Zbl 0983.68787 |
| [39] | Rumbaugh, J.; Blaha, M.; Premerlani, W.; Eddy, F., Object-Oriented Modeling and Design (1991), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ |
| [40] | Shlaer, S.; Mellor, S. J., Object Lifecycles: Modelling the World in States (1992), Yourdon: Yourdon Englewood Cliffs, NJ · Zbl 0796.68006 |
| [41] | Warmer, J.; Kleppe, A., The Object Constraint Language (1999), Addison-Wesely: Addison-Wesely Reading, MA |
| [42] | Wirsing, M., Algebraic specification, (van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics (1990), Elsevier: Elsevier Amsterdam), 675-788 · Zbl 0900.68309 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
