ITTCPS

ITTCPS
Implementable Testing Theory for Cyber Physical Systems
(2015-05-01 - 2017-04-30)

Summary

The objective of this project is to elaborate a novel view on concurrent systems semantics and apply this to the fields of model-based testing and model checking for cyber-physical systems (CPS).

The "classical" semantic approaches available today do no longer cover all phenomena observable in modern hardware architectures and in highly distributed CPS networks with many participants. The latter demand adequate behavioural models reflecting dynamicity of system configurations, evolution of behavioural assertions, large numbers of replicated components, and mixed discrete and time-continuous behaviour. The main challenge, however, consists in inventing a practicable method for translating theories elaborated in one semantic framework into a corresponding theory of another.

The unique selling points of this project do not only consist in the basic research contributions to the field of semantic frameworks, but in a very practical implication: advanced model-based testing tools and model checkers operate on suitable encodings of a given system model's behavioural semantics. To apply a test strategy or to prove the validity of a model property, these tools use theories established in a specific semantic framework. The current state of the art only allows to apply these theories to concrete system models interpreted in the same framework. Mappings to other frameworks are extremely complicated and cumbersome to verify. With the novel method of semantic navigation to be elaborated in this project, easy - even automated - mappings of existing theories established in one semantic framework into others will become possible. This enables an effective application of methods and tools to modelling formalisms originally interpreted in other semantic frameworks.

Overview

• Project description
• Publications

Project description

The challenge: a novel view on concurrent CPS semantics

1. distribution,
2. intelligence in peripheral components (e.g., intelligent sensors),
3. dynamicity (dynamic changes of the CPS infrastructure during operation),
4. autonomy (capability of CPS components or sub-networks to perform "local" decisions),
5. multiple communication mechanisms (due to the technical heterogeneity of the communicating components),
6. observation and control of mixed time-discrete ("switches") and time-continuous ("analogue devices") physical processes,
7. emergence of behaviour (the cooperating components of the CPS achieve something that cannot be achieved by a part of the network alone), and
8. evolution (parts of the CPS may change their asserted behaviour over time; for example, due to a change of operational boundary conditions, or due to technical evolution in components being replaced).

As a consequence, the existing semantic frameworks we have investigated so far for elaborating our theories used in testing and model checking will be left behind, and a new context of reasoning will be established, as described below. This, however, is not the only difference that comes with the envisaged change of paradigm. Additionally, the mapping of established theories from one semantic framework into another one will become one of the major activities in the future: due to the size and heterogeneity of CPS, it is a natural phenomenon that different components will be developed using different formalisms with different semantics optimised for the component's behavioural characteristics. As a consequence, the notion of a single development or test model interpreted in a single semantic framework will no longer exist.

This challenge has already been perceived in the field of model-based software development (see, for example, Favre and NGuyem: Towards a Megamodel to Model Software Evolution Through Transformations), but the results obtained there are of a more syntactic and semiformal nature, while we aim at a network of semantics that are applicable when modelling a CPS with different formalisms. The term "network" is used here in the sense that links between different semantics can be exploited to "transport" theories established in one semantics to another one. Practically speaking, this means, that a test strategy based on a theory established in one semantic framework can be translated into a strategy in the other semantics used for modelling different parts of the CPS. The translation process also maps test case representations into others that are suitable in the modelling formalisms interpreted in the other semantics. As a result, a distributed CPS test can be designed with guaranteed completeness properties, without having to re-establish the underlying theory in every framework.

Summarising, while basic research of the past has been performed in a single semantic framework, future research in the context of this project will be performed in a network of semantics, together with a navigation mechanism allowing to transport theories from their original semantic framework to another one. The benefits of this approach consist in the fact that the application of novel test strategies or model checking techniques can be far more easily applied to other formalisms than it was possible in the past, and that collaborative CPS development and verification with different formalisms and associated semantic frameworks will be enabled.

A bounded dynamicity semantics for CPS

• Just as an assembler programming language may be hard to read, but allows to encode all behaviours that are executable by the underlying hardware, we need a "low-level" semantics that allows to encode all behaviours that might be required for modelling CPS.
• The low-level semantics has to be complemented with a mechanism for abstraction, so that less fine-grained and therefore more elegant and understandable model abstractions can be created.
• The semantic representations should be optimised for the purpose of model-based testing and bounded model checking.

These objectives lead to a new low-level semantics which is based on an extension of Kripke Structures (KS). This structure enables the utilisation of variables and complex data types. It is already equipped with the very first basis of an abstraction mechanism, since the labelling function of KS associates states s with sets of atomic propositions that are valid in s. We will extend the common notion of KS to incorporate time-continuous behaviours, and a more powerful abstraction mechanism based on Galois Connections will be used to define simulation and refinement relations between different KS. This mechanism also provides automated translation rules for model properties that remain valid when changing the abstraction level.

For reflecting dynamic changes of CPS configurations in the semantics, we exploit the observations that CPS also fulfil the standard hypothesis of finite variability, and that model-based test generation and bounded model checking explore models only in a bounded vicinity of a given state. As a consequence, only a bounded number of configuration changes may occur within the "exploration distance" - this motivates the name bounded dynamicity semantics (BDS). This semantics allows for far simpler encodings of configuration changes than are required, for example, when modelling object-oriented software systems, where conceptually infinite numbers of object creations or deletions can occur.

Parallel composition in these extended KS can be instantiated with different flavours: both synchronous "true parallelism" and interleaving semantics can be used.

The emergent behaviour of CPS can be specified by means of temporal logic properties that are directly associated with each extended KS through its labelling functions and the abstractions built on top of that. Moreover, the behaviour of local CPS components can be characterised again by assertions specified in temporal logic, and the evolution of component behaviour can be detected by means of monitors observing contract breaches by means of passive testing techniques (see Comprehensive modelling for advanced systems of systems - contract support for evolving SoS).

To our best knowledge, there is currently no other fully formal - and therefore suitable for mechanised evaluation - semantics that can capture complex data structures, time-discrete and continuous behaviour, dynamicity, emergence, and evolution and comes with a powerful abstraction mechanism. A key enabler, however, for the success of the bounded dynamicity semantics, will be provided by the semantic navigator described below.

The semantic navigator

The second main objective of this project is therefore to provide a semi-automated navigation mechanism that allows to switch between modelling formalisms and their semantic representations, thereby translating model properties and whole theories established in one model and its semantic framework to another framework and its associated models contributing to the overall CPS model. Two alternatives to achieve this in a well-organised and mathematically sound manner are

• Goguen's and Burstall's theory of institutions
• the Unified Theories of Programming (UTP)

To implement the semantic navigator, we will specify and implement sentence and model translation maps from the BDS into the semantic frameworks S listed above. This allows us to translate each model M' interpreted by S into a model M interpreted by the BDS. The characteristic feature of an institution consists in the fact that then a property φ established for M interpreted by the BDS can always be translated into a property σ(φ) fulfilled by M' when interpreted in S.

This abstract concept has surprisingly concrete applications. Suppose, for example, that a testing theory has been established for models interpreted in the BDS. Such a theory results in a strategy how to identify relevant test cases in any model M interpreted in BDS. Test cases are represented symbolically as properties φ and are turned into concrete executable tests by determining traces through M satisfying φ. Executable tests, however, can also be expressed as properties φ', where variable symbols have been associated with concrete data values. If a model M' is transformed into some M using the corresponding signature morphism, we can generate symbolic test cases φ₁,...,φ_n in M according to the existing theory and use a constraint solver to create concrete cases φ₁',...,φ_n'. The latter can be lifted by means of the sentence translation map σ to concrete test cases σ(φ₁'),...,σ(φ_n') defined in M'. This results in a test suite for M' that has analogous properties (e.g., completeness) as the suite originally generated in M, because the signature morphism not only transfers properties, but also whole theories.

Summarising, the novel concept of a semantic navigator enables to apply tools and theories established at the level of the BDS and to map the results to any model interpreted in a semantics S where signature morphisms from BDS to S exist. This enables highly effective collaborative development, verification, and test of CPS with multiple formalisms and multiple semantic interpretations.

Publications

Theory Translation

• The following paper applies a testing theory translation between deterministic finite state machines (DFSM) and a variant of Kripke structures: it is shown that reactive systems with deterministic Kripke structure semantics and infinite input domains (while internal state and output domains are finite) can be abstracted to finite state machines exhibiting equivalent behaviour. Equivalence on FSM level is specified as language equivalence. Equivalence on Kripke structures is defined as I/O-equivalence, which means that both structures produce the same observable input/output sequences. Using the abstraction mapping Kripke models to FSM models, complete test suites for DFSM can be applied to the abstraction. These suites can be translated into test suites for systems in Kripke structure interpretation, and the completeness property of the DFSM suite is preserved in this translation.
  • Jan Peleska and Wen-ling Huang: Complete model-based equivalence class testing. Int J Softw Tools Technol Transfer. Published online: 21 November 2014. DOI 10.1007/s10009-014-0356-8.
• This paper describes a theory translation from the field of runtime verification. It is shown how health monitors (i.e. checkers monitoring a system under test with respect to specification violations at runtime) with certain characteristic properties can be constructed for systems interpreted in Kripke structure semantics. These results are then transferred to the CSP process algebra: using theory translation, health monitors with equivalent characteristic properties can be constructed for monitoring CSP processes.
  • Jan Peleska: Translating Testing Theories for Concurrent Systems. In: Correct System Design, Essays Dedicated to Ernst-Rüdiger Olderog on the Occasion of his 60th Birthday. LNCS (2015) - to appear.

Bounded Dynamicity Semantics

• Some basic ideas describing how complex distributed systems with changing configurations can be tested have been elaborated in the context of the COMPASS project. In
  • Wen-ling Huang and Jan Peleska: Comprehensive Modelling for Advanced Systems of Systems - Specialised Test Strategies
  general strategies for testing large distributed systems are described (Part II of the document) and approaches to testing dynamically changing system configurations are investigated (Part III of the document).