Rapport semestriel d’activité -coordonnateur
Programme SETIN - Edition 2006
http://www-anr-ci.cea.fr

Rappel : le coordonnateur doit fournir un rapport partenaire et un rapport coordonnateur.

1	Identification

Acronyme du projet	VAL-AMS	
Numéro d'identification de l'acte attributif	ANR-06-SETI-018-01	
URL de la page web du projet	http://www-verimag.imag.fr/~tdang/VAL-AMS	
Coordonnateur (société/organisme)	Laboratoire VERIMAG	
Période couverte (date à date)	01/01/2007 – 31/06/2007	
Période couverte (t0+n mois à t0+m mois)	t0  à t0+6 mois	
Rédacteur (nom, téléphone, email)	

Thao Dang, tel : 04 56 52 03 83, Thao.Dang@imag.fr
	
Date	30 juin 2007	

2	Synthèse des rapports des partenaires

Reprendre ici les indications des rapports des partenaires du projet.

Numéro
du
Partenaire	Conformité des résultats obtenus aux prévisions	Conformité de la consommation des ressources par rapport aux prévisions	Difficultés particulières	
1	Yes	Yes		
2	Yes	Yes		
3	Yes	No	Delay in the recruitment of the engineer	
4				
5				
6				
7				
8				
9				
10				

Synthèse
	Yes	No		

Commentaires

3	Activités de coordination du projet 

3.1	Réunions

Réunions passées

Date	Participants (numéro des partenaires)	Objet	
Jan 18 2007,
at Inria Rhône-Alpes	
01, 02, 03	•	Talk titled “SICONOS platform and summary of the non-smooth approach”, given by Pascal Denoyelle and Vincent Acary (BIPOP – Inria Rhône-Alpes)  
•	Discussion on circuit equation generation and optimization 	

March 2, 2007. At VERIMAG	
01, 02, 03	•	Talk titled “Test coverage for continuous and hybrid systems”, given by Thao Dang (VERIMAG)
•	Discussion on translating standard circuit description languages to the input language of the SICONOS platform
•	Discussion on an intermediate circuit description format using Simulink	

April 17, 2007. At INRIA Rhône-Alpes	
01, 02, 03	
•	Talk titled “Behavioral metrics and application for circuit validation“, given by Antoine Girard (LJK) 
•	Discussion on extraction of circuit equations from a Spice netlist.
•	Discussion on connecting the tools developped in WP1 and WP2 with the SINOCOS platform

June 12, 2007. At VERIMAG	
01, 02, 03	
•	Summary of the results obtained and preparation of the semestrial report

June 28, 2007 
Inria, Rhône-Alpes	
01, 02, 03	 
•	Demonstration of the SINOCOS platform,
•	Discussions on tool integration

Compte-rendu de la réunion de lancement
Summary of the kick-off meeting. 

Date and location: Thanks to the proximity of the partners’s locations, we could organize 4 meetings on different days (see the above table). 

Participants: All the permanent members of the project were present at each meeting.

Contents
•	Scientific topics: The above table summarizes the scientific topics discussed in the meetings. 
•	The discussions on administration issues include the web-site of the project and the announcement of the job offers (to recruit the engineers and postdoc for the project)

3.2	Faits marquants
Indiquer les résultats et/ou réalisations marquants. Préciser s’ils peuvent ou non faire l’objet de communications externes par l’ANR et la Délégation ANR-CIGC. Merci de nous fournir le cas échéant des présentations/posters du projet pour enrichir notre site web.

Publications :
1.	Antoine Girard, Approximately Bisimilar Finite Abstractions of Stable Linear Systems, in Hybrid Systems : Computation and Control, vol 4416 in LNCS, pp 231-244, Springer, 2007. 
2.	Alexandre Donze and Oded Maler, Systematic Simulation using Sensitivity Analysis, in Hybrid Systems : Computation and Control, vol 4416 in LNCS, Springer Verlag, 2007.
3.	Tarik Nahhal and Thao Dang, Randomized Guided Simulation, in Hybrid Systems : Computation and Control, vol 4416 in LNCS, Springer Verlag, 2007.
4.	Tarik Nahhal and Thao Dang, Test Coverage for Continuous and Hybrid Systems, in Computer Aided Design, LNCS, Springer Verlag, Berlin, July 2007.

3.3	Statut de l'accord de consortium
Préciser si l'accord de consortium a été signé.

3.4	Difficultés rencontrées ou prévisibles

The recruitments of an engineer by BiPOP (partner 03) and of a postdoc by LJK (partner 02) have been delayed, due to the lack of candidates with the required competences. 

4	Avancement du projet

4.1	Suivi de l'avancement des tâches du projet
Lister pour chaque tâche du projet [WP], l'état d'avancement et le comparer aux prévisions.

WP1 – Coverage guided simulation

Due to the gap between the capacity of exhaustive formal verification methods and the complexity of embedded systems, simulation and testing are still the most commonly-used validation methods in industry. Since it is impossible to enumerate all the admissible external inputs to the hybrid system, much effort has been invested in defining and implementing notions of coverage that guarantee, to some extent, that the finite set of input stimuli against which the system is tested is sufficient for validating correctness. For discrete systems, specified using programming languages or hardware design languages, some syntactic coverage measures can be defined, like exercising every statement or transition, etc. In hybrid systems that operate in a metric space (typically Rn), there is not much inspiration coming from the syntax to the coverage issue. Nevertheless, the metric nature of the state space encourages more semantic notions of coverage, namely that all system trajectories generated by the input test patterns form a kind of dense network in the reachable state space without too many big unexplored `holes'. The results achieved in the context of this work package can be summarized as follows.

 	1. Definition of coverage measure. We proposed a test coverage measure for hybrid systems, which is defined using the star discrepancy notion from statistics. This coverage measure is used to quantify the validation `completeness'. It is also used to guide input stimulus generation by identifying the portions of the system behaviors that are not adequately examined.

2. Coverage-guided simulation algorithm We proposed a coverage-guided simulation algorithm, which is based on the RRT (Rapidly-exploring Random Tree) algorithm from robotic motion planning. The simulation is indeed guided by the above coverage measure.
.
Current work includes extending this simulation approach to hybrid systems testing with a focus on applications to circuits.

WP2 – Verification by simulation

Bisimulation metrics make it possible to define a notion of neighbourhoods for trajectories of a dynamical system. Then, it becomes possible to sample sets of trajectories with a precision that can be chosen arbitrarily small. As a consequence, it is possible to prove some properties satisfied by all the trajectories of a system by simulating only a finite number of them. The line of research we developed on this topic since the beginning of the project follows two main directions:

	1. Property-guided simulation. The number of trajectories that need to be simulated in order to achieve a certain precision grows very fast, making it very hard in practice to sample uniformly the set of trajectories. Moreover, when interested in a particular property (e.g. absence of overshoot in a circuit), a uniform sampling is usually not necessary to prove the property. Indeed, the sample needs to be precise around trajectories that almost violate the property whereas it can be very rough around trajectories that clearly satisfy the property. We developed an algorithm that allows us to sample the set of trajectories adaptively. Starting from a rough sample, we refine it iteratively and locally by analyzing how far the trajectories are from violating the property. We evaluated the algorithm on small examples and it shows good performances. Experimentally, we can see that the number of trajectories that need to be simulated is a polynomial function of the robustness of the property: if the system satisfies quite robustly the property, then we will need to simulate very few trajectories. Current work includes further improvements of the algorithm in order to merge neighbour trajectories when it is possible, reducing the number of trajectories in the sample.

	2. Finite abstractions of continuous systems. The sampling property associated with the existence of a bisimulation metrics allows us to compute finite state approximations of continuous (therefore with an infinite number of sates) systems. The construction of the approximation only involves the simulation of a finite number of trajectories and thus it can be effectively implemented in practice. Any desired accuracy can be achieved. The finite abstractions that we obtain can then be used for property verification (using a model checker for finite systems) or controller synthesis (using supervising controllers or dynamic programming). This work, in the context of linear dynamical systems, has been presented at the last conference on Hybrid Systems: Computation and Control in Pisa. The extension of this work to nonlinear systems is currently under development in collaboration with Giordano Pola and Paulo Tabuada from University of California at Los Angeles.

WP3- Advanced numerical analysis techniques 

The development of a robust electronic simulator based on the non-smooth approach 
involves to enlarge the existing set of resolution techniques and to provide a set of models of 
electronic devices and an automated formulation of circuits equations. 

          1. Resolution techniques.The application of the non smooth approach to mechanics yields specific kind of linear complementarity problems (LCP) that are efficiently solved with dedicated resolution techniques (LCP solvers). When one deals with electronic circuits, the arising LCPs are rather different and generally require other LCP solvers. Thus the available set of solvers was enlarged during this first semester. Successful tests were performed on samples of electronic circuits formulated as non smooth dynamical systems. 

          2. Development of an automatic DAE and LCP formulation tool. A bibliographic study has been carried on during this semester. We have gained a good insight into 
the solutions implemented in the state-of-the-art simulator SPICE coming from the smooth approach. A part of these solutions will be reused in our formulation tool besides the handling of the non smooth elements. 

The hiring of an engineer has been delayed due to the lack of candidates with the required competences so that the specification of this tool will start during the second semester. 

WP4 – Tool development and application to analog and mixed-signal circuits

1. Coverage-guided simulation tool. We have implemented the coverage-guided simulation algorithm in a prototype tool and  tested on a number of benchmarks from control applications and analog circuits.
2. Tool integration. We have investigated the problem of defining an intermediate input language for tool interface and integration. The connection between the high-level simulation methods (developped in WP1 and WP2) and the simulation kernel (developped in WP3) is under progress. 

4.2	Suivi des délivrables du projet
Reprendre ici le tableau initial des livrables contenu dans l'annexe 1 des actes attributifs et le mettre à jour en fonction de la production des livrables. Le code à utiliser est le suivant : X prévision initiale, A atteint, Rn reprévision.
Préciser la raison de chaque reprévision de délivrables (Rn)

	Libellé	Type	Partenaire pilote	Partenaires
Participants	Date
T0 + months	Status	

1	Website
http://www-verimag.imag.fr/~tdang/VAL_AMS	
Website	
VERIMAG	
BIPOP, 
LJK (LMC)	

T0 + 1	

A	

1	Coverage guided simulation
techniques and application
to AMS circuits	
Research
report	
VERIMAG		

T0 + 6	

A	

2	Coverage guided simulation
tool	
Software	
VERIMAG	
BIPOP	
T0 + 12	
X	

3	Verification using
bisimulation metrics	Research
Report	
LJK (LMC)		
T0 + 6	
A	

4	Compositional bisimulation
metrics	Research
Report	
LJK (LMC)		
T0 + 12	
X	

5	Automatic DAE and LCP
matrices assembly from a circuit description	
Research
Report	
BIPOP		
T0 + 12	
X	

6	Tool for DAE and LCP
formulation	
Software	
BIPOP		
T0 + 18	
Rn	

7	Heuristics to speed up
simulation	Research
report	
BIPOP		
T0 + 24	
X	

8	Tool box for validation of
AMS circuits	
Software	
VERIMAG	
BIPOP, 
LJK (LMC)	
T0 + 24	
X	

The rescheduling (`reprévision’)  of the delivrable 6 is due to the delay in the recruitment of the engineer who is in charge of implementing the tool. We have extended its preparation time for additional 6 months.

5	Utilisation des aides ANR

5.1	Liste des CDD recrutés par des établissements publics dans le cadre du projet
Lister ici tous les CDD recrutés depuis le début du projet. Joindre un CV pour chaque nouveau CDD.

Numéro
du
Partenaire	Nom	Prénom	Qualifications	Date de recrutement	Durée du contrat (en mois)	Tâche du projet concernée	
01	Donze	Alexandre	Engineer	May 1, 2007	7 months	Simulation based validation methods	
01	Shalev	Noa	Engineer	May 31, 2007	4 months	Tool interface and integration	

							

							

							

5.2	Equipements (> 4000 €) achetés par les partenaires dans le cadre du projet
Lister ici tous les équipements achetés depuis le début du projet

Numéro
du
Partenaire	Désignation	Date d'achat	Prix d'achat
(en Euros)	Part financées par l'aide ANR
(en Euros)	

					

6	Annexe : Liste des délivrables joints au présent rapport (uniquement pour les rapports de fin d'année)
Les délivrables du projet sont fournis par le coordonnateur.

Numéro
du
délivrable	Désignation	Forme/Support