Most software today is built from pre-existing components, often given in a form which allows then to be used but not analysed (typically off-the-shelf components distributed as binary files). Software design means composition and correctness of the design relies on the correctness of individual components.
This practice saves on time and the cost of development and results in products which are easier to upgrade and maintain. But it also creates a host of basic but technically challenging questions and problems: What in essence is a reusable component? What is the semantics of a component? How can we abstract away from the details of the semantics in order to decide suitability of a component for the design? What is the "best" abstraction level for this? Given two descriptions of one component (a specification and an implementation) how can we make sure they are consistent? How do we check consistency if the implementation details are unavailable (because they are proprietary, remote or even non-existent)? How can we formulate a request for a component? How can we choose one? How can we assemble components and calculate the semantics of the composition? To what extent can we adapt a component which fits only partly into our design? How can we obtain components? How can we store them for effective retrieval? How can we postpone "assembly" till run-time, resulting in software which evolves with its environment? What is the semantics of this? And so on.
The goal of the project is to study formally-based methods for software design from pre-existing components, including but not limited to the issues above. In particular, we look for a common ground to use together formal methods (to predict the result of putting components together) and fault-tolerance (to detect and recover from errors of individual components at run-time). Based on the results of such study we want to implement prototype tools to perform specialised tasks like e.g. calculating the semantics of composition, generating proof conditions, generating component wrappers to monitor their behaviour at run-time, discovering automatically the presence of redundancy among components, carrying out transformations to exploit this redundancy, etc. We plan to implement such tools rigorously using RAISE and integrate them at the end into a single environment: Composition Workbench.
July 1996 - January 1998
So far the project work has gone into three areas of study: (1) Fault-tolerance with Yun Xiaochun. PhD thesis based on the results of the project: "Research on the Reconfiguration Technology of Reusable Software Components". One paper: "Fault-Tolerant Software Composition from Verified and Unverified Components", to be submitted. Describes how to assemble the components to achieve reliability of the composition despite possible failures of individual components. (2) Abstraction with Elsa Estevez. Paper is written: "Bisimulation Abstraction for Selection of Software Components in RAISE". Describes how bisimulation can play the role of an abstracting equivalence for selecting components described as RSL modules, concerned only with their external behaviour. (3) Monitoring, with Wojciech Mostowski from Gdansk, Poland, September 1998 until May 1999. Paper and software are written: "Pattern-Matching for Software Reliability via Run-Time Behaviour-Checking", how to use regular expressions as formal specifications of software components, suitable for checking their behaviour (by pattern-matching) at run-time. Implementation under way to generate a component wrapper from its specification.
Two UNU/IIST reports which document initial stages of the project. Report [1] is a contribution to formalise, in a systematic way, some of the issues related to CORBA, as a means to overcome problems caused by the heterogeneity of the interacting components (so-called specification- and implementation-barriers). Report [2] outlines some initial ideas about an integrated CORBA/RAISE environment for building software from pre-existing components. Given that CORBA IDL (Interface Description Language) describes only the signatures of operations that the component offers for its environment, the papers exploits the possibility that semantics is captured within an extended IDL - XIDL = IDL + RSL. More reports are in progress.
The project is expected to continue. New fellow arrives in January 1999: Mr. Babatunde Opeoluwa Akinkunmi from the University of Ibadan, Nigeria. He will initiate the fourth area of study: Composition. How to exploit applicative part of the RSL language to specify individual components and imperative/concurrent part to assemble them together. How to calculate the result of such composition, semantically.