The development of trustworthy distributed algorithms requires the verification of some key properties with respect to the formal specification of the expected system executions. The atomic-state model (ASM) is the most commonly used computational model to reason on self-stabilizing algorithms. In this work, we propose methods and tools to automatically verify the self-stabilization of distributed algorithms defined in that model. To that goal, we exploit the similarities between the ASM and computational models issued from the synchronous programming area to reuse their associated verification tools, and in particular their model checkers. This allows the automatic verification of all safety properties (including bounded liveness) of any algorithm under various asynchrony assumptions (from fully asynchronous to fully synchronous) and regardless of the hypotheses on the network ( e.g. , on its topology, its edge and node labeling). • We propose a language-based framework to verify distributed algorithms written in the atomic-state model. • The approach is modular due to a clear separation between the description of algorithms, daemons, topologies, and properties. • We illustrate our proposal by verifying various self-stabilizing algorithms, solving both static and dynamic tasks. • The versatility does not come at the price of sacrificing too much efficiency in terms of verification time.

Abstract In this paper, we present sasa, an open-source SimulAtor of Self-stabilizing Algorithms. Self-stabilization defines the ability of a distributed algorithm to recover after transient failures. sasa is implemented as a faithful representation of the atomic-state model (also called the locally shared memory model with composite atomicity). This model is the most commonly used one in the self-stabilizing area to prove both the correct operation of self-stabilizing algorithms and complexity bounds on them. sasa encompasses all features necessary to debug, test and analyze self-stabilizing algorithms. All these facilities are programmable to enable users to accommodate to their particular needs. For example, asynchrony is modeled by programmable stochastic daemons playing the role of input sequence generators. Properties of algorithms can be checked using formal test oracles. The sasa distribution also provides several facilities to easily achieve (batch-mode) simulation campaigns. We show that the lightweight design of sasa allows to efficiently perform huge such campaigns. Following a modular approach, we have aimed at relying as much as possible the design of sasa on existing tools, including ocaml, dot and several tools developed in the Synchrone Group of the VERIMAG laboratory.

Debugging reactive programs requires to provide a lot of inputs -- at each reaction step. Moreover, because a reactive system reacts to an environment it tries to control, providing realistic inputs can be hard. The same considerations apply for automatic testing. This work take advantage on previous work on automated testing of reactive programs that close this feedback loop.

Architecture description languages are used to describe both the hardware and software architecture of an application, at system-level. The basic software components are intended to be developed independently, and then deployed on the described architecture. This separate development of the architecture and of the software raises the problem of early validation of the integrated system.

A sensor network may be considered as a large and complex computer system embedded in the physical environment that has some influence on the sensors. The environment is the source of (almost) all activity that occurs in the network. With a simple example modeled in our tool GLONEMO, we show the influence of an environment model that allows to describe correlated stimuli on the set of sensors at a given instant, and also correlations between successive instants

We present an operational model for describing random reactive systems. Some models have already been proposed for this purpose, but they generally aim at performing global reasoning on systems, such as stochastic analysis, or formal proofs. Our goal is somehow less ambitious, since we are rather interested in executing such models, for testing or prototyping. But on the other hand, the proposed model is not restricted by decidability issues. Therefore it can be more expressive: in particular, our model is not restricted to finite-state descriptions. The proposed model is rather general: systems are described as implicit state/transition machines, possibly infinite, where probabilities are expressed by means of relative weights. The model itself is more an abstract machine than a programming language. The idea is then to propose highlevel, user-friendly languages that can be compiled into the model. We present such a language, based on regular expressions, together with its translation into the model.

Program execution monitoring consists of checking whole executions for given properties, and collecting global run-time information. Monitoring gives valuable insights and helps programmers maintain their programs. However, application developers face the following dilemma: either they use existing monitoring tools which never exactly fit their needs, or they invest a lot of effort to implement relevant monitoring code. In this paper, we argue that when an event-oriented tracer exists, the compiler developers can enable the application developers to easily code their own monitors. We propose a high-level primitive called foldt which operates on execution traces. One of the key advantages of our approach is that it allows a clean separation of concerns; the definition of monitors is totally distinct from both the user source code and the language compiler. We give a number of applications of the use of foldt to define monitors for Mercury program executions: execution profiles, graphical abstract views, and two test coverage measurements. Each example is implemented by a few simple lines of Mercury.