Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Model Driven Architecture (MDA) [1] is recognised as a strong way to develop high-quality systems, and specifically reactive systems which are event-driven systems that must continuously react to external stimuli. Such systems include for instance embedded controllers for automotives, avionics, train, telephony, but also communication network.

Within MDA, models are in the center of a stepwise development based on model extensions, refinements and transformations, from an abstract incomplete specification to a concrete complete model. By this way, models serve both as a description of the problem domain, i.e. a requirement, and a specification for the implementation, bridging the gap between problem and solution. Many methods and tools have been proposed to support model development based on standard modelling languages such as UML or SysML. Methodologies are also necessary in order to deal with complex systems. Systems Engineering [2] addresses this challenge in a holistic way considering both business and technical aspects of a system design, integrating all stakeholders at the early stage of the development, starting from the user requirements and the definition of the environment of the system to be designed in order to produce high-quality systems. Many methodologies and many standards have been proposed to follow these recommendations as it is shown in the survey proposed in [3]. Our area of interest focuses on the definition and the analysis of the behavioural view of the system, expressed by a functional or organic architecture whose components are defined by a behavioural view or an architectural one. The target activities are therefore the functional analysis, the functional verification and the synthesis in the IEEE 1220 Process model [4]. Our experience in system modelling highlighted that architecture definition, behavioural abstraction and refinement are the core activities of system design. Designing a system consists not only in modelling its architecture, but also in evaluating its behavioural models and that of its components at the beginning of the modelling process, although the model is incomplete and non-deterministic. These features have to be considered as a support for designers and architects. It means that such verifications have not to be postponed at the end of the modelling process. They have to be integrated in the incremental development of the system and its components.

For this propose, we have defined IDF, an Incremental Development Framework. It is defined by a set of relations computed on an abstract formalism (LTS for Labelled Transition System), allowing models to be evaluated during their development. The environment of the system to be designed can be at its turn modelled taking into account its uncertain or non-deterministic behaviour. By this way, incompatibility or non-interoperability can be detected at early stages of the design process. The framework is supported by a tool, named IDCM (Incremental Development of Compliant Models). Experiments have been conducted on UML models. Our work is inspired by techniques of model checking [5]. Such verifications aims at:

  • supporting the stepwise realisation of systems by applying refinement and extension operations

  • analysing the interaction of the system with its environment, with respect to non-deterministic scenarios

  • insuring the interoperability of the system components

  • insuring the evolution of the system by substituting a component by a new one

This paper gives an overview of the concepts of IDF and tools we have developed to support IDF. The following section presents modelling concepts of architectures and behavioural components through an incremental development process in order to point out topics being addressed. Section 2 introduces definition of liveness and abstraction models allowing UML/SysML models to be analysed. Section 3 gives an overview of relations we have implemented to support IDF. Section 4 shows main functionalities of the tool IDCM for supporting IDF concepts. A presentation of our future work will close this article.

2 The Architectural Paradigms

In this section, we present main useful concepts to understand our proposal for incremental development of architectural models. We focus on the verification of behavioural specifications of a system all along its design life cycle. Figure 1 gives an overview of the useful operations for the development of a system based on a MDA approach. We suppose that the first step starts by defining a behavioural specification of the system (behav1 in Fig. 1) at a high abstraction level. Such a specification may evolve and be extended (behav2 in Fig. 1) until an agreement is reached between the various stakeholders of the system development (client, end-users, designers). This agreement may however evolve during the system design process and at every step, it will be necessary to be able to take into account new specifications.

Fig. 1
figure 1

Overview of an incremental development through refinement and extension operations

Full size image

When the system is complex, its design is structured into components that may represent functional components or physical components depending on the stage of the design process. Components defined according to a structural view are called architectures. For example, in Fig. 1, the first architecture is named archi1; it is extended into archi2 whose components have to be refined. Architectures can be seen as a hierarchical tree whose leaves are behavioural components. Architectures may represent logical architectures or physical ones.

Extensions means that new behaviours are introduced into the design, for whatever reasons: the system is too complex to be defined in one shot, the client changes is mind, there is an already developed COTS whose specification is closed of the required one that could be integrated with lower cost, a product line has already be tested and its enhancement is expected by introducing new requirements, and so on.

Refinements aim at adding details and reducing non-determinism in order to get a concrete model closer to the final implantation of the system.

Developments of components may be processed by separate teams, by means of a collaborative platform, that increase the complexity of the process. One main concern of component designers is to develop components that meet their specification. Components are supposed to be defined for a given context, except that this context is evolving since it is itself under development. One goal of the architect is to verify the behavioural consistency of the models being developed. This task is critical since sub-systems have their own development life cycle. Nevertheless, the architect cannot wait until the final implantation model to check the consistency analysis of the system. He/she has to maintain the functional consistency of the system model under development whatever the abstractions of sub-system models. We characterize consistency by the following properties:

  • conformance: the behavioural specification of the architecture that is deduced from the interaction of its components fulfils the mandatory parts of the specification [6].

  • interoperability: the system is deadlock free; whatever point of interaction may be reached, communication will not be blocked and each part will reach one of its final states [7].

Architectures and behavioural components are defined from an external point of view, by a set of ports useful for establishing connections and a set of interfaces defining required and provided operations (or services). In order to illustrate concepts of architecture modelling, we will take as example the V76 case study proposed by [8], which is a simplified version of the protocol described in the ITU V.76 recommendation, based on LAPM (Link Access Procedure for Modems). Figure 2a represents an abstract external view of an architecture named V76-DL which represents the communication between two components that implement the protocol V76 and Fig. 2b is a more detailed external view.

Fig. 2
figure 2

External view of two points of view of architecture V76-DL

Full size image

The internal view of an architecture is defined by its components and their interconnections. For example, Fig. 3 illustrates the internal view of architecture V76-DL: it is constituted with two components of type V76 whose external view is given in Fig. 4. The architecture allows two users to communicate through the ports u1 and u2.

Fig. 3
figure 3

Internal view of architecture V76-DL

Full size image
Fig. 4
figure 4

External view of component V76

Full size image

The internal view of a behavioural component is defined by a behavioural specification defined according to its ports, the operations of its external view and private internal operations. Many formalisms may be used for behavioural specification depending on the system features and the progress of the development: sequence diagrams, state machines, functional flow block diagrams. For example, Fig. 5a shows a simplified specification of the architecture V76-DL from the transmitting user point of view and Fig. 5b shows the state machine of component V76 belonging to architecture V76-DL.

Fig. 5
figure 5

Behavioural specifications: a sequence diagram associated with the abstract architecture V76-DL, b state machine of component V76

Full size image

Analysing the consistency of an architecture during its development requires specific mechanisms and tools that are usually not proposed by CASE (Computer-Aided Software Engineering) tools. These mechanisms are divided into two groups:

  • model verifications: adequate relations have to be defined to capture conformance, refinement, extension and interoperability

  • model abstraction: adequate models have to be set up from the model under construction in order to capture behavioural specification from an external point of view and an appropriate abstraction in order to compare models defined at different abstraction levels.

These mechanisms are defined according to liveness properties that have to be preserved during development. This property is the liveness. Next section gives definition of liveness and motivates this choice.

3 The Use of Liveness and Abstraction as a Design Guideline

Liveness and safety properties allow systems to be analysed with respect to their behavioural specification as observed by their environment. This behaviour is observed by traces which are partial sequences of interactions (events or actions) starting from the initial state of the system. There are several ways to define safety and liveness, some of them being contradictory about the classification of deadlock property. We have selected definitions proposed by [9]: a safety property asserts that the system always stays within some allowed set of finite behaviours, in which nothing “bad” happens. The violation of such properties occurs after a finite execution of the system. A liveness property asserts that the system eventually reaches a good set of states, that means it will eventually react as it should after some given traces. A liveness property represents what the system must do, while a safety represents what the system has not to do. When reasoning on models, liveness properties can only be established under some fairness assumption, stating that the system is not allowed to continuously favour certain choices at the expense of others [10]. The fairness assumption implies that the system will eventually accept an event occurring infinitely often. Lastly, we consider that deadlock freedom is a liveness property, as proposed in [11] since a deadlock means that the system refuses any input event.

Many formal methods addressing complex system development advocate refinement techniques [12, 13] such as B method [14] or Object-Z [15]. They focus on the preservation of safety properties all along the process of development. Such methods are adequate when the specification of the component or the complete system is definitive and not being defined or evolved. Another way to support designers during model development is to preserve the liveness properties as mentioned in [16]: liveness properties act as a design guideline for developing systems.

Liveness is crucial for reactive systems and is complementary to safety to support designers during an incremental development: observing liveness allows specification to be enriched, starting from a “draft” model that is completed by a stepwise approach in a non-regressive way.

It is therefore necessary to provide designers with tools to compare models according to their liveness properties, taking into account that they sub-components can be defined at different abstraction levels. For example, how ensuring that architecture V76-DL fulfils the behavioural specification expressed by the sequence diagram? Are components of architecture V76-DL interoperable?

To answer these questions, we have defined two mechanisms: model abstraction and model analysis based on a liveness analysis.

3.1 Model Abstraction

With model abstraction, a simplified behaviour is extracted from models to be analysed. This extraction takes into account several criteria: the abstraction levels of models to be compared, the type of relation to be analysed (extension, refinement or interoperability), and of course, the goal of the analysis that is based on the analysis of the interaction of system (or one of its sub-system) and its environment. Abstract models are formalised by LTS (Labelled Transition System) [17]. Reasoning on such a formalism has many advantages: the system analysis is independent from the modelling formalism chosen by the designer; models can thus be compared even if their application domain is different, that is usual in System Engineering; existing relations already defined on LTS can be used for our purpose.

We do not formally introduce LTS and the process to abstract state machines into LTS. You can refer to [18] and [19] to get details about the transformation. Figure 6a illustrates the LTS generated from the state machine of component V76, and Fig. 6b the LTS associated with the sequence diagram of the architecture V76-DL. The transformation does not handle data; it only focuses on provided and required events (or services) offered by the component under analysis. When the component is an architecture, we have defined a transformation [20] which computes all combinations of internal events between components and reduces the LTS to observable events by hiding internal synchronisations and internal operations. Hidden actions are noted i in the LTS. For example, the LTS associated with the architecture of Fig. 3 handles operations defined on its interfaces given in Fig. 2b. Operations defined on interfaces of internal components, that is interfaces DataLinkIN and DataLinkOUT, are hidden. The LTS is built by synchronising the two LTS of Fig. 6 on their internal connector. It contains 84 transitions and 54 states.

Fig. 6
figure 6

a LTS associated with the state machine of component V76, b LTS associated with the sequence diagram of the simplified specification of architecture V76-DL

Full size image

When models to be compared do not belong to the same abstraction level, their interfaces may be different. For example, there are more operations in interfaces of component V76-DL than those of the specification of V76 protocol given by the sequence diagram. Comparison needs to align the abstraction levels. For this purpose, we use a hiding mechanism and a renaming mechanism, when operations are refined. For example, to compare V76-DL and the sequence diagram, internal operations of the architecture ( ua , i , sabme , and disc ) are hidden such as the operations belonging to the port u 2, which correspond with the user receiving the data. By this mechanism, the LTS associated with V76-DL architecture will be comparable to the abstract specification.

The main feature of this abstract model is that it captures what the system must do and what the system may do. That is crucial for liveness properties as we point out below.

3.2 Liveness Analysis

There exists a specific relation, which lonely goal is to preserve liveness. This relation is conformance relation conf [21, 22]. Conformance testing methodologies proposed by ISO and ETSI [6] are designed to compare an implementation model with a standard specification. Standard specifications or recommendations serve to define both the mandatory and optional parts. The main idea behind conformance is to verify agreement between an implementation and its specification on required parts; informally speaking, an implementation conforms to a standard if it has properly implemented all mandatory parts of the standard [23].

For instance, in Fig. 7, we can deduce the following properties:

  • spec1, spec2 and spec4 may accept releaseREQ or connectREQ after a sequence of connectREQ . As they may also refuse them, operations releaseREQ or connectREQ are optional.

  • spec3 must accept releaseREQ after connectREQ . releaseREQ is thus mandatory after the trace connectREQ .

Fig. 7
figure 7

Example of conf relation

Full size image

We can verify: spec1 conf spec2, spec2 conf spec1, spec1 conf spec4. However, spec1 \( {{\slash\!\!\!{\text{conf}}}} \) spec3: from an observational standpoint, nothing distinguishes spec1 from spec3 but conf relation detects non-determinism of spec3. In this example, spec1 may refuse releaseREQ after a non-empty unbounded occurrences of connectREQ , whereas spec3, which is deterministic, cannot. spec1 and spec3 are trace equivalent, yet not in conformance. Lastly, even if spec1 conf spec4 and spec4 conf spec1, we can verify that spec4 cannot substitute spec1.

Even though the conformance relation has been defined by [22], we are still not aware of any published method to compute it. We have thus proposed an implantation of this relation and pointed out how extension and refinement relations can be defined from the conformance relation [19, 24]. In the same way, we have implemented the procedure allowing to check if a component can substitute another one, whatever its environment may be [20].

Next section gives an overview of the tool IDCM we have defined and implemented to provide designers with a tool box to analyse models.

4 IDCM: Incremental Development of Compliant Models

IDCM is a tool box allowing models to be compared with respect to refinement, extension and substitution relations. It is based on concepts of IDF focusing on the analysis of liveness properties and abstraction of behavioural/functional models. It is developed in Java. Its first release is integrated into TopCased environment [25] and focus on UML state machines and composite component analysis. When a model is loaded for verification, the set of its components is proposed to be abstracted into LTS (see Fig. 8).

Fig. 8
figure 8

Interface to transform behavioural and architectural components into LTS

Full size image

Behavioural component transformation is performed by an ad hoc algorithm we have developed by parsing state machine xmi models. Composite components transformation is done with two stages: the first one produces an intermediate file in EXP.OPEN format [26] that is obtained by parsing composite component xmi models; the second stage, consisting in transforming the intermediate file into LTS, is performed by the CADP toolbox [27]. LTS associated with state machines and composite components are generated into CADP textual and binary formats [27].

IDCM proposes a set of relations for model comparison. They are classified in several families: relations for incremental development (extension or refinement), relation for liveness verification to check the conformance between an implantation and its specification, relations for assembling sub-components (compatibility) and lastly, relations to check if a component can substitute another one. When a relation between two models does not hold, a verdict is given as a sequence of observable events leading to a failure. Designers are in charge to analyse the trace, to execute it on the state machine, or in the architecture in order to find the mistake and correct it. For example, we have found a mistake (Fig. 9) in the state machine of component V76 by comparing the architecture with its abstract specification. There exists a deadlock after the action connectREQ when the two users send together a connectREQ . We have corrected this mistake by adding a state and transitions between wait – eu and wait – establish states in the state machine of Fig. 5b.

Fig. 9
figure 9

Verdict of the conformance between the architecture V76-DL and its abstract specification

Full size image

5 Conclusion

Developing complex systems requires methodologies such as MDA and System Engineering. Nevertheless, there is an actual difficulty for designers and architects for evaluating the behaviour of a system being designed during its development. We have thus proposed a framework supported by a tool allowing models to be developed through a stepwise methodology using extensions, refinements and substitutions. The development guarantees the liveness properties of the system. Our proposal is thus complementary to approaches of safety analysis that must also be performed during the development of critical systems.

Our future work plans to extend the model transformation to other functional formalisms than state machines such as sequence diagrams and eFFBD (enhanced functional block diagram). We are also defining a UML profile for incremental development.