Special Issue: Software Traceability; Guest Editors: George Spanoudakis and Andrea ZismanNo Access

RETRIEVAL BY CONSTRUCTION: A TRACEABILITY TECHNIQUE TO SUPPORT VERIFICATION AND VALIDATION OF UML FORMALIZATIONS

Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, East Lansing, MI 48824, USA

Search for more papers by this author

R. E. K. STIREWALT

Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, East Lansing, MI 48824, USA

Search for more papers by this author

, and

BETTY H. C. CHENG

Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, East Lansing, MI 48824, USA

Search for more papers by this author

https://doi.org/10.1142/S0218194005002531Cited by:8 (Source: Crossref)

Abstract

Recently, there has been growing interest in formalizing UML, thereby enabling rigorous analysis of its many graphical diagrams. Two obstacles currently limit the adoption and use of UML formalizations in practice. First is the need to verify the consistency of artifacts under formalization. Second is the need to validate formalization approaches against domain-specific requirements. Techniques from the emerging field of requirements traceability hold promise for addressing these obstacles. This paper contributes a technique called retrieval by construction (RBC), which establishes traceability links between a UML model and a target model intended to denote its semantics under formalization. RBC provides an approach for structuring and representing the complex one-to-many links that are common between UML and target models under formalization. RBC also uses the notion of value identity in a novel way that enables the specification of the link-retrieval criteria using generative procedures. These procedures are a natural means for specifying UML formalizations. We have validated the RBC technique in a tool framework called UBanyan, written in C++. We applied the tool to three case studies, one of which was obtained from the industry. We have also assessed our results using the two well-known traceability metrics: precision and recall. Preliminary investigations suggest that RBC can be a useful traceability technique for validating and verifying UML formalizations.

Keywords:

References

G. Antoniolet al., IEEE Trans. on Software Engineering 28(10), (2002). Google Scholar
J. Boyle, R. Resler and V. Winter, IEEE Computer 32(5), 65 (1999). Web of Science, Google Scholar
L. A. Campbellet al., Requirements Engineering Journal 37(10), (2002). Google Scholar
B. H. Cheng and E. Y. Wang, IEEE Trans. on Software Engineering 28(28), 747 (2002). Web of Science, Google Scholar
E. J. Chikofsky and J. H. Cross, IEEE Software 7(1), 13 (1990). Web of Science, Google Scholar
A. Egyed, IEEE Trans. on Software Engineering 29(2), (2003). Google Scholar
W. Frakes and R. Baeza-Yates , Information Retrieval: Data Structures and Algorithms ( Prentice-Hall , 1992 ) . Google Scholar
E. Gamma et al. , Design Patterns: Elements of Reusable Object-Oriented Software ( Addison-Wesley , 1995 ) . Google Scholar
H. J. Goldsby, Specifying compositional semantic functions for non-hierarchical languages using natural deduction systems, Master's thesis, Michigan State University, May 2004 . Google Scholar
O. C. Z. Gotel and A. C. W. Finkelstein, An analysis of the requirements traceability problem, in Proc. 1st Int. Conf. on Requirements Engineeering (ICRE'94), 1994 . Google Scholar
D. Harel and O. Kupferman, IEEE Trans. Software Eng. 28(9), 889 (2002). Web of Science, Google Scholar
J. H. Hayes, A. Dekhtyar, and J. Osborne, Improving requirements tracing via information retrieval, in Proc. 11th IEEE Int. Requirements Engineering Conference, 2003 . Google Scholar
G. Holzmann , The SPIN Model Checker ( Addison-Wesley , 2004 ) . Google Scholar
S. N. Khoshafian and G. P. Copeland, Conference Proc. on Object-Oriented Programming Systems, Languages and Applications (ACM Press, 1986) pp. 406–416. Google Scholar
S.-K. Kim and D. A. Carrington, L'OBJET: Software, Databases, Networks 7(1), (2001). Google Scholar
S. Konradet al., Model Checking Software, Lecture Notes in Computer Science 2648, eds. T. Ball and S. K. Rajamani (Springer Verlag, 2003) pp. 18–33. Google Scholar
D. Latella, I. Majzik and M. Massink, Formal Aspects of Computing 11(6), 637 (1999). Google Scholar
L. Lavazza, G. Quaroni, and M. Venturelli, Combining UML and formal notations for modelling real-time systems, in Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT Int. Symp. on the Foundations of Software Engineering (FSE), 2001 . Google Scholar
J. Lilius and I. Porres , Technical Report 273 ( Turku Center for Computer Science (TUCS), Abo Akademi University , Turku, Finland , 1999 ) . Google Scholar
G. Lüttgen, M. von der Beeck, and R. Cleaveland, A compositional approach to statecharts semantics, in Proc. of ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE'2000), 2000 . Google Scholar
J. I. Maletic, E. V. Munson, A. Marcus, and T. N. Nguyen, Using hypertext model for traceability link conformance analysis, in Proc. 2nd Int. Workshop on Traceability in Emerging Forms of Software Engineering (TEFSE 2003), October 2003 . Google Scholar
A. Marcus and J. I. Maletic, Recovering documentation-to-source-code traceability links using latent semantic indexing, in Proc. IEEE Int. Conf. on Software Engineering, May 2003 . Google Scholar
K. L. McMillan , Symbolic Model Checking ( Kluwer Academic Publishers , 1993 ) . Google Scholar
W. McUmber, A Generic Framework for Formalizing Object-Oriented Modeling Notations for Embedded Systems Development, PhD thesis, Michigan State Univ., August 2000 . Google Scholar
W. McUmber and B. H. Cheng, A general framework for formalizing UML with formal languages, in Proc. IEEE Int. Conf. on Software Engineering, May 2001 . Google Scholar
G. C. Murphy, D. Notkin and K. J. Sullivan, IEEE Trans. on Software Engineering 27(4), 364 (2001). Web of Science, Google Scholar
Object Management Group, UML Specifications, Version 1.5, March 2003 . Google Scholar
OMG, UML Specification V1.5, http://www.omg.org/uml . Google Scholar
Promela language reference, http://spinroot.com/spin/Man/promela.html . Google Scholar
J. Richardson and J. Green, Automating traceability for generated software artifacts, in Proc. IEEE Int. Conf. on Automated Software Engineering (ASE'04), September 2004 . Google Scholar
J. Rumbaugh , I. Jacobson and G. Booch , The Unified Modeling Language Reference Manual ( Addison-Wesley , 1999 ) . Google Scholar
M. Shroff and R. France, Towards a formalization of UML class structures in Z, in Proc. COMPSAC'97, 1997 . Google Scholar
K. Slonneger and B. L. Kurtz , Formal Syntax and Semantics of Programming Languages ( Addison-Wesley , 1995 ) . Google Scholar
G. Smith , The Object-Z Specification Language: Advances in Formal Methods ( Kluwer Academic Publishers , 2000 ) . Google Scholar
On-the-fly, LTL model checking with SPIN, http://spinroot.com/spin/whatispin.html . Google Scholar
R. E. K. Stirewalt and L. K. Dillon, Generation of visitor components that implement program transformations, in ACM SIGSOFT Symposium on Software Reusability, 2001 . Google Scholar
M. C. Tanuan, Automated analysis of unified modeling language (UML) specifications, Master's thesis, Univ. of Waterloo, August 2001 . Google Scholar
A. Zisman, G. Spanoudakis, E. Peres-Minana, and P. Krause, Tracing software engineering artifacts, in Proc. 2003 Int. Conf. on Software Engineering Research and Practice (SERP'03), 2003 . Google Scholar