Within the area of Testing and Verification the overall trend is that systems of increasing complexity with an increasing number of features taking into account may be dealt with.

A definite trend is also, that model-checking and testing techniques are being applied directly to software validation (in particular C and JAVA) with noticeable successes given by the SLAM, Blast, VeriSoft, Bandera and JAVA-Path-Finder projects. Here, the method of abstraction-refinement provides a combination of abstract interpretation with model-checking with success within given application domains (e.g. SLAM and Blast addresses debugging of device drivers).

Another trend within the research area of verification is the (re-)discovery of SAT-solving as a technique for performing so-called bounded model-checking. Advances made on SAT-solving during the last 5 years has made this approach competitive compared to other techniques including symbolic model-checking. Members of the T&V cluster are active in pursuing extensions of SAT-solving to extended logics with quantitative aspects (difference constraints, linear constraints) in order to make bounded model-checking applicable to models of embedded systems.

Yet another trend is that the features and properties supported by current technology goes beyond that of pure functional correctness to also include timed, stochastic and hybrid phenomena. Within the Testing and Verification Cluster research on all of these quantitative extensions are pursued actively pursuing different techniques (bounded model checking, regular model checking, decision diagrams, automata for symbolic representation) are finding their way into powerful tools (e.g UPPAAL, IF, CMC, MoDeST, EMTCC, FAST).

Advances in verification technology (in particular the development of symbolic datastructures) are finding their way into mature testing tools (e.g TGV, STG, ToRX). Substantial effort has been made by several partners on model-based testing and monitoring of real-time systems with UPPAAL Tron and IF being some resulting tools. Also, related work on monitoring, controller synthesis, planning and scheduling, and schedulability analysis for real-time systems has been made resulting in tools such as TIMES and UPPAAL Cora and UPPAAL Tiga and several applications.

Model-driven development is highly appreciated in software engineering particularly because of the possibility of automatic code-generation. However, for quantitative models the realization on real hardware raises several problems. Indeed, the quantitative models are theoretical frameworks, assuming infinitely fast hardware, infinitely precise clocks, etc. However, these characteristics are not fulfilled on real CPUs, that are digital and have a finite frequency. Current research within the cluster is addressing this problem in the setting of real-time and involves identification on when (and how) given timed automata models are implementable and to what extent properties proved by the model also may be guaranteed to hold of the final implementation.

Within verification of security properties work has been made on the semantic foundations and the verification of security protocols and web-services. A general verification method for security protocols with possible unbounded sessions has been provided as well as a sound and complete inference systems for bounded-sessions cryptographic protocols. The work also include a classification and relation of different existing specification methods (multiset rewriting and process algebra) for security protocols as well as the use of standard model-checkers for analysing various security protocols (e.g. use of muCRL, SPIN and CADP) and for addressing security treats based on real-time issues (using UPPAAL).

In the area of parallel and distributed model checking of embedded systems we are in close collaboration with other research teams in Europe (INRIA Rhone-Alpes, CWI, Technical University Munich and Aachen Technical University) attempting to gather the European research communities working in the area on cluster and/or grids. Scientifically the work within the cluster has primarily focused on new algorithms for the enumerative distributed checking of reachability properties, and on extended the scope of efficient distributed algorithms to cover model checking of general CTL and LTL properties and of real-time models. The general environement DiVinE has been deployed and has also been extended by a Promela front-end for SPIN.

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet