This section discusses Quantitative Test and Verification, Verification of Security Properties, and the Platform for Testing and Verification.

 

 

 

 

Quantitative Test and Verification

An important step towards supporting quantitative analysis of real-time aspects is provided by the modeling formalism of timed automata. The potential of timed automata for the modeling and analysis of real-time systems has been documented extensively in the literature. Since their introduction by Alur and Dill in 1990, several verification tools for timed automata have been developed (in particular UPPAQAL, Kronos and IF) which are now applied routinely to industrial-size case studies.

More recently priced extensions of the timed automata formalism has been introduced - permitting consumption of resources to be taken into account. During this second year partners within the cluster has provided a number of results concerning decision problems wrt to this model of priced timed automata providing the foundation on which the future implementation within tools will be based. This involves design of datastructures and efficient algorithms. These are now to be found within the special purpose tool UPPAAL Cora.

Also controller synthesis and stochastic extension has been considered as well as the transfer of successful techniques for timed automata to classes of hybrid automata.
In addition, the foundational principles for generation of predictable code from timed automata models, and conformance testing based on timed automata models are being provided during this second year.

Significant effort on stochastic model checking has been made during the last decade. However, technology still lack for making stochastic analysis as tractable as that of analysis of timed or untimed models.

The partners are participating very actively in the research aiming to improve the above state of the art on specific areas within quantitative testing and verification as mentioned below, i.e. within the areas of timing, resources, schedulability, stochastic and hybrid aspects as well as testing theory,

Verification of Security Properties

Security engineering is about building systems to remain reliable despite the presence of malice errors. As a discipline, it studies and develops the tools and methods to design, implement and validate systems that guarantee security properties. Many security systems and in particular embedded systems have critical requirements. Their failure may cause serious economic damages (cash machines, electronic purse and other bank systems), endanger personal privacy (medical record systems), endanger the viability of whole business sectors (pay-tv), etc….

Within Artist2, the focus is on tools and methods needed to design embedded systems that guarantee security protocols. More specifically, the focus is on security protocols.
There are by now a number of efficient validation tools for authentication protocols, e.g., Hermes (Verimag), H1 (LSV), CASRUL (LORIA) mention tools developed by Artist2 partners.

Such validation tools have, however, not yet reached the level of maturity to be autonomously used by protocol designers. What is missing? A major obstacle is that these tools are based on a semantic model that is commonly called symbolic or Dolev-Yao model. This essentially means that cryptographic primitives are idealized and their behaviour is, hence, simplified.

Platform for Testing and Verification

Testing and verification of embedded systems are computationally hard and memory intensive activities as the underlying models contain (multiple) quantitative aspects in order to enable the expression of important properties concerning real-time constraints, impact on physical environment, expected resource consumption and performance of a given design, etc.

During the second year the partners of the cluster have been active in implementing, improving and disseminating a large number of testing and verification tools allowing for the analysis of quantitative models including real-time aspects, resource models, hybrid and stochastic models. We refer to the deliverable for the Testing and Verification Platform for a more detailed account. What is important to note here is that there is a very short distance (time-wise) from foundational decidability results to their impact on performance of tools in terms of improved datastructures and algorithms.

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

Réalisation Axome - Création de sites Internet