Cloud computing offers opportunities to increase productivity and reduce costs. Quickly adapting to changing needs is key to maintaining cloud applications. In traditional development, coordination is implemented in computational code. Although change impact analyses are studied, adjusting the implementation is time-consuming and error-prone when the coordination strategy changes. Exogenous coordination separates the implemented coordination and computational code to cope with this problem. This separation improves the reusability of components. Additionally, other applications with similar interaction patterns can reuse the coordination specification. The main contribution of this paper is to propose a methodology to develop and maintain cloud applications following the exogenous approach. To illustrate the idea, we introduce a new framework named OCCIwareBIP, which integrates JavaBIP — a framework for the exogenous coordination of concurrent Java components into OCCIware — a framework for designing cloud applications. We also leverage the coordination model to verify the deadlock-freedom of the cloud application. Finally, we present an application to show the ability of our approach to guarantee the safety and benefits of modularization in developing concurrent cloud applications.

Abstract We present “Verified JavaBIP”, a tool set for the verification of JavaBIP models. A JavaBIP model is a Java program where classes are considered as components, their behaviour described by finite state machine and synchronization annotations. While JavaBIP guarantees execution progresses according to the indicated state machines, it does not guarantee properties of the data exchanged between components. It also does not provide verification support to check whether the behaviour of the resulting concurrent program is as (safe as) expected. This paper addresses this by extending the JavaBIP engine with run-time verification support, and by extending the program verifier VerCors to verify JavaBIP models deductively. These two techniques complement each other: feedback from run-time verification allows quicker prototyping of contracts, and deductive verification can reduce the overhead of run-time verification. We demonstrate our approach on the “Solidity Casino” case study, known from the VerifyThis Collaborative Long Term Challenge.

Abstract Full a posteriori verification of the correctness of modern software systems is practically infeasible due to the sheer complexity resulting from their intrinsic concurrent nature. An alternative approach consists of ensuring correctness by construction. We discuss the Rigorous System Design (RSD) approach, which relies on a sequence of semantics-preserving transformations to obtain an implementation of the system from a high-level model while preserving all the properties established along the way. In particular, we highlight some of the key requirements for the feasibility of such an approach, namely availability of (1) methods and tools for the design of correct-by-construction high-level models and (2) definition and proof of the validity of suitable domain-specific abstractions. We summarise the results of the extended versions of seven papers selected among those presented at the $$1\mathrm {st}$$ 1 st and the $$2\mathrm {nd}$$ 2 nd International Workshops on Methods and Tools for Rigorous System Design (MeTRiD 2018–2019), indicating how they contribute to the advancement of the RSD approach.

Real-time control systems use controllers that compute and issue setpoints within stringent delay constraints. Failure to do so, due to a crash or delay as a result of software and/or hardware faults, can cause failure of the controlled resources. Recently, Axo, a protocol for masking crash and delay faults by replicating the controller, was proposed. Axo provides safety by discarding delayed setpoints, and it relies on the presence of valid setpoints for providing availability. To ensure that enough valid setpoints are issued, faulty controller replicas need to be detected and recovered. We present a mechanism for detection and recovery of delay- and crash-faulty replicas under the Axo framework. These mechanisms were designed to be soft state (i.e., their state can be reconstructed from received messages) to enable seamless additions of new replicas. Besides presenting the design, we analytically characterize the time to detect and recover a faulty replica, and we validate them experimentally. We demonstrate the performance of Axo by using two case studies: the first provides a stability analysis of an inverted pendulum system with Axo, and the second shows the fault-tolerance performance of Axo through a deployment on a real-time control system that controls a CIGRÉ low-voltage benchmark microgrid.

Real-time control systems (RTCSs) tolerate delay and crash faults by replicating the controller. Each replica computes and issues setpoints to actuators over a network that might drop or delay messages. Hence, the actuators might receive an inconsistent set of setpoints. Such inconsistency is avoided either by having a single primary replica compute and issue setpoints (in passive replication) or a consensus algorithm select one sending-replica (in active replication). However, due to the impossibility of a perfect failure-detector, passive-replication schemes can have multiple primaries, causing inconsistency, especially in the presence of intermittent delay faults. Furthermore, the impossibility of bounded-latency consensus causes both schemes to have poor real-time performance. We identified three properties of RTCSs that enable active-replication schemes to agree on the measurements before computing, instead of using traditional consensus. As all computing replicas compute with the same state, the resulting setpoints are guaranteed to be consistent. We present the design of Quarts, an agreement solution for active replication that guarantees consistency and bounded latency-overhead. We prove the guarantees and compare the performance of Quarts with existing solutions through simulation. We show that Quarts provides an availability higher than existing solutions, and that the availability improvement is up to 10x with two replicas.

Summary A strong separation of concerns is necessary in order to make the design of domain‐specific functional components independent from cross‐cutting concerns, such as concurrent access to the shared resources of the execution platform. Native coordination mechanisms, such as locks and monitors, allow developers to address these issues. However, such solutions are not modular; they are complex to design, debug, and maintain. We present the JavaBIP framework that allows developers to think on a higher level of abstraction and clearly separate the functional and coordination aspects of the system behavior. It implements the principles of the Behavior, Interaction, and Priority (BIP) component framework rooted in rigorous operational semantics. It allows the coordination of existing concurrent software components in an exogenous manner, relying exclusively on annotations, component APIs, and external specification files. We introduce the annotation and specification syntax of JavaBIP and illustrate its use on realistic examples, present the architecture of our implementation, which is modular and easily extensible, and provide and discuss performance evaluation results. Copyright © 2017 John Wiley & Sons, Ltd.

BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to systems parameterized in the number of components. We show that FOIL captures classical parameterized architectures such as token-passing rings, cliques of identical components communicating with rendezvous or broadcast, and client-server systems. Although the BIP framework includes efficient verification tools for statically-defined systems, none are available for parameterized systems with an unbounded number of components. The parameterized model checking literature contains a wealth of techniques for systems of classical architectures. However, application of these results requires a deep understanding of parameterized model checking techniques and their underlying mathematical models. To overcome these difficulties, we introduce a framework that automatically identifies parameterized model checking techniques applicable to a BIP design. To our knowledge, it is the first framework that allows one to apply prominent parameterized model checking results in a systematic way.

We consider real-time control systems that consist of a controller that computes and sends setpoints to be implemented in physical processes through process agents. We focus on systems that use commercial off-the-shelf hardware and software components. Setpoints of these systems have strict real-time constraints: Implementing a setpoint after its deadline, or not receiving setpoints within a deadline, can cause failure. In this paper, we address delay faults: faults that cause setpoints to violate their real-time constraints. We present Axo, a fault-tolerance protocol that guarantees safety and improves availability for a class of such systems that exhibit two main properties: the setpoints must have a known validity horizon, and process agents must be capable of handling duplicate setpoints. To reason about delay faults, and consequently design Axo, we present an abstraction of a controller; the abstraction applies to a wide range of real-time control systems. We prove guarantees of safety and availability. Finally, we present an implementation of Axo and the results of the tests performed with Commelec, a real-time control system for electric grids.

Developing embedded real-time systems based on the TT paradigm is a challenging task due to the increasing complexity of such systems and the necessity to manage, already in the programming model, the fine-grained temporal constraints and the low-level communication primitives imposed by the temporal firewall abstraction. In embedded systems, high-level component-based design approaches have been proposed in order to allow specification and design of complex real-time systems. However, their final implementations mostly rely on the generation of code for generic execution platforms. On the other hand, a variety of Real-Time Operating System (RTOS), in particular when based on the Time-Triggered (TT) paradigm, guarantee the temporal and behavioural determinism of the executed software. However, these TT-based RTOS do not provide high-level design frameworks enabling the scalable design of complex safety-critical real-time systems. The goal of our work is to couple a high-level component-based design approach based on the RT-BIP (Real-Time Behaviour-Interaction-Priority) framework with a safety-oriented real-time execution platform, implementing the TT approach. Thus, we combine their complementary advantages, by deriving correct-by-construction TT implementations from high-level componentised models. To this end, we propose an automatic transformation process from RT-BIP models into applications for the target platform based on the TT execution model. The process consists in a two-step transformation. The first step transforms a generic RT-BIP model into a restricted one, which lends itself well to an implementation based on TT communication primitives. This step was presented in previous work. The second step, which is the subject of this paper, transforms the resulting model into the TT implementation provided by the PharOS RTOS. We identify the key difficulties in defining this transformation, propose solutions to address these difficulties and study how this transformation can be proven to be semantics-preserving. This transformation is already partially implemented.

Abstract Architectures depict design principles: paradigms that can be understood by all, allow thinking on a higher plane and avoiding low-level mistakes. They provide means for ensuring correctness by construction by enforcing global properties characterizing the coordination between components. An architecture can be considered as an operator A that, applied to a set of components B , builds a composite component A ( B ) meeting a characteristic property Φ . Architecture composability is a basic and common problem faced by system designers. In this paper, we propose a formal and general framework for architecture composability based on an associative, commutative and idempotent architecture composition operator ⊕ . The main result is that if two architectures A 1 and A 2 enforce respectively safety properties Φ 1 and Φ 2 , the architecture A 1 ⊕ A 2 enforces the property Φ 1 ∧ Φ 2 , that is both properties are preserved by architecture composition. We also establish preservation of liveness properties by architecture composition. The presented results are illustrated by a running example and a case study.

This paper presents SeBip, the first symbolic executor for component-based systems modeled in BIP. To tackle the path explosion problem, SeBip combines partial order reduction technique to reduce the number of interactions to be explored during executing the system symbolically. An experimental evaluation has been carried out to demonstrate the scalability of SeBip on detecting bugs.

Programmable logic controllers (PLCs) are embedded computers widely used in industrial control systems. Ensuring that a PLC software complies with its specification is a challenging task. Formal verification has become a recommended practice to ensure the correctness of safety-critical software, but is still underused in industry due to the complexity of building and managing formal models of real applications. In this paper, we propose a general methodology to perform automated model checking of complex properties expressed in temporal logics [e.g., computation tree logic (CTL) and linear temporal logic (LTL)] on PLC programs. This methodology is based on an intermediate model (IM) meant to transform PLC programs written in various standard languages [structured text (ST), sequential function chart (SFC), etc.] to different modeling languages of verification tools. We present the syntax and semantics of the IM, and the transformation rules of the ST and SFC languages to the nuXmv model checker passing through the IM. Finally, two real cases studies of the European Organization for Nuclear Research (CERN) PLC programs, written mainly in the ST language, are presented to illustrate and validate the proposed approach.

Coordinating component behaviour and access to resources is among the key difficulties of building large concurrent systems. To address this, developers must be able to manipulate high-level concepts, such as Finite State Machines and separate functional and coordination aspects of the system behaviour. OSGi associates to each bundle a state machine representing the bundle's lifecycle. However, once the bundle has been started, it remains in the state Active - the functional states are not represented. Therefore, this mechanism is not sufficient for coordination of active components.

Testing of critical PLC (Programmable Logic Controller) programs remains a challenging task for control system engineers as it can rarely be automated. This paper proposes a model based approach which uses the BIP (Behavior, Interactions and Priorities) framework to perform automated testing of PLC programs developed with the UNICOS (UNified Industrial COntrol System) framework. This paper defines the translation procedure and rules from UNICOS to BIP which can be fully automated in order to hide the complexity of the underlying model from the control engineers. The approach is illustrated and validated through the study of a water treatment process.

We develop a unified functional formalism for modelling complex systems, that is to say systems that are composed of a number of heterogeneous components, including typically software and physical devices. Our approach relies on non-standard analysis that allows us to model continuous time in a discrete way. S ystems are defined as generalized Turing machines with temporized input, internal and output mechanisms. Behaviors of systems are represented by transfer functions. A transfer function is said to be implementable if it is associated with a system. This notion leads us to define a new class – which is natural in our framework – of computable functions on (usual) real numbers. We show that our definitions are robust: on one hand, the class of implementable transfer functions is closed under composition; on the other hand, the class of computable functions in our meaning includes analytical functions whose coefficients are computable in the usual way, and is closed under addition, multiplication, differentiation and integration. Our class of computable functions also includes solutions of dynamical and Hamiltonian systems defined by computable functions. Hence, our notion of system appears to take suitably into account physical systems.

We provide an algebraic formalization of connectors in the BIP component framework. A connector relates a set of typed ports. Types are used to describe different modes of synchronization: rendezvous and broadcast, in particular. Connectors on a set of ports P are modeled as terms of the algebra AC(P), generated from P by using a binary fusion operator and a unary typing operator. Typing associates with terms (ports or connectors) synchronization types --- trigger or synchron --- that determine modes of synchronization. Broadcast interactions are initiated by triggers. Rendezvous is a maximal interaction of a connector including only synchrons. The semantics of AC(P) associates with a connector the set of its interactions. It induces on connectors an equivalence relation which is not a congruence as it is not stable for fusion. We provide a number of properties of AC(P) used to symbolically simplify and handle connectors. We provide examples illustrating applications of AC(P), including a general component model encompassing synchrony, methods for incremental model decomposition, and efficient implementation by using symbolic techniques.

We provide an algebraic formalisation of connectors in BIP. These are used to structure interactions in a component-based system. A connector relates a set of typed ports. Types are used to describe different modes of synchronisation: rendezvous and broadcast, in particular.

We consider several hybrid ARQ (H-ARQ) control schemes for high speed downlink packet access (HSDPA) with 16 symbols quadrature amplitude modulation (16QAM). These schemes consist of a sequence of values for the X/sub rv/ parameter to be used at sequential retransmissions when a block is not decoded correctly. A choice of an H-ARQ control scheme influences two parameters: quality of service (QoS) and user equipment (UE) buffer requirements. Based on several link level simulations, we propose an optimal control scheme using maximum space, as well as two slightly suboptimal ones that allow to reduce the UE buffer size.