Runtime Enforcement (RE) is a monitoring technique aimed at correcting possibly incorrect executions w.r.t. a set of formal requirements (properties) of a system. In this paper, we consider enforcement monitoring of real-time properties. Thus, executions are modelled as timed words and specifications as timed automata. Moreover, we consider that the enforcer has the ability to delay events by storing or buffering them into its internal memory (and releasing them when the property is finally satisfied) and suppressing events when no delaying is appropriate. Practically, in an implementation, the internal memory of the enforcer is finite. In this paper, we propose a new RE paradigm for timed properties, where the memory of the enforcer is bounded/finite, to address practical applications with memory constraints and timed specifications. Bounding the memory presents a number of difficulties, e.g., how to accommodate a timed event into the memory when the memory is full, s.t., regardless of the course of action we choose to handle this situation, the behaviour of the bounded enforcer should not significantly differ from that of the unbounded enforcer. The problem of how to optimally discard events when the buffer is full is significantly more difficult in a timed environment where the progress of time affects the satisfaction or violation of a property. We define the bounded-memory RE problem for timed properties and develop a framework for regular timed properties specified as timed automata. The proposed framework is implemented in Python, and its performance is evaluated. From experiments, we discovered that the enforcer has a reasonable execution time overhead.

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.

SUMMARY This paper explores the generation of conformance test cases for recursive tile systems (RTSs) in the framework of the classical ioco testing theory. The RTS model allows the description of reactive systems with recursion and is very similar to other models like pushdown automata, hyperedge replacement grammars or recursive state machines. Test generation for this kind of infinite state labelled transition systems is seldom explored in the literature. The first part presents an off‐line test generation algorithm for weighted RTSs, a determinizable sub‐class of RTSs, and the second one an on‐line test generation algorithm for the full RTS model. Both algorithms use test purposes to guide test selection through targeted behaviours. Additionally, essential properties relating verdicts produced by generated test cases with both the soundness, with respect to the specification, and the precision, with respect to a test purpose, are proved. Copyright © 2014 John Wiley & Sons, Ltd.

In this paper, we describe a methodology integrating verification and conformance testing. A specification of a system - an extended input-output automaton, which may be infinite-state - and a set of safety properties ("nothing bad ever happens") and possibility properties ("something good may happen") are assumed. The properties are first tentatively verified on the specification using automatic techniques based on approximated state-space exploration, which are sound, but, as a price to pay for automation, are not complete for the given class of properties. Because of this incompleteness and of state-space explosion, the verification may not succeed in proving or disproving the properties. However, even if verification did not succeed, the testing phase can proceed and provide useful information about the implementation. Test cases are automatically and symbolically generated from the specification and the properties and are executed on a black-box implementation of the system. The test execution may detect violations of conformance between implementation and specification; in addition, it may detect violation/satisfaction of the properties by the implementation and by the specification. In this sense, testing completes verification. The approach is illustrated on simple examples and on a bounded retransmission protocol.

The object-oriented software development process is increasingly used for the construction of complex distributed systems. In this context, behavior models have long been recognized as the basis for systematic approaches to requirements capture, specification, design, simulation, code generation, testing, and verification. Two complementary approaches for modeling behavior have proven useful in practice: interaction-based modeling (e.g., UML sequence diagrams) and state-based modeling (e.g., UML statecharts). Building on formal V&V techniques, in this article we present a method and a tool for automated synthesis of test cases from scenarios and a state-based design model of the application, remaining entirely within the UML framework. The underlying "on the fly" test synthesis algorithms are based on the input/output labeled transition system formalism, which is particularly appropriate for modeling applications involving asynchronous communication. The method is eminently compatible with classical OO development processes since it can be used to synthesize test cases from the scenarios used in early development stages to model global interactions between actors and components, instead of these test cases being derived manually. We illustrate the system test synthesis process using an air traffic control software example

We report on a tool we have developed that automates the derivation of tests from specifications. The tool implements conformance testing techniques to derive symbolic tests that incorporate their own oracles from formal operational specifications. It was applied for testing a simple version of the CEPS (Common Electronic Purse Specification).

This paper presents a model, a strategy and a methodology for planning integration and regression testing from an object-oriented model. It shows how to produce a model of structural system test dependencies which evolves with the refinement process of the object-oriented design. The model (test dependency graph) serves as a basis for ordering classes and methods to be tested for regression and integration purposes (minimization of test stubs). The mapping from unified modeling language to the defined model is detailed as well as the test methodology. While the complexity of optimal stub minimization is exponential with the size of the model, an algorithm is given that: computes a strategy for integration testing with a quadratic complexity in the worst case; and provides an efficient testing order for minimizing the number of stubs. Various integration strategies are compared with the optimized algorithm (a real-world case study illustrates this comparison). The results of the experiment seem to give nearly optimal stubs with a low cost despite the exponential complexity of getting optimal stubs. As being a part of a design-for-testability approach, the presented methodology also leads to the early repartition of testing resources during system integration for reducing integration duration.

We present a model, a strategy and a methodology for planning integration and regression testing from an object oriented (OO) model. We show how to produce a model of structural system test dependencies which evolves with the refinement process of the OO design. The model, that is the test dependency graph, serves as a basis for ordering classes and methods to be tested for regression and integration purposes (minimization of test stubs). The mapping from UML to the defined model is detailed as well as the test methodology. While the complexity of optimal stub minimization is exponential with the size of the model, an algorithm which computes a strategy for integration testing with a quadratic complexity is detailed. This algorithm provides an efficient testing order for minimizing the number of stubs. A comparison is given of various integration strategies with the proposed optimized algorithm (a real-world case study illustrates this comparison). The results of the experiment seem to give nearly optimal stubs with a low cost despite the exponential complexity of getting optimal stubs.

The problem of checking the correctness of distributed computations arises when debugging distributed algorithms, and more generally when testing protocols or distributed applications. For that purpose, one describes the expected behavior (or suspected errors) by a global property: for example, a predicate on process variables, or the set of admissible orderings on observable events. The problem is to check whether this property is satisfied or not during the execution. A relevant model for this study is the partial order of message causality and the associated state graph, called "lattice of consistent cuts". In this paper, we propose a general approach to trace checking, based on partial order theory.>