This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Formal Semantics for Object Model Diagrams
October 1995 (vol. 21 no. 10)
pp. 799-821
Informal software development techniques, such as the Object Modeling Technique (OMT), provide the user with easy to understand graphical notations for expressing a wide variety of concepts central to the presentation of software requirements. OMT combines three complementary diagramming notations for documenting requirements: object models, dynamic models, and functional models. OMT is a useful organizational tool in the requirements analysis and system design processes. Currently, the lack of formality in OMT prevents the evaluation of completeness, consistency, and content in requirements and design specifications. A formal method is a mathematical approach to software development that begins with the construction of a formal specification describing the system under development. However, constructing a formal specification directly from a prose description of requirements can be challenging. This paper presents a formal semantics for the OMT object model notations, where an object model provides the basis for the architecture of an object-oriented system. A method for deriving modular algebraic specifications directly from object model diagrams is described. The formalization of object models contributes to a mathematical basis for deriving system designs.

[1] R. Lutz, "Targeting Safety-Related Errors During Software Requirements Analysis," Proc. First ACM SIGSOFT Symp.The Foundations of Software Engineering, 1993.
[2] R.R. Lutz,“Analyzing software requirements errors in safety-critical embedded systems,” Proc. of IEEE Int’l Symp. on Requirements Engineering, 1993.
[3] J.C. Kelly, J.S. Sherif, and J. Hops, "An Analysis of Defect Densities Found During Software Inspections," J. Systems Software, Feb. 1992, pp. 111-117.
[4] V.R. Basili and B.T. Perricone,“Software errors and complexity: An empirical investigation,” Comm. ACM, vol. 27, no. 1, pp. 42-52, Jan. 1984.
[5] B. Boehm,“Software engineering economics,” IEEE Transactions on Software Engineering, vol. 10, pp. 4-21, Jan. 1984.
[6] J.M. Wing,“A specifier’s introduction to formal methods,” IEEE Computer, vol. 23, pp. 8-24, Sept. 1990.
[7] B.H.C. Cheng,“Applying formal methods in automated software development,” J. of Computer and Software Engineering, vol. 2, no. 2, pp. 137-164, 1994.
[8] P. Coad and E. Yourdon, Object-Oriented Analysis, second ed., Yourdon Press, Englewood Cliffs, N.J., 1991.
[9] R.J. Wirfs-Brock, B. Wilkerson, and L. Wiener, Designing Object Oriented Software, Prentice Hall, Upper Saddle River, N.J., 1990.
[10] C.L. Chang, R.A. Stachowitz, and J.B. Combs, “Validation of Nonmonotonic Knowledge-Based Systems,” Proc. IEEE Int'l Conf. Tools for Artificial Intelligence, Nov. 1990.
[11] D. Coleman et al., Object‐Oriented Development: The Fusion Method, Prentice‐Hall, Englewood Cliffs, N.J., 1994.
[12] R.S. Pressman, Software Engineering—A Practitioner's Approach, 3rd ed., McGraw-Hill, New York, 1992.
[13] P.P. Chen, “The Entity‐Relationship Model: Toward a Unified View of Data,” ACM Trans. Database Systems, Vol. 1, No. 1, Jan. 1976, pp. 9–36.
[14] D. Harel,A. Pneuli,J.P. Schmidt,, and R. Sherman,“On the formal semantics of statecharts,” Proc. Second IEEE Symp. on Logic in Computer Science, pp. 54-64, 1987.
[15] J.E. Hopcroft and J.D. Ullman, Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Apr. 1979.
[16] M. Wirsing, “Algebraic Specification,” Handbook of Theoretical Computer Science, vol. B, pp. 675-788, Amsterdam: North Holland, 1990.
[17] R.H. Bourdeau,B.H. Cheng,, and B. Pijanowski,“A regional information system for environmental data analysis,” to appear in Photogrammetric Engineering&Remote Sensing.
[18] B.H.C. Cheng,R.H. Bourdeau,, and G.C. Gannod,“The object-oriented development of a distributed multimedia environmental information system,” Proc. Sixth Int’l Conf. on Software Engineering and Knowledge Engineering, pp. 70-77, June 1994.
[19] B. Liskov and J. Wing,“Family values: A semantic notion of subtyping,” Tech. Rep. 562, MIT Laboratory for Computer Science, 1992.
[20] G.T. Leavens and W.E. Weihl,“Subtyping, modular specification and modular verification for applicative object-oriented programs,” Tech. Rep. #92-28, Department of Computer Science, Iowa State University, Sept. 1992.
[21] J.A. Bergstra,J. Heering,, and P. Klint,“The algebraic specification formalism ASF,” Algebraic Specification (J. A. Bergstra, J. Heering, and P. Klint, eds.), ACM Press, Addison-Wesley Publishing Company, 1989.
[22] J. Guttag, J. Horning, S. Garland, K. Jones, A. Modet, and J. Wing, Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
[23] J. Horning and J. Guttag,“Larch shared language checker.” Private communication.
[24] S. Garland and J. Guttag,“A guide to lp, the larch prover,” Technical Report TR 82, DEC SRC, Dec. 1991.
[25] M.R. Laux,R.H. Bourdeau,, and B.H.C. Cheng,“An integrated development environment for formal specifications,” Proc. Int’l Conf. on Software Engineering and Knowledge Engineering(San Francisco, Calif.), pp. 681-688, July 1993.
[26] C.L. Chang and R.C.T. Lee,Symbolic Logic and Mechanical Theorem Proving.New York: Academic Press, 1973.
[27] L.C. Grove,Algebra. Academic Press, 1983.
[28] J. M. Spivey,The Z Notation: A Reference Manual. Englewood Cliffs, NJ: Prentice-Hall, 1989.
[29] T.C. Hartrum and P.D. Bailor,“Teaching formal extensions of informal-based object-oriented analysis methodologies,” Proc. Computer Science Education, pp. 389-409, 1994.
[30] F. Polack,M. Whiston,, and K. Mander,“The SAZ project: Integrating SSADM and Z,” FME’93: Industrial-Strength Formal Methods (J. Woodcock and P. Larsen, eds.), Odense, Denmark, pp. 541-557, Springer-Verlag, Apr. 1993.
[31] L. Semmens and P. Allen,“Using Yourdon and Z: An approach to formal specification,”inZ User Workshop,Oxford, 1990, J. E. Nicholls, Ed. New York: Springer-Verlag, 1991.
[32] J. Rumbaugh,“Relations as semantic constructs in an object-oriented language,” Proc. of OOPSLA‘87, pp. 466-481, 1987.
[33] F. Hayes and D. Coleman,“Coherent models for object-oriented analysis,” Proc. OOPSLA‘91, pp. 171-183, 1991.
[34] C. B. Jones,Systematic Software Development Using VDM. Englewood Cliffs, NJ: Prentice-Hall, 1990, 2nd ed.
[35] R.H. Bourdeau,E.Y. Wang,, and B.H.C. Cheng,“An integrated approach to developing diagrams as formal specifications,” Technical Report MSU-CPS-94-42, Michigan State University, Sept. 1994. (submitted for publication).
[36] B.H.C. Cheng,E.Y. Wang,, and R.H. Bourdeau,“A graphical environment for formally developing object-oriented software,” Proc. IEEE Sixth Int’l Conf. on Tools with Artificial Intelligence, Nov. 1994.

Index Terms:
Algebraic specification, formal methods, object modeling, requirements specification, semantics.
Citation:
Robert H. Bourdeau, Betty H.C. Cheng, "A Formal Semantics for Object Model Diagrams," IEEE Transactions on Software Engineering, vol. 21, no. 10, pp. 799-821, Oct. 1995, doi:10.1109/32.469459
Usage of this product signifies your acceptance of the Terms of Use.