Algebraic specifications and refinement for component-based development using RAISE
Keywords:algebraic specifications, refinement, component-based development, formal methods, software engineering
There are two main activities in Component-Based Development: component development, where we build libraries for general use, and component integration, where we assemble an application from existing components. In this work, we analyze how to apply algebraic specifications with refinement to component development. So we restrict our research to the use of modules that are described as class expressions in a formal specification language, and we present several refinement steps for component development, introducing in each one design decisions and implementation details. This evolution starts from the initial specification of a component as an abstract module, and finishes with the final deployment as fully implemented code. The usage of formal tools helps to assure the correctness of each step, and provides the ground to introduce complementarytechniques, such as bisimulations, for the process of component integration.
 John Derrick and Eerke Boiten. Refinement in Z and Object-Z: Foundations and Advanced Applications. Formal Approaches to Computing and Information Technology. Springer, May 2001.
 Hartmut Ehrig and Hans-Jorg Kreowski. Refinement and Implementation. In E. Astesiano, H.-J. Kreowski, and B. Krieg-Bruckner, editors, Algebraic Foundations of System Specification, pages 201–242. Springer, 1999.
 Elsa Est´evez and Pablo Fillottrani. Bisimulation for component-based development. Journal of Computer Science and Technology, 2(6):67–80, 2002.
 Marie-Claude Gaudel and Gilles Bernot. The Role of Formal Specifications. In E. Astesiano, H.-J. Kreowski, and B. Krieg-Bruckner, editors, Algebraic Foundations of System Specification, pages 1–12. Springer, 1999.
 The RAISE Method Group. The RAISE Specification Language. Prentice Hall, 1992.
 The RAISE Method Group. The RAISE Development Method. Prentice Hall, 1995.
 B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222–259, 1997.
 Bertrand Meyer. On to components. Computer, Innovative Technology for Computer Professionals, IEEE Computer, January(4):139–140, 1999.
 Kokichi Futatsugi Razvan Diaconescu. CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. World Scientific, 6, 1998.
 D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing, 9(3):229–269, 1997.
 D. Sannella and A. Tarlecki. Algebraic Preliminaries. In Algebraic Foundations of System Specification, pages 13–30. Springer, 1999.
 Donald Sannella. Algebraic specification and program development bystepwise refinement. In Annalisa Bossi, editor, Logic Programming Synthesis and Transformation, 9th International Workshop, LOPSTR’99, Venezia, Italy, September 22-24, 1999, Selected Papers, volume 1817 of Lecture Notes in Computer Science, pages 1–9. Springer, 2000.
 G. Smith and J. Derrick. Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods in Systems Design, 18:249–284, May2001.
 Clemens Szyperski. Component Software Beyond Object-Oriented Programming. Addison Wesley, 1998.