Abstract Formal methods have been successfully used to develop advanced test generation techniques. While various test generation tools and test coverage criteria have been proposed, their adoption in industrial practice remains fragmented. This paper presents , a novel open-source toolset for testing C programs, which aims to facilitate the industrial application of diverse testing technologies by integrating them within a single framework. offers a comprehensive set of testing services, ranging from the specification of test objectives for selected test coverage criteria, through test case generation and the detection of uncoverable objectives, to the measurement of the resulting coverage. It integrates a rich set of analyzers: the fuzzer , the model-checker , the dynamic symbolic execution tool , and the static analyzer for detecting uncoverable test objectives. These analyzers enrich each other’s results through a shared store of test objectives and a shared corpus of test cases. Particular attention is paid to the careful handling of runtime errors and initialization functions, which are essential for industrial applications. Initial experiments confirm the benefits of the proposed toolset.

We present an extension of the actor model with real-time, including deadlines associated with messages, and explicit application-level scheduling policies, e.g.,"earliest deadline first" which can be associated with individual actors. Schedulability analysis in this setting amounts to checking whether, given a scheduling policy for each actor, every task is processed within its designated deadline. To check schedulability, we introduce a compositional automata-theoretic approach, based on maximal use of model checking combined with testing. Behavioral interfaces define what an actor expects from the environment, and the deadlines for messages given these assumptions. We use model checking to verify that actors match their behavioral interfaces. We extend timed automata refinement with the notion of deadlines and use it to define compatibility of actor environments with the behavioral interfaces. Model checking of compatibility is computationally hard, so we propose a special testing process. We show that the analyses are decidable and automate the process using the Uppaal model checker.

Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on the diagnosability property of a system. Diagnosability describes the system ability to determine whether a given fault has effectively occurred based on the observations. However, this is a very strong property that requires generally high number of sensors to be satisfied. Consequently, it is not rare that developing a diagnosable system is too expensive. To solve this problem, in this paper, we first define a new system property called manifestability that represents the weakest requirement on faults and observations for having a chance to identify on line fault occurrences and can be verified at design stage. Then, we propose an algorithm with PSPACE complexity to automatically verify it.

Summary In the context of testing from algebraic specifications, test cases are ground formulas chosen amongst the ground semantic consequences of the specification, according to some possible additional observability conditions. A test set is said to be exhaustive if every programmePpassing all the tests is correct and if for every incorrect programmeP, there exists a test case on whichPfails. Because correctness can be proved by testing on such a test set, it is an appropriate basis for the selection of a test set of practical size. The largest candidate test set is the set of observable consequences of the specification. However, depending on the nature of specifications and programmes, this set is not necessarily exhaustive. In this paper, we study conditions to ensure the exhaustiveness property of this set for several algebraic formalisms (equational, conditional positive, quantifier free and with quantifiers) and several test hypotheses. Copyright © 2016 John Wiley & Sons, Ltd.

SUMMARY We propose a theoretical testing framework and a test generation algorithm for concurrent systems specified with true‐concurrency models, such as Petri nets or networks of automata. The semantic model of computation of such formalisms is labelled event structures, which allow to represent concurrency explicitly. We introduce the notions of strong and weak concurrency: strongly concurrent events must be concurrent in the implementation, while weakly concurrent ones may eventually be ordered. The ioco type conformance relations for sequential systems rely on the observation of sequences of actions and blockings; thus, they are not capable of capturing and exploiting concurrency of non‐sequential behaviours. We propose an extension of ioco for labelled event structures, named co‐ioco, allowing to deal with strong and weak concurrency. We extend the notions of test cases and test execution to labelled event structures and give a test generation algorithm building a complete test suite for co‐ioco. Copyright © 2014 John Wiley & Sons, Ltd.

We apply automata theory to specifying behavioralinterfaces of objects and show how to check schedulabilityand compatibility of real time asynchronous objects.The behavioral interfaces of real time objects specify(the order and timings of) the messages an object maysend and receive. Each object is checked against itsbehavioral interface; first, to guarantee its correct outputbehavior, and second to make sure that every messageit may receive is processed within the designateddeadline (schedulability analysis). Next, we propose anew technique for testing whether every object is usedas expected (i.e., according to its behavioral interface)when combined with other objects (compatibility check).Compatibility additionally implies schedulability in thecontext of the actual system. The analyses are automatedusing the Uppaal model checker.

In the framework of functional testing from algebraic specifications, the strategy of test selection which has been widely and efficiently applied is based on axiom unfolding. In this paper, we propose to extend this selection strategy to a modal formalism used to specify dynamic and reactive systems. Such a work is then a first step to tackle testing of such systems more abstractly than most of the works dealing with what is called conformance testing. We get a higher level of abstraction since our specifications account for what is usually called underspecification, i.e. they do not denote a unique model but a class of models. Hence, the testing process can be applied at every design level.

In this paper, we present a temporal logic called /spl Fscr/ whose interpretation is over input output symbolic transition systems (IOSTS). IOSTS extend transition systems to communications and data in order to tackle communications with system environment. /spl Fscr/ is then defined as an extension of temporal logic CTL* (a temporal logic which mixes together the features of linear temporal logic (LTL) and computational temporal logic (CTL)). Three basic properties are established on /spl Fscr/: adequacy and preservation of properties along synchronized product and IOSTS refinement.