VERIMAG is one of the main European labs in embedded systems. It develops theory, methods and tools for safety critical and embedded systems. It has been established in 1993. It is a joint research unit belonging to the CNRS, the Universit Joseph Fourier Grenoble 1 and the Grenoble-INP technical university. Currently, it has a total staff of 82 persons including 26 permanent researchers, 7 researchers under contract and 30 Ph.D. students.

Expertise. VERIMAG aims to produce theoretical and practical tools for the cost-effective development of embedded systems of guaranteed quality. Quality includes properties such as security, safety, availability, and performance. Between 1993 and 1997, VERIMAG has produced and transferred, in collaboration with Verilog SA, and subsequently with Telelogic, the Lustre language which is the basis for the Scade environment, as well as verification and testing results integrated into the Object-Geode environment.

Several other results of VERIMAG have been transferred to industry as well. For instance, a verification tool dedicated to Lustre has been transferred to Prover-Technology, now part of Esterel-Technologies, and EADS and Schneider Electric benefit through long-term contracts from VERIMAG’s new techniques to develop safety critical systems. Other industrial partners are STMicroelectronics, Alcatel, CS-Transport, EDF, France Telecom, IBM, Intrasoft, ISD, Leti/CEA, RATP, Silicomp, Trusted Logic. VERIMAG has well-recognized competences in synchronous languages, validation and verification techniques focusing on security and safety, and modelling and analysis of temporal and hybrid systems.

Role in ASCENS. VERIMAG will bring into the project its expertise on component-based design of critical systems, correct-by-construction systems design methodology, and verification and synthesis techniques for embedded systems. VERIMAG will lead work package 5 on correctness of service components and service-component ensembles in coordination with the research performed in work packages 1 to 4 and 6. We will extend our portfolio of correctness techniques to the analysis and verification of service-component ensembles.

Key members