Abstract
Construction of powerful analysis tools by establishing a joint server platform providing extraordinary computational resources for conducting large-scale verification and testing efforts for embedded systems with respect to real-time requirements, quality-of-service guarantees as well as security properties.

The platform will provide a uniform, open and secure access and to all testing and verification tools of the academic as well as industrial partners of the consortium. The platform builds on existing works from the various partners and will also make available new powerful analysis tools developed within the network, in particular those from the related Joint Research Activities (“Quantitative Testing and Verification” and “Verification of Security Properties”).

Baseline

The teams collaborating on this activity are leading tool providers for testing and verification, with particular emphasis on real-time, hybrid and stochastic aspects.
Automatic analysis of such quantitative aspects are crucial in validating embedded systems, but are computationally significantly more difficult than validation of simple functional aspects.

Thus, to address industrial size models continued development of new algorithmic techniques and data structures should be combined with powerful computational resources. We seek to establish this by maximal use, coordination and extension of existing local resources (e.g. PC-clusters) and by exploiting on-going work on exchange between and combinations of tools.

Despite advances in algorithmic techniques verification and test case generation are computationally notoriously hard problems.

Consideration of quantitative phenomena (real-time, stochastic) adds to the complexity. Thus, to address industrial size models powerful computational resources are necessary for example by maximal coordination of existing local resources.

The computational resources of the platform will initially be provided by existing powerful stand-alone computers with the various verification and testing tools being made available via a common web-based interface. A procedure for controlling access in a flexible and secure (e.g. in accordance with the individual tools licence agreements) manner will be investigated.

Among the tools that will be made available we mention: SPIN, SMV, UPPAAL, Kronos, Blast, TorX, TGV, FAST, CADP, IF; HyTech, visualSTATE, TAU, LASH, EMTCC and Rapture where the individual consortium member will have responsibility for integrating their tools into the platform.

The emerging advances in parallel and distributed model checking also motivate the development of a generally accessible server platform consisting of local clusters of (inexpensive) PCs.

Long term vision includes an experimental GRID infrastructure targeted specifically towards verification and testing.

Problem Tackled in Year2

In order to pursue the overall goal of making the tools applied and developed by the cluster partners attractive for industrial usage, the following problems have been addressed in year 2:

• First of all, the individual tools have been further refined – both with respect to functionality and performance. This includes work on enabling the distribution of analysis techniques over a PC-cluster.
• Secondly, the work of dessimination of the tools through case study demonstrators has been initiated through the introduction of a joint web page for industrial case studies.
• Finally, in order to clarify the possibilities with respect to the establishment of an experimental Grid infrastructure, interaction with European Grid activities has been initiated.

Previous Work

During the first 12 months a number of improvements have been made on the individual tools as developed by the partners:

• The Vertecs team (IRISA) supports two test generation tools: TGV and STG. During the period, a new version of TGV (based on on-the-fly enumerative algorithms) linked to the IF toolbox (Verimag) has been developed using STL libraries (in place of CADP libraries).
• Results have been implemented in the TIMES tool for automated schedulability checking.
• CFV supports the verification tool LASH and hosts powerful servers dedicated to verification tools.
• A number of improvements have been made on the Uppaal real-time model checker (www.uppaal.com). This includes the possibility to enrich the timed automaton models with C code. An extension of Uppaal (Uppaal Cora), dedicated to solving optimal scheduling and planning problems, has been introduced. Recently, a version of Uppaal (Uppaal Tron), dedicated to online testing of real time systems, has been announced.
  Also, a general distributed verification environment (DiVinE, Brno) has been deployed. The environment supports the development of distributed enumerative model checking algorithms, enables unified and credible comparison of these algorithms, and makes the distributed verification available for public use in a form of a distributed verification tool.
  Finally, an overview of existing tools has been made accessible via a common web portal (the Yahooda web-page maintained by Brno).

Current Results

Development of existing and new tools
Brno has completed deployment of the distributed verification tool "DiVinE" (version 0.7) for enumerative model checking of LTL properties on a network of workstations. This includes the development of new algorithms for cluster-based decomposition of state spac into strongly connected components to be used in reduction of state spaces
Neijmegen has recently implemented an initial extension of the TorX tool (TorXakis) for symbolic testing – based on the formalism of Symbolic Transition Systems.
IRISA has worked on symbolic test selection for extended automata using abstract interpretation and included the results by improving test selection in their toolset STG.
Verimag has continued work on conformance testing for real-time systems and in particular worked on general improvements on the tool TTG (Timed Test Generator).

A new version of UPPAAL (Aalborg, Uppsala), UPPAAL 4.0, has been released with a number of new facilities and algorithms user defined functions (syntax follows the style of C/C++/Java, and most control-flow constructs of C are supported), priorities and channels may be specified and dealt with during analysis, full support for symmetry reduction is implemented enabled by the introduction of a scalar datatype and the so-called swep-line method may be used to reduce memory consumption.
The online testing tool Uppaal Tron (Aalborg) has been ported to MS windows, and a new version 1.4 has been released. This represents a significant development effort since the OS and development environments on windows are quite different from those of Linux. We have identified specific technical problems with timing under windows. We believe that the windows version will greatly extend the applicability of the tool
A new variant of Uppaal, Uppaal Tiga, for the analysis and synthesis of winning strategies for times games has been released. Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.

Evaluation of tools
The planned work on tool dissemination and evaluation through case studies has been initiated through the establishment of an open repository for Artist2 Test and Verification Case Studies (https://bugsy.grid.aau.dk/artist2). The repository can be maintained by the individual tool providers and users through the use of Wiki.

Exploiting European Grid activities
ARTIST2 partners have participated in two European meetings on parallel and distributed model checking where the issue of exploiting grid activities to build a joint infrastructure has been discussed. The meetings showed that

• here are a number of ongoing European projects with respect to the usage of high performance and Grid-based servers for model checking. Each of the projects have made contributions through new distributed algorithms, new parallel architectures and new interesting applications, and it is likely that these activities will be their main focus for the immediate future. This means that the question of mutual exploitation of resources and the provision of a common web interface will be postponed for the time being.
• The long term vision of a joint high-performance verification platform is still relevant and should be maintained.
• There are already a number of facilities (e.g.) NorduGrid available that may be exploited be the individual tool providers and users. So far, a distributed version of Uppaal (DUppaal) has been made available on the NorduGrid in a certified manner via manual certificate distribution.

Publications Resulting from these Achievements

 J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova: Distributed Qualitative LTL Model Checking of Markov Decision Processes. PDMC 2006.
L. Brim: Distributed Verification: Exploring the Power of Raw Computing Power. PDMC 2006.
 J. Barnat, L. Brim, I. Cerna, P. Moravec, P. Rockai, P. Simecek: DiVinE - The Distributed Verification Environment. CAV 2006.
 L. Brim, I. Cerna, P. Moravec, J. Simsa: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. Electr. Notes Theor. Comput. Sci. 135(2): 3-18 (2006)
 J. Barnat, P. Moravec: Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. PDMC 2006.
 J. Barnat, L. Brim, I. Cerna: Distributed Analysis of Large Systems. FMCO 2005.
Elena Fersman, Leonid Mokrushin, Paul Pettersson, Wang Yi : Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354(2): 301-317 (2006).
 B. Blanc, F. Bouquet, A. Gotlieb, B. Jeannet, T. J’8eron, B. Legeard, B. Marre, C. Michel, M. Rueher : The V3F Project. in Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA’06), Sept 25-29, Nantes, 2006
 L. Frantzen, J. Tretmans, T. Willemse. Test Generation based on Symbolic Specifications.In: J. Grabowski, B. Nielsen (eds.),FATES 2004 - Formal Approaches to Testing of Software.Lecture Notes in Computer Science 3395, pp. 1-15, Springer-Verlag, 2005.
 L. Frantzen, J. Tretmans, T. Willemse. A Symbolic Framework for Model-Based Testing.In K. Havelund, M. Nunez, G. Rosu, B. Wolff (eds.),Formal Approaches to Testing and Runtime Verification - FATES/RV’06.Lecture Notes in Computer Science. Springer-Verlag, 2006. To appear.
 Kim Guldstrand Larsen, Marius Mikucionis, Brian Nielsen, Arne Skou: Testing real-time embedded software using UPPAAL-TRON: an industrial case study. In proceedings of EMSOFT 2005.
 Anders Hessel, Kim Guldstrand Larsen, Marius Mikucionis, Brian Nielsen, Paul Pettersson, Arne Skou: Automated Model-Based Conformance Testing of Real-Time Systems. Book Chapter: “Formal Methods and Testing” Editor(s): Jonathan Bowen, Mark Harman, Rob Hierons, Publishing institution: Springer Verlag 2005. Number of pages: 39. To Appear.
 Gerd Behrmann: Distributed reachability analysis in timed automata. In STTT: Software Tools for Technology Transfer 7 (1): 19-30 (2005)
 Gerd Behrmann, Alexandre David, Martijn Hendriks, John Håkansson, Kim G. Larsen, , Paul Pettersson, Wang Yi. UPPAAL 4.0. In Proceedings of the Third International Conference on Quantitative Evaluation of Systems, Riverside, CA, USA, September 11-14, 2006.
 Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, Didier Lime: Efficient On-the-Fly Algorithms for the Analysis of Timed Games. CONCUR 2005: 66-80
 Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen, Didier Lime: UPPAAL Tiga: Timed Games for Everyone. To appear in Nordic Workshop of Programming Theory, Iceland, October 2006.

Keynotes, Workshops, Tutorials

• Keynote: Real-time Modle Checking using UPPAAL by Kim G. Larsen. TCS Excellence in Computer Science (TECS) Week 2006, Pune, India, January 3–7 2006,
• Workshop: SENVA Meeting on Clusters and Grids for Verification and Performance Evaluation
  INRIA Rhône-Alpes - Montbonnot (Isère), France, November 16-17, 2005
  The aim of this workshop was to present algorithms and tools for distributed analysis of concurrent systems. It was arranged by the SENVA project – a joint CWI, INRIA project on safety critical systems. ARTIST2 partners from Aalaborg and Brno made contributions to the presentations and discussions.
• Workshop: SENVA Meeting on Parallel and Distributed Verification
  CWI, Amsterdam, The Netherlands, April 3-4, 2006-09-19
  The workshop was dedicated to algorithms, tools and case studies for parallel and distributed verification. It was arranged by SENVA in collaboration with a Dutch national project and with contributions from the ARTIST2 partners Aalborg and Brno.
• Workshop: 5th International Workshop on Parallel and Distributed Methods in verification, PDMC 2006
  August 31, 2006, Bonn, Germany
  The PDMC workshop aims to provide a working forum for presenting, sharing, and discussing recent achievements in the field of parallel and distributed verification. The workshop consists of invited talks and a selection from the submitted papers. It was co-located with CONCUR 2006. ARTIST2 partners served as invited speaker, committee mebers and also presented accepted papers.
• Tutorial: Tutorial on UPPAAL by Gerd Behrmann, Alexandre David, Kim G. Larsen (Aalborg U.) and Paul Pettersson, Wang Yi (Uppsala U.). The 26th IEEE Real-Time Systems Symposium, http://www.rtss.org/rtss2005, Miami, Florida, USA, December 5-8, 2005
• Tutorial: Model-based Testing and Validation of Real-Time Systems by Kim G. Larsen and Brian Nielsen. TAROT Summerschool on Testing, http://www.info-ab.uclm.es/tarot/, Toledo, Spain, June 26 - July 1, 2006
• Tutorial: Verification of UML models by Susane Graf (Verimag). ARTIST2 Summer School on Components & Modelling, Testing & Verification, and Static Analysis of Embedded Systems, Nässlingen, Sweden, September 29 - October 2, 2005.
• Tutorial: On-line Testing for Real-time Systems by Brian Nielsen (Aalborg). ARTIST2 Summer School on Components & Modelling, Testing & Verification, and Static Analysis of Embedded Systems, Nässlingen, Sweden, September 29 - October 2, 2005.
• Tutorial: Real-time Model Checking by Gerd Behrmann (Aalborg). ARTIST2 Summer School on Components & Modelling, Testing & Verification, and Static Analysis of Embedded Systems, Nässlingen, Sweden, September 29 - October 2, 2005.

ARTIST2 Participants: Expertise and Roles

• Team Leader: Ed Brinksma (University of Twente)
  verification and testing of reactive and stochastic systems.
• Team Leader: Pierre Wolper (Centre Fédéré de Verification)
  model checking.
• Team Leader: Philippe Schnoebelen (LSV)
  model checking.
• Team Leader: Thierry Jeron (INRIA)
  testing theory and tools.
• Team Leader: Yassine Lakhnech (Verimag)
  infinite state model checking.
• Team Leader: Wang Yi (Uppsala)
  model checking for real-time systems.
• Team Leader: Tom Henzinger (EPFL )
  model checking of embedded software and hybrid systems.

Affiliated Participants: Expertise and Roles

• Team Leader: Lubos Brim (University Brno)
  distributed model checking.
• Team Leader: Henrik Leerberg (IAR Systems A/S)
  tool provider.
• Team Leader: Tommy Ericsson (Telelogic)
  tool provider.
• Team Leader: Jan Tretmans (Nijmegen)
  models and tools for model based testing
• Team Leader: Sven H. Sørensen: (Motorola A/S)
  end user.
• Team Leader: Thomas Hune: (Terma A/S)
  end user.

Réalisation Axome - Création de sites Internet