Reuse of Formal Specifications

INTRODUCTION

During the Rigorous Approach to Industrial Software Engineering (RAISE) specification development process, a variety of components and infrastructures are built. All of these components are not independent, but related to one another, especially when we specify different systems into the same infrastructure. The RAISE method (Bjorner, 2000) is based on the idea that software development is a stepwise, evolutionary process of applying semantics-preserving transitions. Thus, the reuse process is crucial in all of the stages of the development, but there is no explicit reference to the specification reusability in this development process.
Software components are typically very rich in information, making the task of characterizing them and capturing their relevant properties difficult. However, this is not the only reason that makes software reuse difficult. Krueger (1992) provides a brief general survey and very clear view of different approaches for software reuse.
Information retrieval methods based on analyses of natural-language documentation have been proposed to construct software libraries (Helm & Maarek, 1991; Maarek, Berry & Kaiser, 1991). Software components represented by natural language can make the retrieval process a task with ambiguity, incompleteness and inconsistency. Using a rigorous method to the retrieval of a component can minimize all of these problems.
Based on these observations, we introduce a Reusable Component (RC) model for the definition of the reusable component structure into RAISE. Related to this method, it is important to emphasize the work of Beltaifa and Moore (2001). They propose an infrastructure to support reuse improving the efficiency of reusing software components.
RC model integrates RAISE Specification Language (RSL) specifications (George et al., 1992) and object-oriented code. RC model describes object-oriented classes at different levels of abstraction:
• Specialization: hierarchies of RSL implicit specifications related by formal specialization relationship.
• Realization: hierarchies of RSL complete algebraic specifications related by realization relationship.
• Code: hierarchies of imperative RSL schemes related by implementation relationship and linked to object-oriented code.
Also, a rigorous process for reusability of RC components is defined. Its manipulation, by means of specification building operators (Rename, Extend, Combine and Hide), is the basis for the reusability.
Our approach allows that the properties of components formally specified can be characterized by giving a functional (RSL specification) description. Therefore, they may be useful to someone searching for a particular component.
Different possible classes of existing RC components may be retrieved using a formal reasoning technique: an exact match to the query specification, a component more general than the query, or a component more specific than the query.


BACKGROUND

Different approaches to specify reusable components functionalities have been proposed. The way in which the components can be used with others can play a critical role in the reuse implementation.
Related with the RAISE method, we emphasize the work of Beltaifa. They propose an infrastructure to support reuse which improve both the ease and efficiency of reusing software components. The main difference with our work is the integrated process defined for all stages of the development method.
As a typical related work, we can mention Hennicker and Wirsing (1992) who present a model for reusable component definition. A reusable component is defined as an unordered tree of specifications where any two consecutive nodes are related by the implementation relation and the leaves are different implementations of the root. The work of Chen and Cheng (1997) is another approach that provides a formalism to register components properties to reuse them based on the architecture and integration of the system. They are related to LOTOS tools to facilitate the retrieval of the reusable component.
On the other hand, the work of Zaremski and Wing (1997) is related to the specification matching. It is very important to emphasize this proposal has been referenced by a lot of authors.
There are two main activities in the RAISE method: writing an initial specification, and developing it towards something that can be implemented in a programming language (George, 2002). Writing the initial specification is the most critical task in software development. If it is wrong, that is, if it fails to meet the requirements, the following work will be largely wasted. It is well known that mistakes made in the life-cycle are considerably more expensive to fix than those made later.
What kinds of errors are made at the beginning? The main problem is that we may not understand the requirements. The requirements are written in a natural language, and, as a result, likely to be ambiguous. The aim of the initial specification is to capture the requirements in a formal and precise way.

MAIN THRUST OF RAISE AND REUSE

The aim of the project RAISE was to develop a language, techniques and tools that would enable industrial usage of “formal methods” in the construction of software systems. The results of this project include the RSL language, which allows us to write formal specifications; a method to carry out developments based on such specifications, and a set of tools to assist in edition, checking, transforming and reasoning about specifications.
RSL is a “wide spectrum” language that can be applied at different levels of abstraction as well as stages of development. It includes several definition styles such as model-based or property-based, applicative or imperative, sequential or concurrent.
A development in RAISE begins with an abstract specification and gradually evolves to concrete implementations. The first specification is usually an abstract applicative one, for example, functional or algebraic. A first algebraic specification should have:
• A hierarchy of modules whose root is the system module;
• A module containing types and attributes for the non-dynamic identified entities; and
• The signatures of the necessary functions associated with types. These functions should be categorized as generators (if the associated type or a type dependent on it appears in their result types) and as observers. Besides, preconditions should be formulated for partial functions. These preconditions are expressed by means of functions called “guards”.
The specification may contain invariants expressed as functions.

RC Model Description

RC describes object classes at three different conceptual levels: specialization, realization and code. These names refer to the relations used to integrate specifications in the three levels. A more detailed description can be found in Felice, Leonardi, Favre, and Mauco (2001).

RC Components

The specialization level describes a hierarchy of incomplete RSL specifications as an acyclic graph. The nodes are related by the specialization relationship. In this context, it must be verified that if P(x) is a property provable about objects x of type T, then P(y) must be verified for every object y of type S, where S is a specialization of T.
Specialization level reconciles the need for precision and completeness in abstract specifications with the desire to avoid over-specification.
Every leaf in the specialization level is associated with a sub-component at the realization level. A realization sub-component is a tree of complete specifications in RSL:
• The root is the most abstract definition.
• The internal nodes correspond to different realizations of the root.
• Leaves correspond to sub-components at the implementation level.
If E1 and E2 are specifications E1 can be realized by E2 if E1 and E2 have the same signature and every model of E2 is a model ofE1 (Hennicker & Wirsing, 1992).
Adaptation of reusable components, which consumes a large portion of software cost, is penalized by over-dependency of components on the physical structure of data.
The realization level allows us to distinguish decisions linked with the choice of data structure. In RAISE, there are four main specification style options. They are applicative sequential, imperative sequential, applicative concurrent and imperative concurrent (George, Haxthausen, Hughes, Milne, Prehn, & Pedersen, 1995). Associated with them, there are two styles: abstract and concrete. Imperative and concrete styles use variables,assignments, loops, channels (in concurrent specifications), and so forth, that are related to design decisions about data structures. Every specification at the realization level is linked to sub-components at the code level.
The code level groups a set of schemes in RSL associated with code. The RAISE method provides translation processes, which start with a final RSL specification and produce a program in some executable language, for example, C++ using the translation tool component of the RAISE toolset (George, 2001).

RC Relationships

It is worth considering that the three relations (Specialization, Realization and Code) form the “RAISE implementation relation” (George et al., 1992). Any formal system that aims to provide a means of specification and development must provide a notion of implementation. That is, if specification E1 is related to specification E2 in the model, we need to know ifE1 and E2 are in the “RAISE implementation relation”. The following properties must be satisfied:
“Properties preservation: All properties that can be proved about E1 can also be proved for E2 (but not vice versa in general).
Substitutivity: An instance of E1 in a specification can be replaced by an instance E2, and the resulting new specification should implement the earlier specification”.

RAISE DEVELOPMENT PLAN APPLYING A REUSE MODEL

Engineers usually proceed from applicative to imperative specifications. The proposal is to introduce the RC model for the definition of the reusable component structure into RAISE method. Where does one introduce this model? RAISE developers start with the module scheme specification, define an abstract applicative module, and develop a sequence of concrete applicative modules and the corresponding set of imperative modules from the final applicative modules. Figure 1 summarizes the overview of the method.
During the first stages of development, when the interaction with the stakeholders is crucial, the use of client-oriented requirements engineering techniques seem to be necessary in order to enhance the communication between the stakeholders and the software engineers. It has been proposed that a systematic reuse approach integrates natural language requirement specifications with formal specifications in RSL. Some heuristics are described to develop a formal specification in RSL starting from models which belong to the requirements baseline (Mauco & George, 2000).
The goal is that engineers can make reuse in all development stages. Therefore, by introducing the RC model in all the development steps, it will be possible to make use of abstraction, selection, specialization, and integration of software artifacts in the RAISE method.

THE REUSE PROCESS

Formal specifications are used to model the problem requirements and the function of the library components. The specifications are written in RSL language. The classification scheme consists of a collection of formal definitions representing possible component features in the domain. The formalization of the scheme permits automated classification of the specifications. The retrieval mechanism is based on syntactic comparison of features sets. The components returned by the retrieval mechanism are passed on to a more detailed evaluation that uses specification matching to determine reusability.
The work of Penix (1998) is an important approximation, because he proposes automated component retrieval and adaptation using a heuristic based on specification semantics to indicate component reusability.

Figure 1. Overview of the RAISE method

Overview of the RAISE method

Figure 2. The method

 The method
The results of specification matching determine the relationship that exists between the retrieved components and the requirements specification. The adaptation phase allows in determining whether a mechanism exists to adapt or combine the retrieved components to solve the problem.
The main idea is to transform the incomplete RSL specification into complete imperative specification by reusing existing components. The method has the following steps: decomposition, identification, adaptation and composition depicted in Figure 2.
• Decomposition step: the decomposition of a goal specification Eg into sub-specifications E1, E2, ….En is formalized.
• Identification step: for each specification Ei a component Ci (in the specialization level) and a sequence s1,s2,…,sn of RSL specifications must be identified, verifying the implementation relation. A node in Ci must be selected as a candidate to be transformed. The identification of a component is correct if it can be modified by rename, hide and extend operators to match the query Ei.
• Adaptation step: not only a leaf in the sub-component associated in the realization level but also a sequence of operators used in the previous steps are applied. Then, a scheme in the code level is selected and the same operators in the selected leaf are applied.
• Composition step: the sub-specifications Ei and their implementations are composed. Next, the Identification step is introduced.

RC Identification

The component classification is described by a set of features. Each feature represents a property or an attribute of the component. They can be refined to give them a more precise meaning. The objective is to support effective retrieval of component. So, in order to be useful in practice, the component specifications should be independent of the kind of component, allowing the storage of different kinds of them, for example, requirements definitions, designs, documentation, and so forth. A very important approach that provides a formalism to register components properties is the work of Chen and Cheng (1997). It is based on the architecture and integration of the system facilitating the retrieval of a reusable component.
Being a RSL specification is a collection of modules, and a module basically a named collection of declarations as either a scheme or an object -objects and schemes defined using class expressions-, we propose a classification based on a feature-oriented model. Each feature describes a property of the component, and is characterized by:
(a) kind of component: describing the function of different kinds of components like: requirements specifications, designs specifications, systems specifications, documentation, and so forth;
(b) operations performed;
(c ) component structure: modules involved (schemes and objects):
(c.1) granularity of each module: list of objects related with the class;
(d) relationships to another component (‘implements’ relations and composition of components); and
(e) component specification style (applicative sequential, imperative sequential, imperative sequential, applicative concurrent or imperative concurrent and abstract and concrete styles).
By localizing the possible components, the goal is to compare a component with the query. This process has two essential steps: signature matching and semantic matching. The signature matching enables a syntactic comparison of a query specification with specifications
Signature-Matching:
Query-Signature X RC-Library X Match-Predicate Set-of RC-Components Signature-Matching(Q,C,P) = { c C/ P(Q,C)} existing in RC reusable components. The semantic matching compares the specifications dynamic behavior. The bases of the signature matching come from Zaremski and Wing (1997), even though they were adapted to the identification of RC components.
The signature of a specification consists of a set of sorts and a set of operations, each operation being equipped with a particular functionality.
Let L=<SL, FL> be the signature of a library specification and Q=<SQ,FQ> the signature of a query specification where SL and SQ are sets of sorts and FL and FQ are sets of operation symbols, the signature matching is defined in the figure above.
This means that given a query specification Q, a RC library C and a predicate P, it gives back the RC components that satisfy P. The signature matching is based on operations matching. Different kinds of operation matching can be applied. They are the exact, generalized and specialized matching of operations. This matching requires a specifications signature matching (sorts and operations) and the axioms proofs between pairs of operations.

Searching for a Reusable Candidate

The RC library is a fundamental piece to the engineering because it contains existing components that will be reused later in the large systems constructions. The appropriate use of it requires:
• the organization of the library, in order to facilitate the search of the components and to improve the efficiency retrieval, and
• the comparison between the description of the library component with the description of the new description.
The identification consists: first, in a syntactic comparison between a library component in RSL language and the user query one, and then, in a semantic comparison of the library component behavior with the query specification behavior both expressed by axioms. The former description corresponds to the syntactic matching, and the latter corresponds to the semantic matching. A very important factor to consider is the granularity levels of components. They are the list of objects that belong to a
RSL module. The component can modify its size, from construct operations of the language to modules for big software systems. To describe and to reuse components they must be encapsulated.

FUTURE TRENDS

Our goal is to solve a problem which is a weakness of the RAISE formal method. Therefore, the proposal of our future work is to apply not only the software components reuse but also a domain specifications reuse, that is, in the confines of the domain engineering.

CONCLUSION

An overview of the strategy to classify and select a RAISE reusable component is presented. The RC model serves for the description of reusable components and a transformational process with reuse from RSL specifications to code is presented. This model aims to solve a problem that is a weakness of RAISE formal method.

KEY TERMS

Algebraic Specification: A technique whereby an object is specified in terms of the relationships between
the operations that act on that object. A specification is presented in four parts:
1. Introduction part, where the sort of the entity being specified is introduced and the name of any other specifications that are required are set out;
2. Informal description of the sort and its operations;
3. Signature, where the names of the operations on that object and the sorts of their parameters are defined; and
4. Axioms, where the relationships between the sort operations are defined.
Reusable Component: The aim of reusable components is to provide services to other components and to require services from others. There are three concepts associated with them: their interfaces, their architectures and their realizations.
Reuse Process: A method having the following steps: the decomposition of the goal specification, the identification for each specifications, the adaptation step using the appropriate operators and the composition of the sub-specifications.
Rigorous Process: A mathematically-based technique for describing and reasoning about system properties. It provides frameworks within which people specify, develop, and verify systems in a systematic manner.
Semantic Matching: Semantic matching compares the specifications dynamic behavior.
Signature Matching: Signature matching enables a syntactic comparison of a query specification with specifications existing in a model.
Specification Matching: The process to determine if two software components are related. It allows us to distinguish when two component specifications match, we know that certain guarantees about the behavior of the system will hold if we substitute one component for the other.

Next post:

Previous post: