Using Formal Methods to Facilitate Software Reuse

Reusing software may greatly increase the productivity of software engineers and improve the quality of developed software. Software component libraries have been suggested as a means for facilitating reuse. A major difficulty in designing software libraries is in the selection of a component representation that will facilitate the classification and the retrieval processes. Using formal specifications to represent software components facilitates the determination of reusable software because they more precisely characterize the functionality of the software, and the well-defined syntax makes processing amenable to automation.

This project applies formal methods to the classification and organization of reusable software components. From a set of formal specifications, a two-tiered hierarchy of software components is constructed. The formal specifications represent software that has been implemented and verified for correctness. The lower-level hierarchy is created by a subsumption test algorithm that determines whether one component is more general than another; this level facilitates the application of logical reasoning techniques for a fine-grained, exact determination of reusable candidates. The higher-level hierarchy provides a coarse-grained determination of reusable candidates and is constructed by applying a hierarchical clustering algorithm, based on syntactical similarity, to the most general components from the lower-level hierarchy. The hierarchical organization of the software component specifications provides a means that is amenable to automation for storing, browsing, and retrieving reusable components In addition, the formal specifications facilitate the verification process that proves a given software component correctly satisfies the current problem.

We are also investigating the use of analogy to determine how a given reusable component should be modified to satisfy a new problem specification. A prototype browser that provides a graphical framework for the classification and retrieval process is being developed.

Recent Papers

  • ``A Semantic Foundation for Specification Matching'' (with Y. Chen) in Foundations of Component-Based Systems Eds. M.~Sitaraman and G.~Leavens, Cambridge University Press, 2000.

  • ``Formalizing and Automating Component Reuse'' (with Yonghao Chen), in IEEE Proc. of International Conference on Tools with Artificial Intelligence, November 1997.

  • ``Facilitating an Automated Approach to Architecture-based Software Reuse'' (with Yonghao Chen), in Proc. of IEEE Automated Software Engineering, November 1997.

  • ``Reusing Analogous Components'' (Betty H.C. Cheng and Jun-Jang Jeng), in IEEE Trans. on Knowledge and Data Engineering, Vol 9., No. 2, March/April 1997, pp. 341--349. (extended version) Michigan State University Technical Report, MSU-CSE-94-28 (Revised June 1995).

  • ``Formally Specifying and Analyzing Architectural and Functional Properties of Components for Reuse'' (with Yonghao Chen), Proc. Eighth Annual Workshop on Software Reuse (WISR8), Columbus, OH, March 1997.
  • ``Specification Matching for Software Reuse: A Foundation'' (Jun-Jang Jeng and Betty H.C. Cheng), Proc. of ACM Symposium on Software Reuse , Seattle, Washington, April 1995.

  • ``A Formal Approach to Reusing More General Components'' (Jun-Jang Jeng and Betty H.C. Cheng), IEEE Proc. of 9th Knowledge-Based Software Engineering Conference, Monterey, California, pp. 90-97, September 1994.

  • ``Applying Formal Methods to Software Reuse'', Jun-Jang Jeng, PhD Thesis, December 1993.

  • ``Using Analogy to Determine Program Modifications Based on Specification Changes'' (Jun-Jang Jeng and Betty H.C. Cheng), Proc. of IEEE Int'l Conf. on Tools with Artificial Intelligence, pp. 113--119, November 1993.

  • ``Using Formal Methods to Construct a Software Component Library,'' (Jun-Jang Jeng and Betty H.C. Cheng), Lecture Notes in Computer Science, Vol. 717, Springer-Verlag, pp. 397--417, %in Proc. of Fourth European Software Engineering Conference, September 1993.

  • ``Formal Methods Applied to Reuse'' (Jun-Jang Jeng and Betty H.C. Cheng), Proc. of the Fifth Annual Workshop on Software Reuse, October 1992.

  • ``Using Automated Reasoning Techniques to Determine Software Reuse'' (Jun-jang Jeng and Betty H.C. Cheng), International Journal of Software Engineering and Knowledge Engineering, Vol. 2, No. 4, pp. 523--546, December 1992.