TTI project proposal

1. Title

Systems Validation Centre (SVC)

2. Synopsis

The SVC project is devoted to fundamental and applied research in the area of system validation for telematics systems. System validation is concerned with techniques and tools for the (automated) analysis of the (functional) correctness of specifications, designs and products. In the project validation methods and tools will be developed, applied, evaluated and improved on the basis of real-life applications. Important validation techniques that will be used in the project are simulation, model checking, verification and testing.

This project aims to secure the position of the Telematics Institute with respect to strategic expertise in the area of system validation. To achieve this the project builds on existing activities with a proven track-record in applicability. It is intended that in the course of the project new spin-off projects will be started in the form dedicated validation studies for organisations with specific validation needs. Such special studies will be carried out as separate contract research. This can ultimately lead to a Systems Verification Centre offering state-of-the-art validation support as a standard TI service.

To coordinate the interaction with industry the project has a steering committee consisting of industrial experts that have an interest in applying validation methods and tools within their organisations. Initially, the application of validation methods will be studied on the basis of jointly selected case studies. Later feedback will be based on the aforementioned larger spin-off validation projects. The project will also carry out pro-active studies into generally applicable state-of-the art validation techniques, maintaining working sets of succesful tools and techniques, and awareness of similar projects and developments elsewhere. As a centre of expertise for system validation SVC will also actively promote knowledge and technology transfer to industry in the area of validation methods and tools through publications, presentations, demonstrations, courses and workshops.

The research partners of this project are the CTIT, CWI and Telematics Institute. Industrial support from with the Telematics Institute consortium has been obtained from CMG, IBM, KPN and Lucent. Additional support has been obtained from Rijkswaterstaat and Holland Railconsult.

[Systems Validation Centre approach]

3. Objectives & advances

The SVC project aims to achieve several goals at a time, all of which are directly in line with the aims and objectives of the Telematics Institute. The specific objectives of the project are:

  1. to advance the state-of-the-art in validation techniques and tools by a combination of fundamental research and practical application;
  2. to increase the competence of the Telematics Institute in the field of system validation by carrying out realistic validation studies;
  3. to increase awareness, knowledge, and acceptance of system validation techniques among TI projects, partners and clients by knowledge and technology transfer;
  4. to become a knowledge centre for the application of validation techniques by means of structural inventorisation of such techniques, related tools and their applications.
  5. to establish a TI Systems Validation Centre that carries out specialist validation services for TI projects, partners and clients on the basis of contract research.

These objectives will be realised by the two main activities of the project, which will be carried out in a closely interwoven fashion:

  1. fundamental research into the improvement of validation techniques and tools;
  2. technology application, evaluation, transfer, and support.

4. Compliance with aims and objectives of the TI

The proposed project is of direct relevance for all the TI research clusters that involve the technical design of (parts of) telematic systems. Effective validation methods and tools are a strategic asset for the fast development of reliable telematic systems. The project contributes concretely to the knowledge and technology transfer to industry in the area of state-of-the-art validation techniques. Moreover, it promotes the international visibility of the TI as a centre of expertise for system validation. Finally, the project is set up in such a way as to promote contract research in system validation.

Telematic systems provide increasingly critical services to their users. This makes the reliability of their functioning a key issue of their design. Because of the usually great complexity of such systems and the pressure to reduce their design and development time ("time to market"), the use of advanced techniques and tools to check the validity of designs is of increasing importance. Validation issues are very relevant for most of the TI research clusters (see Scientific Programme for the first cycle, clusters 1-6, cf. e.g. section 1.3.2).

In spite of the importance of the use of advanced validation techniques, many projects pay only lip service to the systematic validation of their designs. An important reason is that the availability of practically usable validation techniques is relatively new, and that experts that know how to develop and apply them are scarce. The use of advanced validation techniques, moreover, is quite sophisticated and often requires specialist knowledge and skills that are unrelated to the application domain of the system itself. The above arguments suggest that the TI should concentrate its validation efforts and expand its expertise in this area, making it available to client projects within and outside TI, instead of following a policy where validation efforts are just scattered over many different projects.

Internationally leading research groups in system validation are active within the TI consortium. The Formal Methods and Tools Group of the CTIT and the SEN2 Theme of CWI have a worldwide reputation in the development and practical application of formal methods and tools for system specification and validation. In recent years practical validation has been carried out in collaboration with external partners such as Philips, Bosch-Blaupunkt, Nederlandse Spoorwegen, CMG, Rijkswaterstaat and others on real-life systems for car automation, consumer electronics, control systems, railway safety, etc. The activities of the Telematics Institute in the TESTBED project have lead to the creation of an advanced architecture and software environment for the integration of software tools, which can be used for the creation of integrated validation environments. Members of the TESTBED Tools team have extensive experience in software tool development and integration.

Given the experience, past achievements and mixture of common and complementary skills, these groups and their expertise form an excellent starting point for the proposed project. Nevertheless, it is intended that the project is based on an open consortium, where efforts can be strengthened further by the involvement of other groups, now or later.

5. State of the art: analysing complex systems

Based on the use of formal methods a host of techniques to analyse system behaviour has been developed in the last two decades. Using constructive formal description techniques system designs can be defined in terms of precise and unambiguous specifications that provide the basis for systematic analysis. Tool environments consisting of static semantic checkers and animators allowing system simulation can be used for a quick assessment of the quality of specifications.

Based on the specifications of the system behaviour models can be obtained that can be systematically checked with respect to given properties. Such properties must be formalised in an appropriate logical language, usually in a modal logic involving special operators that represent temporal and/or spatial aspects of system behaviour. This technique of so-called model checking is one of the more effective validation methods currently available. One of the advantages of this approach is that implementations can also be verified against partial specifications, by considering only a subset of all specification requirements. This allows for increased efficiency by checking correctness with respect to only the most relevant requirements that should be fulfilled.

Verification is the mathematical demonstration of the correctness of the behaviour of an implementation model with respect to its specification. In priciple, this yields a complete analysis of the system implementation. In some cases such proofs can be carried out by computer, using appropriate algorithms, otherwise proofs are by hand, using an adequate proof methodology. In the latter case, to overcome human fallibility, techniques have been developed to check the proofs by computer. These proof checking techniques are difficult and labour intensive to apply, but when succesful give an unparalleled level of precision and reliability of the proofs.

Testing is a technique that can be applied both to prototypes, in the form of a systematic simulation, and to final products. Two basic approaches are transparent box testing, where the internal structure of an implemention can be observed (e.g. in the form of the source code), and black box testing, where only the communication between the system under test and its environment can be observed. In reality, testing is mostly somewhere in beteen these two extremes, which is referred to as so-called grey box testing. Testing is the validation technique that is most used in practice, but almost exclusively on the basis of informal and heuristical methods. Such procedures can be improved significantly by the use of formal methods, especially in the area of the (semi-)automatic generation and selection of test cases from formal specifications.

Current methods and technology provide the means for the specification, static analysis and simulation of large real-life systems. Systematic testing and model checking, however, is generally limited to systems with state spaces of the magnitude of 108 states. Verification based on syntactic manipulation of specifications is not restricted by the size of the state space, but by the size of the specification itself. Proving properties by hand is limited to system descriptions that do not extend beyond a few pages. Although this limits the scope of the current validation techniques, they are being applied sucessfully in practical validation studies for real-life applications. Success stories involving the groups from CTIT and CWI include the validation of the BOS control system of the storm surge barrier in the Nieuwe Waterweg, and the analysis of a much implemented sliding window protocol specification. In both cases unknown, but fatal flaws were exposed.

In spite of these and many other succesful applications of validation techniques, many systems still fall outside the scope of the current methods and tools. Even small to medium size systems can have state spaces in the order of 101000 states. Most of these systems will also require more than a few pages of specification. An important goal of the project, therefore, is intended to work towards closing the gap between the current limits of technology and the size of `real' systems.

One way to handle very large state spaces is to encode them efficiently in propositional logic (e.g. the reachability of a state can be encoded in one bit). Such encoding can be further optimised by the sharing of common code fragments using Binary Decision Diagrams (BDDs) and related techniques. The BDD-literature features claims of state spaces of up to 101300 states that have been analysed in this way. Based on completely different propositional techniques the prover HeerHugo has been used at CWI to show the safety of railway guarding systems with at least 101000 states.

Experience indicates that individual characteristics of systems are very important for the success of these methods. There are examples where BDDs are ineffective, whereas provers like HeerHugo are successful, and vice versa. There are even examples were propositional encoding performs worse than explicit state space analysis. As yet, there is little understanding of how the success of the different methods depends on the characteristics of systems at hand, and indeed of the relative power of the different propositional encoding techniques.

A second approach towards a more efficient representation of state spaces is the use of so-called true concurrency models. The state space explosion problem typically exists with systems that consist of many components running in parallel. Most behavioural models use a so-called interleaving semantics that creates global states by all possible cominations of local states. This makes state spaces grow with the product of the sizes of the local state spaces. In true concurrency models information is defined in terms of the causal dependencies between system actions. The complexity of this information grows only with the sum of that of the components.

Yet another approach is to somehow reduce the state spaces that must be generated or maintained. Typical examples are on-the-fly state space generation (generating only those parts of the state space that are really necessary at a given moment), and partial order reductioen techniques (creating only one instead of all interleavings of independent local behaviours). Still another technique is that of state abstraction (representing many states by one), which can be used to suppress irrelevant information for the validation property in question. A typical example is to replace unimportant system components by single state systems.

The effects of the use of such techniques can be substantially amplified if the models used are compositional with respect to common operators for system synthesis, e.g. parallel composition. This means that the model (properties) of the entire system is (are) functions of the model (properties) of its components. In the common interleaving approach the global state space reduction is the product of the local reductions, resulting in a reduction that is exponential in the number of components.

A completely different approach is to exploit the regularity of the syntactic structure of specifications in order to reduce complexity. In many (protocol) systems the ultimate state space can be huge, whereas the internal structure may be quite simple, or be transformed int=o something with a highly regular structure. This can be exploited to reduce the size of the generated state spaces quite drastically, or even avoid the generation of large semantic models altogether.

An important technique in this vein is the symbolic treatment of data values. Large domains of data types can cause arbitrary blow-up of state spaces, whereas the qualitative behaviour of systems depends only on the effect that data values have on conditional control structures. This leads to equivalence classes of data values, where the number of classes can be small even if the domains are infinite. Many problems can be solved by representing the classes instead of the data values. Moreover, the classes can be constructed using on-the-fly methods. This approach is followed in many simulators, e.g. the LOTOS simulator Smile.

An entirely different way to keep the representation of large state spaces small is by encoding the states by data parameters, and characterizing the behaviour of the system by condition-effect functions. The descriptions obtained in this way are referred to as linear process equations. They yield descriptions with a very regular structure. Such techniques can be applied to process algebraic specification formalisms that include features for the specification of data, such as muCRL and LOTOS. First studies on transforming arbitrary muCRL process descriptions, including parallelism, into this form are promising in the sense that medium-sized systems can be easily transformed into this format.

For checking the behavioural equivalence between specifications and implementations of systems the so-called cones and foci proof system has been developed. If specification and implementation are both given as linear process operators, the problem is reduced to six classes of identities on data parameters. Although these identities are not always easy to prove, they do capture the essence of the distributed system under study. Moreover, they lead the way to automatic assistance, for instance by generating these classes of identities automatically, and by solving at least the trivial ones automatically.

The same principles may be exploited for checking logical requirements. Current research aims to develop proof systems for modal formulas with data on linear process operators. After identifying the basic rules, it is intended to develop a proof methodology, in the same style as the cones and foci method to make proving such modal formulas efficient.

Current process description languages, such as LOTOS, SDL, muCRL, CHILL, Erlang and Promela have been designed to model concurrent, communicating systems with discrete events. They are much less suited, however, for the specification and, in particular, the analysis of quantitative features such as timed, probabilistic, and stochastic behaviour.

Networking systems and telematics applications, however, crucially depend on the correctness of their quantitative behaviour, which is usually encoded in their Quality of Service (QoS) parameters. Typical examples are such measures as maximal delay, throughput, jitter, failure ratios, etc. In modern network and multimedia systems the difference between functional and quantitative properties has become blurred. This also holds for the class of so-called embedded systems , which is rapidly gaining importance for the modelling of all sorts of (safety) critical applications.

During the past decade a lot of research has been carried out in the area of timed specification languages. One of the most significant developments has been the introduction of the timed automata model. In this model infinite state spaces due to continuous time parameters can, under reasonable conditions, be reduced to a finite set of region graphs allowing algorithmic property checking. In this way, although still for relatively small systems, modal properties and trace inclusions can be checked.

Compared to timed systems much less research has been devoted as yet to the development, and especially the application of probabilistic systems (where nondeterministic choices are resolved with specified probabilities) and stochastic systems (where timed action occurrences are determined by probability distributions). In the performance analysis community research into so-called stochastic Petri nets has some tradition. In search of a compositional theory of stochastic systems also research in the area of Stochastic Process Algebras (SPA) has started to flourish. The potential benefits of these models is great, as they can be used for the structured specification and analysis of functional and stochastic system features in one model. Process algebraic models can be related to both labelled transitions systems, being the basic model of functional behaviour, as well as to well-know analytic and simulation models of stochastic behaviour such as (generalised) (semi-)Markov processes. Although application examples here are still of small systems only, much progress is expected here, because of the underlying compositional model.

6. Approach, organisation & work plan

6.1 Fundamental research

Research into the systematic improvement of validation methods and tools can profit from the substantial progress that is being made in the very active international validation research scene. We will focus on two main research tasks that are highly relevant for the validation of telematics systems.

  1. Fighting complexity
    Formal models of medium and large size specifications tend to grow much too large to check their correctness effectively. This problem is usually known as the combinatorial or state space explosion problem . This calls for special means to curb this complexity, such as compression, reduction and abstraction techniques. Complementary syntactical techniques, such as structural analysis and symbolic data representation, can be used to reduce the size and/or complexity of specifications even before the generation of semantic models.
  2. Extending expressivity
    The importance of quality of service parameters for most telematics systems and applications calls for formal techniques for the specification and analysis of real-time and stochastic behaviour in addition to their qualitative functional behaviour.

6.1.1 Fighting complexity

The approaches of task A to overcome the gap can be divided into three main classes.

6.1.2 Extending expressivity

Task B aims at the extension of existing models of behaviour to accommodate the specification and analysis of quantitative features.