Multilevel Traceability Links Establishments Between SOFL Formal Specifications and Java Codes Using Multi-dimensional Similarity Measures

Linking the components in a formal specification to those in the corresponding program is a prerequisite for formal specification-based program fault detection. Existing traceability link techniques for reducing manpower and time cost suffer from the limitation in effectiveness due to over dependency of textual similarity. Unlike the existing work, this paper presents an automatic method for constructing traceability links between SOFL formal specifications and Java codes, taking semantical, structural, functional, and relational similarities measures into account. It operates at multiple levels of a formal specification, such as data flows, processes, and modules, to establish finegrained link relationships between artifacts. Further, a comparative evaluation of the proposed method, using two selected modules of the SOFL formal specification of a critical ATM system and its Java implementation with 951 code of lines, demonstrates an improvement in precision and more generality than existing latent semantic indexing that is an information retrieval-based method.