Software Testing is normally one of the main forms of verification and validation used in software development but it is often manual and so expensive and error prone. One of the proposed solutions to this is to use model-based testing, in which testing is based on a model of how the system should behave. If the model has a formal semantics, then there is potential to automate systematic test generation. In this paper we consider the case where the semantics of the model is a set of refusal traces, also called failure traces. We show how the notions of fundamental refusal and fundamental refusal trace can be used to derive a normalised transition system, which we call an observation transition system (OTS), from the semantics. We then show how, if this OTS has finitely many states, and we are given a bound m, one can produce a corresponding complete test suite: one that is guaranteed to determine correctness as long as the number of states of the OTS defined by the semantics of the system under test has no more than m states. In practice, the choice of value for m might be based on domain knowledge or a cost-benefit analysis. As far as we are aware, this is the first work to show how a finite complete test suite can be derived when the semantics under consideration is a set of refusal traces.

We explore the problem of finding a minimal complete test suite for refusal trace (or failure trace) semantics. Our approach is based on generating a minimal complete set of forbidden refusal traces and utilises several interesting insights into the semantics. In particular, we identify a key class of refusals called fundamental refusals which essentially determine the refusal trace semantics, and the associated equivalence relation. We then propose a small but not necessarily minimal test suite, which can be constructed with a simple algorithm. Subsequently, we provide an enumerative method to remove all redundant traces from our complete test suite, which comes in two variants, depending on whether we wish to retain the highly desirable uniform completeness. We also address a related problem from modal logic, namely the construction of a characteristic formula of a given process with respect to refusal trace semantics, using a variant of Hennessy-Milner logic with recursion.

The existing testing theories for CSP cater for verification of interaction patterns (traces) and deadlocks, but not time. We address here refinement and testing based on a dialect of CSP, called tock -CSP, which can capture discrete time properties. This version of CSP has been of widespread interest for decades; recently, it has been given a denotational semantics, and model checking has become possible using a well established tool. Here, we first equip tock -CSP with a novel semantics for testing, which distinguishes input and output events: the standard models of ( tock -)CSP do not differentiate them, but for testing this is essential. We then present a new testing theory for timewise refinement, based on novel definitions of test and test execution. Finally, we reconcile refinement and testing by relating timed ioco testing and refinement in tock -CSP with inputs and outputs. With these results, this paper provides, for the first time, a systematic theory that allows both timed testing and timed refinement to be expressed. An important practical consequence is that this ensures that the notion of correctness used by developers guarantees that tests pass when applied to a correct system and, in addition, faults identified during testing correspond to development mistakes.

We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.

We explore the problem of finding a minimal complete test suite for a refusal trace (or failure trace) semantics. Since complete test suites are typically infinite, we consider the setting with a bound ℓ on the length of refusal traces of interest. A test suite T is thus complete if it is failed by all processes that contain a disallowed refusal trace of length at most ℓ.The proposed approach is based on generating a minimal complete set of forbidden refusal traces. Our solution utilises several interesting insights into refusal trace semantics. In particular, we identify a key class of refusals called fundamental refusals which essentially determine the refusal trace semantics, and the associated fundamental equivalence relation. We then propose a small but not necessarily minimal test suite based on our theory, which can be constructed with a simple algorithm. Subsequently, we provide an enumerative method to remove all redundant traces from our complete test suite, which comes in two variants, depending on whether we wish to retain the highly desirable uniform completeness (guarantee of shortest counterexamples).A related problem is the construction of a characteristic formula of a process P, that is, a formula ΦP such that every process which satisfies ΦP refines P. Our test generation algorithm can be used to construct such a formula using a variant of Hennessy-Milner logic with recursion.

Abstract We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time– and value–domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.

Logical characterisation of a behavioural equivalence relation precisely specifies the set of formulae that are preserved and reflected by the relation. Such characterisations have been studied extensively for exact semantics on discrete models such as bisimulations for labelled transition systems and Kripke structures, but to a much lesser extent for approximate relations, in particular in the context of hybrid systems. We present what is to our knowledge the first characterisation result for approximate notions of hybrid refinement and hybrid conformance involving tolerance thresholds in both time and value. Since the notion of conformance in this setting is approximate, any characterisation will unavoidably involve a notion of relaxation, denoting how the specification formulae should be relaxed in order to hold for the implementation. We also show that an existing relaxation scheme on Metric Temporal Logic used for preservation results in this setting is not tight enough for providing a characterisation of neither hybrid conformance nor refinement. The characterisation result, while interesting in its own right, paves the way to more applied research, as our notion of hybrid conformance underlies a formal model-based technique for the verification of cyber-physical systems.

Abstract A basic sanity property of a process semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by developing, for a specific process semantics, a syntactic format for operational semantics specifications. We suggest a novel, orthogonal approach, which focuses on a specific process operator and determines a class of congruence relations for this operator. To this end, we impose syntactic restrictions on Hennessy–Milner logic, so that a process semantics whose modal characterization satisfies those criteria is guaranteed to be a congruence with respect to the operator in question. We investigate alternative composition, action prefix, projection, encapsulation, renaming, and parallel composition with communication, in the context of both concrete and weak process semantics.

We present a theory of abstraction for the framework of parameterised Boolean equation systems, a first-order fixpoint logic. Parameterised Boolean equation systems can be used to solve a variety of problems in verification. We study the capabilities of the abstraction theory by comparing it to an abstraction theory for Generalised Kripke modal Transition Systems (GTSs). We show that for model checking the modal μ-calculus, our abstractions can be exponentially more succinct than GTSs and our theory is as complete as the GTS framework for abstraction. Furthermore, we investigate the completeness of our theory irrespective of the encoded decision problem. We illustrate the potential of our theory through case studies using the first-order modal μ-calculus and a real-time extension thereof, conducted using a prototype implementation of a new syntactic transformation for parameterised Boolean equation systems.

An existing axiomatization strategy for process algebras modulo bisimulation semantics can be extended so that it can be applied to other behavioural semantics as well. We study term rewriting properties of the resulting axiomatizations.

We prove a compactness theorem in the context of Hennessy–Milner logic and use it to derive a sufficient condition on modal characterisations for the approximation induction principle to be sound modulo the corresponding process equivalence. We show that this condition is necessary when the equivalence in question is compositional with respect to the projection operators. Furthermore, we derive different upper bounds for the constructive version of the approximation induction principle with respect to simulation and decorated trace semantics.