peer reviewed

peer reviewed

This tool paper presents the design and tool-support of Messir, an approach centered on textual domain-specific languages supported by our open-source UML requirements engineering tool, named Excalibur. The novelty of our approach is the actual integration in a single workbench (Excalibur) of textual DSLs richly covering the requirements and analysis phases, i.e. improved use-cases, environment, conceptual and operations models; and the read-only visualisation of the requirements with UML-compliant views; and the generation of scientific requirements analysis documents in LATEX; and the formal simulation of test cases requirements.

Today computer systems are becoming very complex and often depending on some off-the-shelf components or external service providers. Validating the security aspects of these systems is a highly challenging goal, especially when we target security critical systems where guarantees must be provided on the robustness of the produced systems. Model Driven Engineering (MDE) is becoming popular and well accepted in both academia and critical systems industry. In our work, we aim to propose a novel MDE compliant security validation methodology based on architecture model based testing. In this paper, we focus on security modeling for improving the testability of the architecture models and facilitating the evaluation of the proposed test generation and selection methods. More specifically, we are interested in extending the SAE standard AADL [1] to improve the quality of the security test cases generated from AADL models.

SPLACID is a semi-formal language conceived for the specification and synthesis of (advanced) transactional models from basic features, such as transaction types and (relaxed) ACID variants. SPLACID is an improvement of the ACTA framework offering a well-structured and formal syntax. Neither ACTA nor SPLACID, however, benefit from a formal tool-supported semantics. This paper presents the first step for having a full formal semantics of SPLACID by translation to Alloy. In particular, we present the translation of the SPLACID concepts into Alloy concepts focusing on those concepts pertaining to the structure of a Transactional Model and those characterizing the isolation variant. The Alloy specification obtained by this translation preserve the SPLACID main key-properties, namely, modularity, flexibility and reusability. To support this claim we show how flexible, modular and reusable structures and isolation variants can be obtained in Alloy. Finally, we analyze the flat and nested transactional model structures and the serializability-based isolation variant using the Alloy Analyzer.

Flexibility, autonomy, distribution and openness of the modern computing systems are properties which expand the spectrum of interactions possible among system components. Moreover these properties tend to impose more rigorous quality requirements on software development. To ensure the quality of distributed applications two notions have already been introduced: concurrency control and fault-tolerance. These notions are present and refined in so-called advanced transactional frameworks. All these frameworks have different interpretations of these two notions because they try to solve different issues. Engineering from scratch such a framework is a complex task which will achieve a low level result, if not supported by a quality oriented approach. This paper solves this issue by introducing a product line perspective founded on the semantic analysis of the variabilities and commonalities of the ACID (atomicity, isolation, durability and consistency) properties. Varying and composing ACID properties in a disciplined way is in our opinion a key issue to increase quality and quality reuse in the development of advanced transactional frameworks. For this our approach allows the elicitation of the requirements of the advanced transactional frameworks product line using the "DRET" template.

ACID (Atomicity, Consistency, Isolation and Durability) properties characterize the initial transactional model (TM). Being too restrictive and functionally limited to face the requirements of more recent application domains, the semantics of these properties has been relaxed (weakened) leading to an important set of TMs. Understanding, comparing and synthesizing TMs on the basis of core features and, more specifically, understanding and comparing relaxed ACID properties to be able to reuse them, during the synthesis of TMs, is still an unreached goal. The ACTA framework represented a relevant step towards the achievement of that goal. ACTA, however, as we contribute in highlighting, presents several points of weakness. To contribute in easing the identification and specification of reusable and composable commonalities and variabilities among TMs, we introduce a software product line oriented, ACTA-based, language, called SPLACID. SPLACID is dedicated to the formal specification of TMs in terms of the selection and specialisation of a set of TM standard features. SPLACID promotes reuse and enhance rigor and precision by providing a well structured concrete syntax.

Product derivation, i.e. reusing core assets to build products, did not receive sufficient attention from the product-line community, yielding a frustrating situation. On the one hand, automated product derivation approaches are inflexible; they do not allow products meeting unforeseen, customer-specific, requirements. On the other hand, approaches that consider this issue do not provide adequate methodological guidelines nor automated support. This paper proposes an integrated product derivation approach reconciling the two views to offer both flexibility and automation. First, we perform a pre-configuration of the product by selecting desired features in a generic feature model and automatically composing their related product-line core assets. Then, we adapt the pre-configured product to its customer-specific requirements via derivation primitives combined by product engineers and controlled by constraints that flexibly set product line boundaries. Our process is supported by the Kermeta meta modeling environment and illustrated through an example.

Coordinated Atomic Actions (CAAs) have been introduced about ten years ago as a conceptual framework for developing fault-tolerant concurrent systems. All the work done since then extended the CAA framework with the capabilities to model, verify, and implement concurrent distributed systems following pre-defined development methodologies. As a result, CAAs, compared to other approaches available, offer a rich set of means for engineering dependable systems. Nevertheless, it is sometimes difficult to have a global and analytical view of all the features available as this concept provides a number of features which need to be applied in combination. The main contribution of this paper is in presenting a complete state-of-the-art overview of the work done around CAAs from the three perspectives: the definitions of the fundamental concepts, their various semantics and the means supporting formal verification. This paper is useful for the potential CAAs users in helping them to avoid misinterpretation when employing all the available features. Finally, our paper should contribute in better understanding of the likely directions in which the CAA framework may evolve in the near future.

Fault tolerance engineering has been advocated as one of the main approaches to ensuring the overall system dependability. The 2nd International Workshop on Engineering Fault Tolerant Systems (EFTS 2007) aims to investigate how fault tolerance mechanisms can be taken into account when engineering complex software systems and to improve our understanding of where and how fault-tolerance should be integrated in the software life-cycle. The focus of the workshop is on developing novel models to be applied at different abstraction levels (requirements, architecture and design models for fault tolerance, together with new implementation schemes), innovative technologies (tools and frameworks for implementing distributed fault tolerant systems) and advanced verification environments (to assess the achieved level of fault tolerance and to evaluate the dependability properties of the systems). Recently there has been a growing interest in the areas directly related and overlapping with fault tolerance, such as self-healing, resilience, self-adaptation and self-management. The topics related to engineering of systems with such properties are in the scope of the workshop as the intention is to improve the current understanding of how fault tolerance engineering can benefit from research on these areas.

This paper presents an implementation framework, called CAA-DRIP, that has been defined to allow a straightforward implementation of dependable distributed applications designed using the coordinated atomic action (CAA) paradigm. CAAs provide a coherent set of concepts adapted to the design of fault tolerant distributed systems that includes: structured transactions, distribution, cooperation, competition, and forward and backward error recovery mechanisms triggered by exceptions. DRIP (dependable remote interacting processes) is an efficient Java implementation framework, which provides support for implementing "dependable multiparty interactions (DMI)" which includes a general exception handling mechanism. As DMI has a softer exception handling semantics with respect to CAA semantics, a CAA design can be implemented by DRIP. The aim of the CAA-DRIP framework is to provide a set of Java classes that allows programmers to implement only the semantics of CAAs with the same terminology and concepts at the design and implementation levels. The new framework simplifies the implementation phase and at the same time reduces the size of the final system since it requires fewer number of instances for creating a CAA at runtime. Details of these improvements as well as a precise description of the CAAs behaviour in terms of state charts, which is used as a reference model to define the CAA-DRIP framework, are presented in this paper

The lack of a precise semantics for UML activity diagrams makes the reasoning on models constructed using such diagrams infeasible. However, such diagrams are widely used in domains that require a certain degree of confidence. Due to economical interests, the business domain is one of these. To enhance confidence level of UML activity diagrams, this paper provides a formal definition of their syntax and semantics. The main interest of our approach is that we chose UML activity diagrams, which are recognized to be more tractable by engineers, and we extend them with timing constraints. We outline the translation of our semantics into the PROMELA input language of the SPIN model checker which can be used to check several properties.

In this paper, we present the Concurrent Object-Oriented Petri Nets (CO-OPN/2) formalism devised to support the specification of large distributed systems. Our approach is based on two underlying formalisms: order-sorted algebra and algebraic Petri nets. With respect to the lack of structuring capabilities of Petri nets, CO-OPN/2 has adopted the object-oriented paradigm. In this hybrid approach (model- and property-oriented), classes of objects are described by means of algebraic Petri nets, while data structures are expressed by order-sorted algebraic specifications. An original feature is the sophisticated synchronization mechanism. This mechanism allows to involve many partners in a synchronization and to describe the synchronization policy. A typical example of distributed systems, namely the Transit Node, is used throughout this paper to introduce our formalism and the concrete specification language associated with it. By successive refinements of the components of the example, we present, informally, most of the notions of CO-OPN/2. We also give some insights about the coordination layer, Context and Objects Interface Language (COIL), which is built on top of CO-OPN/2. This coordination layer is used for the description of the concrete distributed architecture of the system. Together, CO-OPN/2 and COIL provide a complete formal framework for the specification of distributed systems.

The rapid expansion of Java programs into the software market is often not supported by a proper development methodology. We present a formal development methodology, well suited for Java dependable distributed applications. It is based on the stepwise refinement of model oriented formal specifications, and enables validation of the obtained system wrt the client's requirements. Three refinement steps have been identified in the case of fault tolerant distributed applications: first, starting from informal requirements, an initial formal specification is derived. It does not depend on implementation constraints and provides a centralized solution; second, dependability and distribution constraints are integrated; third, the Java implementation is realised. The CO-OPN/2 language is used to express specifications formally; and the dependability and distribution design as based on the Coordinated Atomic action concept. The methodology and the three refinement steps are presented through a very simple fault tolerant distributed Java application.