An Approach to Formal Specification of Component-Based Software

Introduction

Component based development (CBD) is a new promising approach for building software applications. The central idea of this emerging approach is based on reuse of software building blocks to make entirely new systems by assembly (composition), and thus has the advantage of providing software systems in a shorter time with better quality.

Building an application is thus seen, not as an integral and complete development (from scratch), but like an assembly of reusable pieces. In this field, technologies supporting the construction and assembly of components has reached a first level of maturity, in particular with the emergence of technological components standards such as EJB (Enterprise JavaBeans), CCM (Corba Component Model), or (D)COM ((Distributed) Component Object Model). The goal of component-based software engineering (CBSE) is to increase productivity, quality, and time-to-market in software development. The software engineering techniques specific to this field (CBSE), in phases such as modeling, verification or validation of components based applications still insufficient and need more research efforts. The heart of CBD is components. A software component is a contractually specified building block for software which can be readily deployed by third parties without understanding its internal structure. A component is a black box which is described by its interfaces throw which it can interact with other components in the system. The ultimate goal of Component-based Software Development (CBD) is third-party assembly. To achieve this, it is necessary to be able to specify components in such a way that we can reason about their construction and composition (Lau, A., Ornaghi, M., 2001). The specifications of components used in practical software development today are limited primarily to what we’ll call syntactic specifications. This form of specification includes the specifications used with technologies such as COM, the Object Management Group’s Common Object Request Broker Architecture (CORBA), and Sun’s JavaBeans (Crnkovic, I., Larsson, M., 2002). The two first ones use IDLs while the third uses the Java programming language. However, syntactic specification does not provide information on the semantic of operations that define the component interfaces, which can help to better understand their behavior. Formal specification methods are good candidate to specify component software.

The objective of our work is to propose a formal approach for component based software modeling using ECATNets (Extended Concurrent Algebraic Term Nets). ECATNets are a kind of High-Level Algebraic Nets. They are proposed as a way for specification, modeling and validation of applications from the area of communication networks, computer designs and other complex systems (Bettaz, 1996). They are built around a combination of three formalisms. The two first formalisms constitute a net/data model, and are used for defining the syntax of the system, in other terms to capture its structure. The net model, which is a kind of advanced Petri net, is used to describe the process architecture of the system; the data model, which is an algebraic formalism, is used for specifying the data structures of the system. The third formalism, which is a rewriting logic, is used for defining the semantics of the system, or in other words to describe its behavior.

In this chapter we will try to explain how to produce a model of a component based software system using our notation based on ECATNets formalism. The model denotes the interconnection of behavioral specifications of connected software components. The elements, composing the whole system, can be for instance a travel agency system with its components: ‘a coordinator component’, ‘book hotel’, ‘Book flight’. This example will serve to illustrate in this paper our modeling approach. The expected benefits of this work are: Offer a formal notation for describing the different features of concurrent and distributed software components; Defining a formal unambiguous semantic to describe behavior of the composed system; Allowing formal verification of some properties of the modeled systems helping to avoid composition mistakes leading to unexpected and often bizarre behavior.

The chapter is organized as follows. In Section 2, we review some basic concepts about ECATNets. In section 3, we present the notation proposed to specify formally a software component using ECATNets and how connections are made between the components. Section 4 shows an example illustrating our approach. Finally, conclusions and perspectives are presented.