Refinement and verification in component-based model-driven design

Modern software development is complex as it has to deal with many different and yet related aspects of applications. In practical software engineering this is now handled by a UML-like modelling approach in which different aspects are modelled by different notations. Component-based and object-oriented design techniques are found effective in the support of separation of correctness concerns of different aspects. These techniques are practised in a model-driven development process in which models are constructed in each phase of the development. To ensure the correctness of the software system developed, all models constructed in each phase are verifiable. This requires that the modelling notations are formally defined and related in order to have tool support developed for the integration of sophisticated checkers, generators and transformations. This paper summarises our research on the method of Refinement of Component and Object Systems (rCOS) and illustrates it with experiences from the work on the Common Component Modelling Example (CoCoME). This gives evidence that the formal techniques developed in rCOS can be integrated into a model-driven development process and shows where it may be integrated in computer-aided software engineering (CASE) tools for adding formally supported checking, transformation and generation facilities.     

The Real-Time Process Algebra (RTPA)

The real-time process algebra (RTPA) is a set of new mathematical notations for formally describing system architectures, and static and dynamic behaviors. It is recognized that the specification of software behaviors is a three-dimensional problem known as: (i) mathematical operations, (ii) event/process timing, and (iii) memory manipulations. Conventional formal methods in software engineering were designed to describe the 1-D (type (i)) or 2-D (types (i) and (iii)) static behaviors of software systems via logic, set and type theories. However, they are inadequate to address the 3-D problems in real-time systems. A new notation system that is capable to describe and specify the 3-D real-time behaviors, the real-time process algebra (RTPA), is developed in this paper to meet the fundamental requirements in software engineering.RTPA is designed as a coherent software engineering notation system and a formal engineering method for addressing the 3-D problems in software system specification, refinement, and implementation, particularly for real-time and embedded systems. In this paper, the RTPA meta-processes, algebraic relations, system architectural notations, and a set of fundamental primary and abstract data types are described. On the basis of the RTPA notations, a system specification method and a refinement scheme of RTPA are developed. Then, a case study on a telephone switching system is provided, which demonstrates the expressive power of RTPA on formal specification of both software system architectures and behaviors. RTPA elicits and models 32 algebraic notations, which are the common core of existing formal methods and modern programming languages. The extremely small set of formal notations has been proven sufficient for modeling and specifying real-time systems, their architecture, and static/dynamic behaviors in real-world software engineering environment.     

Alliance of model-driven engineering with a proof-based formal approach

Model-driven engineering (MDE) promotes the use of models throughout the software development cycle in order to increase abstraction and reduce software complexity. It favors the definition of domain-specific modeling languages (DSMLs) thanks to frameworks dedicated to meta-modeling and code generation like EMF (Eclipse Modeling Framework). The standard semantics of meta-models allows interoperability between tools such as language analysers (e.g., XText), code generators (e.g., Acceleo), and also model transformation tools (e.g., ATL). However, a major limitation of MDE is the lack of formal reasoning tools allowing to ensure the correctness of models. Indeed, most of the verification activities offered by MDE tools are based on the verification of OCL constraints on instances of meta-models. However, these constraints mainly deal with structural properties of the model and often miss out its behavioral semantics. In this work, we propose to bridge the gap between MDE and the rigorous world of formal methods in order to guarantee the correctness of both structural and behavioral properties of the model. Our approach translates EMF meta-models into an equivalent formal B specification and then injects models into this specification. The equivalence between the resulting B specification and the original EMF model is kept by proven design steps leading to a rigorous MDE technique. The AtelierB prover is used to guarantee the correctness of the model’s behavior with respect to its invariant properties, and the ProB model-checker is used to animate underlying execution scenarios which are translated back to the initial EMF model. Besides the use of these automatic reasoning tools in MDE, proved B refinements are also investigated in this paper in order to gradually translate abstract EMF models to concrete models which can then be automatically compiled into a programming language.

     

Foundations of a new software engineering method for real-time systems

The design of a fault-tolerant distributed, real-time, embedded system with safety-critical concerns requires the use of formal languages. In this paper, we present the foundations of a new software engineering method for real-time systems that enables the integration of semiformal and formal notations. This new software engineering method is mostly based upon the ”COntinuuM” co-modeling methodology that we have used to integrate architecture models of real-time systems (Perseil and Pautet in 12th International conference on engineering of complex computer systems, ICECCS, IEEE Computer Society, Auckland, pp 371–376, 2007) (so we call it “Method C”), and a model-driven development process (ISBN 978-0-387-39361-2 in: From model-driven design to resource management for distributed embedded systems, Springer, chap. MDE benefits for distributed, real time and embedded systems, 2006). The method will be tested in the design and development of integrated modular avionics (IMA) frameworks, with DO178, DO254, DO297, and MILS-CC requirements.     

TALISMAN MDE: Mixing MDE principles

The Model-Driven Engineering approach is progressively gaining popularity in the software engineering community as it raises the level of abstraction in software development. In TALISMAN MDE framework, we combine the principles of the two most important initiatives, Model-Driven Architecture and Software Factories. Both have their pros and cons, and we select the best from each in TALISMAN MDE. To show the advantages of TALISMAN MDE, we have developed a systems generator and used it to create applications for controlling food traceability. The applications are being used in dairies with different manufacturing processes, using software developed specifically for each dairy by working only with models, without additional programming.     

Formalising natural language specifications using a cognitive linguistic/configuration based approach

This paper addresses the problem of transforming business specifications written in natural language into formal models suitable for use in information systems development. It proposes a method for transforming controlled natural language specifications based on the Semantics of Business Vocabulary and Business Rules standard. This approach is unique in combining techniques from Model-Driven Engineering (MDE), Cognitive Linguistics, and Knowledge-based Configuration, which allows the reliable semantic processing of specifications and integration with existing MDE tools to improve productivity, quality, and time-to-market in software development. The method first learns the vocabulary of the specification from glossary-like definitions then parses the rules of the specification and outputs the resulting formal SBVR model. Both aspects of the method are tested separately, with the system correctly learning 98% of the vocabulary and correctly interpreting 98% of the rules of an SBVR SE based example. Finally, the proposed method is compared to state-of-the-art approaches for creating formal models from natural language specifications, arguing that it meets the criteria necessary to fulfil the three goals of (1) shifting control of specification to non-technical business experts, (2) reducing the manual effort involved in formalising specifications, and (3) supporting business experts in creating well-formed sets of business vocabularies and rules.     

Slicing ATL model transformations for scalable deductive verification and fault localization

Model-driven engineering (MDE) is increasingly accepted in industry as an effective approach for managing the full life cycle of software development. In MDE, software models are manipulated, evolved and translated by model transformations (MT), up to code generation. Automatic deductive verification techniques have been proposed to guarantee that transformations satisfy correctness requirements (encoded as transformation contracts). However, to be transferable to industry, these techniques need to be scalable and provide the user with easily accessible feedback. In MT-specific languages like ATL, we are able to infer static trace information (i.e., mappings among types of generated elements and rules that potentially generate these types). In this paper, we show that this information can be used to decompose the MT contract and, for each sub-contract, slice the MT to the only rules that may be responsible for fulfilling it. Based on this contribution, we design a fault localization approach for MT, and a technique to significantly enhance scalability when verifying large MTs against a large number of contracts. We implement both these algorithms as extensions of the VeriATL verification system, and we show by experimentation that they increase its industry readiness.     

Repository support for multi-perspective requirements engineering

Relationships among different modeling perspectives have been systematically investigated focusing either on given notations (e.g. UML) or on domain reference models (e.g. ARIS/SAP). In contrast, many successful informal methods for business analysis and requirements engineering (e.g. JAD) emphasize team negotiation, goal orientation and flexibility of modeling notations. This paper addresses the question how much formal and computerized support can be provided in such settings without destroying their creative tenor. Our solution is based on a novel modeling language, M-Telos, that integrates the adaptability and analysis advantages of the logic-based meta modeling language Telos with a module concept covering the structuring mechanisms of scalable software architectures. It comprises four components: (1) A modular conceptual modeling formalism organizes individual perspectives and their interrelationships. (2) Perspective schemata are linked to a conceptual meta meta model of shared domain terms, thus giving the architecture a semantic meaning and enabling adaptability and extensibility of the network of perspectives. (3) Inconsistency management across perspectives is handled in a goal-oriented manner, by formalizing analysis goals as meta rules which are automatically customized to perspective schemata. (4) Continuous incremental maintenance of inconsistency information is provided by exploiting recent view maintenance techniques from deductive databases. The approach has been implemented as an extension to the ConceptBase³ meta database management system and has been applied in a number of real-world requirements engineering projects.     

Formal verification of static software models in MDE: A systematic review

ContextModel-driven Engineering (MDE) promotes the utilization of models as primary artifacts in all software engineering activities. Therefore, mechanisms to ensure model correctness become crucial, specially when applying MDE to the development of software, where software is the result of a chain of (semi)automatic model transformations that refine initial abstract models to lower level ones from which the final code is eventually generated. Clearly, in this context, an error in the model/s is propagated to the code endangering the soundness of the resulting software. Formal verification of software models is a promising approach that advocates the employment of formal methods to achieve model correctness, and it has received a considerable amount of attention in the last few years.ObjectiveThe objective of this paper is to analyze the state of the art in the field of formal verification of models, restricting the analysis to those approaches applied over static software models complemented or not with constraints expressed in textual languages, typically the Object Constraint Language (OCL).MethodWe have conducted a Systematic Literature Review (SLR) of the published works in this field, describing their main characteristics.ResultsThe study is based on a set of 48 resources that have been grouped in 18 different approaches according to their affinity. For each of them we have analyzed, among other issues, the formalism used, the support given to OCL, the correctness properties addressed or the feedback yielded by the verification process.ConclusionsOne of the most important conclusions obtained is that current model verification approaches are strongly influenced by the support given to OCL. Another important finding is that in general, current verification tools present important flaws like the lack of integration into the model designer tool chain or the lack of efficiency when verifying large, real-life models.     

On the use of models for high-performance scientific computing applications: an experience report

This paper reports on a four-year project that aims to raise the abstraction level through the use of model-driven engineering (MDE) techniques in the development of scientific applications relying on high-performance computing. The development and maintenance of high-performance scientific computing software is reputedly a complex task. This complexity results from the frequent evolutions of supercomputers and the tight coupling between software and hardware aspects. Moreover, current parallel programming approaches result in a mixing of concerns within the source code. Our approach relies on the use of MDE and consists in defining domain-specific modeling languages targeting various domain experts involved in the development of HPC applications, allowing each of them to handle their dedicated model in a both user-friendly and hardware-independent way. The different concerns are separated thanks to the use of several models as well as several modeling viewpoints on these models. Depending on the targeted execution platforms, these abstract models are translated into executable implementations by means of model transformations. To make all of these effective, we have developed a tool chain that is also presented in this paper. The approach is assessed through a multi-dimensional validation that focuses on its applicability, its expressiveness and its efficiency. To capitalize on the gained experience, we analyze some lessons learned during this project.     

Literate Specification: Using Design Rationale to Support Formal Methods in the Development of Human-Machine Interfaces

The design of safety-critical user interfaces is typically very different from that of many other applications. Reactor control systems and aircraft cockpits are complex and dynamic, open to input from many different users and devices. A number of formal notations, including Z and temporal logic, have been developed to address these problems. They provide precise and concise means of representing a potential design before designers incur the expense of implementation. Consequently, government bodies and commercial organizations have recommended that these techniques be used when tendering for their contracts. However, there are a number of limitations that restrict the use of mathematical specifications for interface development in large scale projects. In particular, formal notations cannot easily be used to coordinate the activities of human factors and systems engineering teams. This creates particular difficulties if some group members have only a limited understanding of discrete mathematics. A further problem is that the development of a safety-critical application may take many months, or even years, to complete. This creates difficulties because abstract mathematical specifications cannot be used easily by new members of a development team to understand past design decisions. To avoid these limitations I have developed a literate approach to interface specification. This technique uses a formal development language and a semiformal design rationale to support the design of safety-critical user interfaces.     

Executable visual software modeling—the ZOOM approach

In this paper, we introduce a new executable visual software modeling approach called ZOOM (Z-Based Object Oriented Modeling). ZOOM extends a subset of UML-2 notations by providing UI modeling notations and a formal integration mechanism. ZOOM allows software modeling using both graphical and textual views for its structural, behavioral and UI models. Through a pre-defined event model, ZOOM integrates these models, and provides the runtime execution semantics for both code generation and software animation.     

On the application of model-driven engineering in data reengineering

Model-Driven Engineering (MDE) emphasizes the systematic use of models to improve software productivity and some aspects of the software quality such as maintainability or interoperability. Model-driven techniques have proven useful not only as regards developing new software applications but also the reengineering of legacy systems. Models and metamodels provide a high-level formalism with which to represent artefacts commonly manipulated in the different stages of a software evolution process (e.g., a software migration) while model transformation allows the automation of the evolution tasks to be performed. Some approaches and experiences of model-driven software reengineering have recently been presented but they have been focused on the code while data reengineering aspects have been overlooked. The objective of this work is to assess to what extent data reengineering processes could also take advantage of MDE techniques.The article starts by characterising data-reengineering in terms of the tasks involved. It then goes on to state that MDE is particularly amenable as regards addressing the tasks previously identified. We present an MDE-based approach for the reengineering of data whose purpose is to improve the quality of the logical schema in a relational data migration scenario. As a proof of concept, the approach is illustrated for two common problems in data re-engineering: undeclared foreign keys and disabled constraints. This approach is organised following the three stages of a software reengineering process: reverse engineering, restructuring and forward engineering. We show how each stage is implemented by means of model transformation chains. A running example is used to illustrate each stage of the process throughout the article. The approach is validated with a real widely-used database. An assessment of the application of MDE in each stage is then presented, and we conclude by identifying the main benefits and drawbacks of using MDE in data reengineering.     

A Generalized Structural Model of Structured Programs for Software Metrics Definition

There are many different types of models to describe various aspects of software from inception to completion. Some of these models are the basis for defining software metrics. In this paper, we propose a generalized formal structural model for traditional structured programs such as 3/4 GLs. We provide a formal definition using conventional notations for our proposed model covering information flow, control flow and combination of information and control flows.     

Reengineering component-based software systems with Archimetrix

Many software development, planning, or analysis tasks require an up-to-date software architecture documentation. However, this documentation is often outdated, unavailable, or at least not available as a formal model which analysis tools could use. Reverse engineering methods try to fill this gap. However, as they process the system’s source code, they are easily misled by design deficiencies (e.g., violations of component encapsulation) which leaked into the code during the system’s evolution. Despite the high impact of design deficiencies on the quality of the resulting software architecture models, none of the surveyed related works is able to cope with them during the reverse engineering process. Therefore, we have developed the Archimetrix approach which semiautomatically recovers the system’s concrete architecture in a formal model while simultaneously detecting and removing design deficiencies. We have validated Archimetrix on a case study system and two implementation variants of the CoCoME benchmark system. Results show that the removal of relevant design deficiencies leads to an architecture model which more closely matches the system’s conceptual architecture.     

A model-driven engineering framework for embedded systems design

This work presents a Model-Driven Engineering (MDE) framework to improve embedded system design. The framework adopts concepts from MDE for the automatic generation of a control and data flow internal representation, starting from the functional specification of an embedded application described using UML class and sequence diagrams. By means of transformations rules applied on the UML model of the embedded system, an MOF-based (Meta Object Facility is a standard representation for meta-models and models proposed by OMG) internal representation is automatically obtained, which is iteratively mapped into a hardware/software implementation by means of model transformations. This mapping is optimized by a design space exploration (DSE) method based on a categorical graph product. The model transformations have also as input a platform model, which specifies the available hardware, software and interface resources, and produce an implementation model, on which software synthesis, communication synthesis and high-level synthesis algorithms are applied to generate the final implementation. A case study is described to illustrate the application of the framework.