Formal Aspects of Component Software

Frontmatter

Taming Distributed System Complexity through Formal Patterns

Abstract

Many current and future distributed systems are or will be:

• real-time and cyber-physical
• probabilistic in their operating environments and/or their algorithms
• safety-critical, with strong qualitative and quantitative formal requirements
• reflective and adaptive, to operate in changing and potentially hostile environments.

José Meseguer

Composing Safe Systems

Abstract

Failures in component-based systems are generally due to unintended or incorrect interactions among the components. For safety-critical systems, we may attempt to eliminate unintended interactions, and to verify correctness of those that are intended. We describe the value of partitioning in eliminating unintended interactions, and of assumption synthesis in developing a robust foundation for verification. We show how model checking of very abstract designs can provide mechanized assistance in human-guided assumption synthesis.

John Rushby

A Denotational Model for Component-Based Risk Analysis

Abstract

Risk analysis is an important tool for developers to establish the appropriate protection level of a system. Unfortunately, the shifting environment of components and component-based systems is not adequately addressed by traditional risk analysis methods. This paper addresses this problem from a theoretical perspective by proposing a denotational model for component-based risk analysis. In order to model the probabilistic aspect of risk, we represent the behaviour of a component by a probability distribution over communication histories. The overall goal is to provide a theoretical foundation facilitating an improved understanding of risk in relation to components and component-based system development.

Gyrd Brændeland, Atle Refsdal, Ketil Stølen

Synthesis of Hierarchical Systems

Abstract

In automated synthesis, given a specification, we automatically create a system that is guaranteed to satisfy the specification. In the classical temporal synthesis algorithms, one usually creates a “flat” system “from scratch”. However, real-life software and hardware systems are usually created using preexisting libraries of reusable components, and are not “flat” since repeated sub-systems are described only once.

In this work we describe an algorithm for the synthesis of a hierarchical system from a library of hierarchical components, which follows the “bottom-up” approach to system design. Our algorithm works by synthesizing in many rounds, when at each round the system designer provides the specification of the currently desired module, which is then automatically synthesized using the initial library and the previously constructed modules. To ensure that the synthesized module actually takes advantage of the available high-level modules, we guide the algorithm by enforcing certain modularity criteria.

We show that the synthesis of a hierarchical system from a library of hierarchical components is Exptime-complete for μ-calculus, and 2Exptime-complete for Ltl, both in the cases of complete and incomplete information. Thus, in all cases, it is not harder than the classical synthesis problem (of synthesizing flat systems “from scratch”), even though the synthesized hierarchical system may be exponentially smaller than a flat one.

Benjamin Aminof, Fabio Mogavero, Aniello Murano

A Modal Specification Theory for Components with Data

Abstract

Modal specification is a well-known formalism used as an abstraction theory for transition systems. Modal specifications are transition systems equipped with two types of transitions: must-transitions that are mandatory to any implementation, and may-transitions that are optional. The duality of transitions allows to develop a unique approach for both logical and structural compositions, and eases the step-wise refinement process for building implementations.

We propose Modal Specifications with Data (MSD), the first modal specification theory with explicit representation of data. Our new theory includes all the essential ingredients of a specification theory. As MSD are by nature potentially infinite-state systems, we propose symbolic representations based on effective predicates. Our theory serves as a new abstraction-based formalism for transition systems with data.

Sebastian S. Bauer, Kim Guldstrand Larsen, Axel Legay, Ulrik Nyman, Andrzej Wąsowski

Evaluating the Performance of Model Transformation Styles in Maude

Abstract

Rule-based programming has been shown to be very successful in many application areas. Two prominent examples are the specification of model transformations in model driven development approaches and the definition of structured operational semantics of formal languages. General rewriting frameworks such as Maude are flexible enough to allow the programmer to adopt and mix various rule styles. The choice between styles can be biased by the programmer’s background. For instance, experts in visual formalisms might prefer graph-rewriting styles, while experts in semantics might prefer structurally inductive rules. This paper evaluates the performance of different rule styles on a significant benchmark taken from the literature on model transformation. Depending on the actual transformation being carried out, our results show that different rule styles can offer drastically different performances. We point out the situations from which each rule style benefits to offer a valuable set of hints for choosing one style over the other.

Roberto Bruni, Alberto Lluch Lafuente

Interactive Transformations from Object-Oriented Models to Component-Based Models

Abstract

Consider an object-oriented model with a class diagram, and a set of object sequence diagrams, each representing the design of object interactions for a use case. This article discusses how such an OO design model can be automatically transformed into a component-based model for the purpose of reusability, maintenance, and more importantly, distributed and independent deployment. We present the design and implementation of a tool that transforms an object-oriented model to a component-based model, which are both formally defined in the rCOS method of model driven design of component-based software, in an interactive, stepwise manner. The transformation is designed using QVT Relations and implemented as part of the rCOS CASE tool.

Dan Li, Xiaoshan Li, Zhiming Liu, Volker Stolz

Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components

Abstract

Dynamic reconfigurations increase the availability and the reliability of component-based systems by allowing their architectures to evolve at runtime. Recently we have proposed a temporal pattern logic, called FTPL, to characterize the correct reconfigurations of component-based systems under some temporal and architectural constraints.

As component-based architectures evolve at runtime, there is a need to check these FTPL constraints on the fly, even if only a partial information is expected. Firstly, given a generic component-based model, we review FTPL from a runtime verification point of view. To this end we introduce a new four-valued logic, called RV-FTPL (Runtime Verification for FTPL), characterizing the “potential” (un)satisfiability of the architectural constraints in addition to the basic FTPL semantics. Potential true and potential false values are chosen whenever an observed behaviour has not yet lead to a violation or satisfiability of the property under consideration. Secondly, we present a prototype developed to check at runtime the satisfiability of RV-FTPL formulas when reconfiguring a Fractal component-based system. The feasability of a runtime property enforcement is also shown. It consists in supervising on the fly the reconfiguration execution against desired RV-FTPL properties. The main contributions are illustrated on the example of a HTTP server architecture.

Julien Dormoy, Olga Kouchnarenko, Arnaud Lanoix

Timed Conformance Testing for Orchestrated Service Discovery

Abstract

Orchestrations are systems deployed on the Internet where there is a central component (called orchestrator) coordinating other components (called Web services), pre-existing to the orchestration design phase. Web services are made available through repositories on the Internet to orchestration designers. Service discovery refers to the activity of identifying Web services offered by third parties. We propose an approach to discover Web services by taking into account the intended behaviors of Web services as they can be inferred from the orchestrator specifications. Web services are tested with respect to those behaviors to decide whether or not they can be selected. Specifications of orchestrators are Timed Input/Output Symbolic Transition Systems. Web service intended behaviors are elicited by means of symbolic execution and projection techniques. Those behaviors can be used as test purposes for our timed symbolic conformance testing algorithm.

Jose Pablo Escobedo, Christophe Gaston, Pascale Le Gall

Realizability of Choreographies for Services Interacting Asynchronously

Abstract

Choreography specification languages describe from a global point of view interactions among a set of services in a system to be designed. Given a choreography specification, the goal is to obtain a distributed implementation of the choreography as a system of communicating peers. These peers can be given as input (e.g., obtained using discovery techniques) or automatically generated by projection from the choreography. Checking whether some set of peers implements a choreography specification is called realizability. This check is in general undecidable if asynchronous communication is considered, that is, services interact through message buffers. In this paper, we consider conversation protocols as a choreography specification language, and leverage a recent decidability result to check automatically the realizability of these specifications by a set of peers under an asynchronous communication model with a priori unbounded buffers.

Gregor Gössler, Gwen Salaün

Networks of Real-Time Actors

Schedulability Analysis and Coordination

Abstract

We present an automata theoretic framework for modular schedulability analysis of networks of real-time asynchronous actors. In this paper, we use the coordination language Reo to structure the network of actors and as such provide an exogenous form of scheduling between actors to complement their internal scheduling. We explain how to avoid extra communication buffers during analysis in some common Reo connectors. We then consider communication delays between actors and analyze its effect on schedulability of the system. Furthermore, in order to have a uniform analysis platform, we show how to use Uppaalto combine Constraint Automata, the semantic model of Reo, with Timed Automata models of the actors. We can derive end-to-end deadlines, i.e., the deadline on a message from when it is sent until a reply is received.

Mohammad Mahdi Jaghoori, Ólafur Hlynsson, Marjan Sirjani

A Formal Model of Object Mobility in Resource-Restricted Deployment Scenarios

Abstract

Software today is often developed for deployment on different architectures, ranging from sequential machines via multicore and distributed architectures to the cloud. In order to apply formal methods, models of such systems must be able to capture different deployment scenarios. For this purpose, it is desirable to express aspects of low-level deployment at the abstraction level of the modeling language. This paper considers formal executable models of concurrent objects executing with user-defined cost models. Their execution is restricted by deployment components which reflect the execution capacity of groups of objects between observable points in time. We model strategies for object relocation between components. A running example demonstrates how activity on deployment components causes congestion and how object relocation can alleviate this congestion. We analyze the average behavior of models which vary in the execution capacity of deployment components and in object relocation strategies by means of Monte Carlo simulations.

Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa

The Logic of XACML

Abstract

We study the international standard XACML 3.0 for describing security access control policy in a compositional way. Our main contribution is to derive a logic that precisely captures the idea behind the standard and to formally define the semantics of the policy combining algorithms of XACML. To guard against modelling artefacts we provide an alternative way of characterizing the policy combining algorithms and we formally prove the equivalence of these approaches. This allows us to pinpoint the shortcoming of previous approaches to formalization based either on Belnap logic or on \(\mathcal{D}\)-algebra.

Carroline Dewi Puspa Kencana Ramli, Hanne Riis Nielson, Flemming Nielson

A Proof Assistant Based Formalization of MDE Components

Abstract

Model driven engineering (MDE) now plays a key role in the development of safety critical systems through the use of early validation and verification of models, and the automatic generation of software and hardware artifacts from the validated and verified models. In order to ease the integration of formal specification and verification technologies, various formalizations of the MDE technologies were proposed by different authors using term or graph rewriting, proof assistants, logical frameworks, etc.

The use of components is also mandatory to improve the efficiency of system development. Invasive Software Composition (ISC) has been proposed by A\(\ss\)man in [1] to add a generic component structure to existing Domain Specific Modeling Languages in MDE. This approach is the basis of the ReuseWare toolset.

We present in this paper an extension of a formal embedding of some key aspects of MDE in set theory in order to formalize ISC and prove the correctness of the proposed approach with respect to the conformance relation with the base metamodel. The formal embedding we rely on was developed by some of the authors, presented in [25] and then implemented using the Calculus of Inductive Construction and the Coq proof-assistant. This work is a first step in the formalization of composable verification technologies in order to ease its integration for DSML extended with component features using ISC.

Mounira Kezadri, Benoît Combemale, Marc Pantel, Xavier Thirioux

Controlling an Iteration-Wise Coherence in Dataflow

Abstract

This paper formalizes a data-flow component model specifically designed for building real-time interactive scientific visualization applications. The advantages sought in this model are performance, coherence and application design assistance. The core of the article deals with the interpretation of a property and constraint based user specification to generate a concrete assembly based on our component model. To fulfill one or many coherence constraints simultaneously, the application graph is processed, particularly to find the optimal locations of filtering objects called regulators. The automatic selection and inter-connection of connectors in order to maintain the requested coherences and the highest performance possible is also part of the process.

Sébastien Limet, Sophie Robert, Ahmed Turki

Learning from Failures: A Lightweight Approach to Run-Time Behavioural Adaptation

Abstract

Software integration needs to face signature and behaviour incompatibilities that unavoidably arise when composing services developed by different parties. While many of such incompatibilities can be solved by applying existing software adaptation techniques, these are computationally expensive and require to know beforehand the behaviour of the services to be integrated. In this paper we present a lightweight approach to dynamic service adaptation which does not require any previous knowledge on the behaviour of the services to be integrated. The approach itself is adaptive in the sense that an initial (possibly the most liberal) adaptor behaviour is progressively refined by learning from failures that possibly occur during service interaction.

José Antonio Martín, Antonio Brogi, Ernesto Pimentel

Verifying Safety of Fault-Tolerant Distributed Components

Abstract

We show how to ensure correctness and fault-tolerance of distributed components by behavioural specification. We specify a system combining a simple distributed component application and a fault-tolerance mechanism. We choose to encode the most general and the most demanding kind of faults, byzantine failures, but only for some of the components of our system. With Byzantine failures a faulty process can have any behaviour, thus replication is the only convenient classical solution; this greatly increases the size of the system, and makes model-checking a challenge. Despite the simplicity of our application, full study of the overall behaviour of the combined system requires us putting together the specification for many features required by either the distributed application or the fault-tolerant protocol: our system encodes hierarchical component structure, asynchronous communication with futures, replication, group communication, an agreement protocol, and faulty components. The system we obtain is huge and we have proved its correctness by using at the same time data abstraction, compositional minimization, and distributed model-checking.

Rabéa Ameur-Boulifa, Raluca Halalai, Ludovic Henrio, Eric Madelaine

Reducing the Model Checking Cost of Product Lines Using Static Analysis Techniques

Abstract

Software product line engineering is a paradigm to develop software applications using platforms and mass customization. Component based approaches play an important role in development of product lines: Components represent features, and different component combinations lead to different products. The number of combinations is exponential in the number of features, which makes the cost of product line model checking high. In this paper, we propose two techniques to reduce the number of component combinations that have to be verified. The first technique is using the static slicing approach to eliminate the features that do not affect the property. The second technique is analyzing the property and extracting sufficient conditions of property satisfaction/violation, to identify products that satisfy or violate the property without model checking. We apply these techniques on a vending machine case study to show the applicability and effectiveness of our approach. The results show that the number of generated states and time of model checking is reduced significantly using the proposed reduction techniques.

Hamideh Sabouri, Ramtin Khosravi

Bigraphical Modelling of Architectural Patterns

Abstract

Archery is a language for behavioural modelling of architectural patterns, supporting hierarchical composition and a type discipline. This paper extends Archery to cope with the patterns’ structural dimension through a set of (re-)configuration combinators and constraints that all instances of a pattern must obey. Both types and instances of architectural patterns are semantically represented as bigraphical reactive systems and operations upon them as reaction rules. Such a bigraphical semantics provides a rigorous model for Archery patterns and reduces constraint verification in architectures to a type-checking problem.

Alejandro Sanchez, Luís Soares. Barbosa, Daniel Riesco

Coordinated Execution of Heterogeneous Service-Oriented Components by Abstract State Machines

Abstract

Early design and validation of service-oriented applications is hardly feasible due to their distributed, dynamic, and heterogeneous nature. In order to support the engineering of such applications and discover faults early, foundational theories, modeling notations and analysis techniques for component-based development should be revisited. This paper presents a formal framework for coordinated execution of service-oriented applications based on the OSOA open standard Service Component Architecture (SCA) for heterogeneous service assembly and on the formal method Abstract State Machines (ASMs) for modeling notions of service behavior, interactions, and orchestration in an abstract but executable way. The proposed framework is exemplified through a Robotics Task Coordination case study of the EU project BRICS.

Davide Brugali, Luca Gherardi, Elvinia Riccobene, Patrizia Scandurra

Verifying Temporal Properties of Use-Cases in Natural Language

Abstract

This paper presents a semi-automated method that helps iteratively write use-cases in natural language and verify consistency of behavior encoded within them. In particular, this is beneficial when the use-cases are created simultaneously by multiple developers. The proposed method allows verifying the consistency of textual use-case specification by employing annotations in use-case steps that are transformed into temporal logic formulae and verified within a formal behavior model. A supporting tool for plain English use-case analysis is currently being enhanced by integrating the verification algorithm proposed in the paper.

Viliam Simko, David Hauzar, Tomas Bures, Petr Hnetynka, Frantisek Plasil

Backmatter