Model-based implementation of distributed systems with priorities

Model-based application development aims at increasing the application’s integrity by using models employed in clearly defined transformation steps leading to correct-by-construction artifacts. In this paper, we introduce a novel model-based approach for constructing correct distributed implementation of component-based models constrained by priorities. We argue that model-based methods are especially of interest in the context of distributed embedded systems due to their inherent complexity (e.g., caused by non-deterministic nature of distributed systems). Our method is designed based on three phases of transformation. The input is a model specified in terms of a set of behavioral components that interact through a set of high-level synchronization primitives (e.g., rendezvous and broadcasts) and priority rules for scheduling purposes. The first phase transforms the input model into a model that has no priorities. Then, the second phase transforms the deprioritized model into another model that resolves distributed conflicts by incorporating a solution to the committee coordination problem. Finally, the third phase generates distributed code using asynchronous point-to-point message passing primitives (e.g., TCP sockets). All transformations preserve the properties of their input model by ensuring observational equivalence. All the transformations are implemented and our experiments validate their effectiveness.     

Parameterized synthesis of self-stabilizing protocols in symmetric networks

Self-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric networks, including ring, line, mesh, and torus. First, we develop cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimate states. We also develop a sufficient condition for convergence in self-stabilizing systems. Since some of our cutoffs grow with the size of the local state space of processes, scalability of the synthesis procedure is still a problem. We address this problem by introducing a novel SMT-based technique for counterexample-guided synthesis of self-stabilizing algorithms in symmetric networks. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems for ring and line topologies.     

Time-triggered runtime verification

The goal of runtime verification is to monitor the behavior of a system to check its conformance to a set of desirable logical properties. The literature of runtime verification mostly focuses on event-triggered solutions, where a monitor is invoked when an event of interest occurs (e.g., change in the value of some variable). At invocation, the monitor evaluates the set of properties of the system that are affected by the occurrence of the event. This constant invocation introduces two major defects to the system under scrutiny at run time: (1) significant overhead, and (2) unpredictability of behavior. These defects are serious obstacles when applying runtime verification on safety-critical systems that are time-sensitive by nature. To circumvent the aforementioned defects in runtime verification, in this article, we introduce a novel time-triggered approach, where the monitor takes samples from the system with a constant frequency, in order to analyze the system’s health. We describe the formal semantics of time-triggered monitoring and discuss how to optimize the sampling period using minimum auxiliary memory. We show that such optimization is NP-complete and consequently introduce a mapping to Integer Linear Programming. Experiments on a real-time benchmark suite show that our approach introduces bounded overhead and effectively reduces the involvement of the monitor at run time by using negligible auxiliary memory. We also show that in some cases it is even possible to reduce the overall overhead of runtime verification by using our time-triggered approach when the structure of the system allows choosing a long enough sampling period.     

First international Competition on Runtime Verification: rules,benchmarks, tools,and final results of CRV 2014

International Journal on Software Tools for Technology Transfer - The first international Competition on Runtime Verification (CRV) was held in September 2014, in Toronto, Canada, as a satellite...     

A framework for automated distributed implementation of component-based models

Although distributed systems are widely used nowadays, their implementation and deployment are still time-consuming, error-prone, and hardly predictable tasks. In this paper, we propose a method for producing automatically efficient and correct-by-construction distributed implementations from a model of the application software in Behavior, Interaction, Priority (BIP). BIP is a well-founded component-based framework encompassing high-level multi-party interactions for synchronizing components (e.g., rendezvous and broadcast) and dynamic priorities for scheduling between interactions. Our method transforms an arbitrary BIP model into a Send/Receive BIP model that is directly implementable on distributed execution platforms. The transformation consists in (1) breaking the atomicity of actions in components by replacing synchronous multiparty interactions with asynchronous Send/Receive interactions; (2) inserting distributed controllers that coordinate the execution of interactions according to a user-defined partition of interactions, and (3) adding a distributed algorithm for handling conflicts between controllers. The obtained Send/Receive BIP model is proven observationally equivalent to its corresponding initial model. Hence, all functional properties of the initial BIP model are preserved by construction in the implementation. Moreover, the obtained Send/Receive BIP model can be used to automatically derive distributed executable code. The proposed method is fully implemented. Currently, it is possible to generate C++ implementations for (1) TCP sockets for conventional distributed communication, (2) MPI for multi-processor platforms, and (3) POSIX threads for deployment on multi-core platforms. We present four case studies and report experimental results for different design choices including partition of interactions and choice of algorithm for distributed conflict resolution.     

Symbolic synthesis of masking fault-tolerant distributed programs

We focus on automated addition of masking fault-tolerance to existing fault-intolerant distributed programs. Intuitively, a program is masking fault-tolerant, if it satisfies its safety and liveness specifications in the absence and presence of faults. Masking fault-tolerance is highly desirable in distributed programs, as the structure of such programs are fairly complex and they are often subject to various types of faults. However, the problem of synthesizing masking fault-tolerant distributed programs from their fault-intolerant version is NP-complete in the size of the program’s state space, setting the practicality of the synthesis problem in doubt. In this paper, we show that in spite of the high worst-case complexity, synthesizing moderate-sized masking distributed programs is feasible in practice. In particular, we present and implement a BDD-based synthesis heuristic for adding masking fault-tolerance to existing fault-intolerant distributed programs automatically. Our experiments validate the efficiency and effectiveness of our algorithm in the sense that synthesis is possible in reasonable amount of time and memory. We also identify several bottlenecks in synthesis of distributed programs depending upon the structure of the program at hand. We conclude that unlike verification, in program synthesis, the most challenging barrier is not the state explosion problem by itself, but the time complexity of the decision procedures.     

Gray-box monitoring of hyperproperties with an application to privacy

Formal Methods in System Design - Runtime verification is a complementary approach to testing, model checking and other static verification techniques to verify software properties. Monitorability...