Abstract This paper deals with runtime enforcement of timed properties with uncontrollable events. Runtime enforcement consists in defining and using an enforcement mechanism that modifies the executions of a running system to ensure their correctness with respect to the desired property. Uncontrollable events cannot be modified by the enforcement mechanisms and thus have to be released immediately. We present a complete theoretical framework for synthesising such mechanism, modelling the runtime enforcement problem as a Büchi game. It permits to pre-compute the decisions of the enforcement mechanism, thus avoiding to explore the whole execution tree at runtime. The obtained enforcement mechanism is sound, compliant and optimal, meaning that it should output as soon as possible correct executions that are as close as possible to the input execution. This framework takes as input any timed regular property modelled by a timed automaton. We present GREP, a tool implementing this approach. We provide algorithms and implementation details of the different modules of GREP, and evaluate its performance. The results are compared with another state of the art runtime enforcement tool.

This paper deals with runtime enforcement of untimed and timed properties with uncontrollable events. Runtime enforcement consists in defining and using mechanisms that modify the executions of a running system to ensure their correctness with respect to a desired property. We introduce a framework that takes as input any regular (timed) property described by a deterministic automaton over an alphabet of events, with some of these events being uncontrollable. An uncontrollable event cannot be delayed nor intercepted by an enforcement mechanism. Enforcement mechanisms should satisfy important properties, namely soundness, compliance and optimality – meaning that enforcement mechanisms should output as soon as possible correct executions that are as close as possible to the input execution. We define the conditions for a property to be enforceable with uncontrollable events. Moreover, we synthesise sound, compliant and optimal descriptions of runtime enforcement mechanisms at two levels of abstraction to facilitate their design and implementation.

We leverage Büchi games for the runtime enforcement of regular properties with uncontrollable events. Runtime enforcement consists in modifying the execution of a running system to have it satisfy a given regular property, modelled by an automaton. We revisit runtime enforcement with uncontrollable events and propose a framework where we model the runtime enforcement problem as a Büchi game and synthesise sound, compliant, and optimal enforcement mechanisms as strategies.We present algorithms and a tool implementing enforcement mechanisms.We reduce the complexity of the computations performed by enforcement mechanisms at runtime by pre-computing the decisions of enforcement mechanisms ahead of time.

This paper deals with communicating system robustness testing by proposing a method for checking the correct behaviour of the Implementation Under Test (IUT) in unexpected situations. This formal method takes specifications written with IOLTS and generates robustness test cases by using the ioco theory. IOLTS are used to model many systems like distributed ones or Web service compositions. We present an algorithm permitting to generate sound test cases especially focusing on robustness aspects.

Robustness is an important feature required for embedded systems. This paper presents a methodology to test robustness of such systems. We investigate system behaviour aspects. We handle two formal specifications : a nominal one which describes the system behaviour in normal conditions and a degraded one which describes the behaviour in critical conditions. Both are described as Labelled Transition Systems for the untimed systems and as Timed Automata for timed systems. We extract test sequences from the nominal or from the degraded specification. We perform fault injection on these test sequences. Finally, we submit these sequences to the Implementation Under Test (IUT) and then we analyze its behaviour using adequate robustness relations.

Summary form only given. In this paper, we suggest a realistic methodology for testing robustness of real-time component-based systems (RTCBS). A RTCBS system is described as a collection of components where each component is specified by a nominal and a degraded specification, modeled as a timed input-output automaton (TIOA). Further, the communication of the whole system is also specified by its nominal and degraded specification. We extract test sequences from the nominal specification and we inject automatically faults in order to model hostile environments. Then, we present an adequate test architecture consisting of the system under test (SUT) of components, and a distributed tester that consists of a set of coordinating testers. Each tester is dedicated to test a single SUT component. A test execution algorithm with an approach to handle testers coordination and execution delay is presented. Testing the SUT is divided into two phases. In the first phase, the tester tests the robustness of each component in isolation. If all components are robust according to the inserted hazards, in the second phase, we use the nominal and degraded specification of the whole system to check the robustness of communications between components.