´ Equivalence entre propri´et´es Simulink et Crit`eres de Couverture de Test Manel TEKAYA1, 2 Mohamed Taha BENNANI Samir BEN AHMED 2 1 Universit´ e de Carthage Telnet Innovation Labs 2 Universit´ e de Tunis Elmanar 3 Universit´ e de Tunis Elmanar CAL 10-11 Juin 2014 - CNAM Paris 2 Contexte Telnet Innovation Labs : Activit´es, Recherches et d´eveloppement I I I I I I T´el´ecommunication Multim´edia Automobile Avionique Mon´etique Syst`eme d’Information TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 2 / 29 Contexte Telnet Innovation Labs : Activit´es, Recherches et d´eveloppement I I I I I I T´el´ecommunication Multim´edia Automobile Avionique Mon´etique Syst`eme d’Information TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 2 / 29 Contexte D´epartement Automobile et Avionique : Processus du Test Unitaire TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 3 / 29 Contexte D´epartement Automobile et Avionique : Processus du Test Unitaire TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 3 / 29 Contexte TELNET Innovation Labs : D´efi `a relever TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 4 / 29 Contexte Outils de g´en´eration des entr´ees de test `a partir des mod`eles Matlab/Simulink I SmartTestGen I REDIRECT I Embedded Tester from BTC I AutoMotGen I Diversity-TG I Reactis de ”Reactive Systems Inc” I I Simulink Design verifier Sal-ATG TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 5 / 29 Contexte Outils de g´en´eration des entr´ees de test `a partir des mod`eles Matlab/Simulink I SmartTestGen I REDIRECT I Embedded Tester from BTC I AutoMotGen I Diversity-TG I Reactis de ”Reactive Systems Inc” I I Simulink Design verifier Sal-ATG TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 5 / 29 Contexte Outils de g´en´eration des entr´ees de test `a partir des mod`eles Matlab/Simulink I SmartTestGen I REDIRECT I Embedded Tester from BTC I AutoMotGen I Diversity-TG I Reactis de ”Reactive Systems Inc” I I Simulink Design verifier Sal-ATG TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 5 / 29 Plan 1 Approche MB-ATG 2 Cas d’´ etude 3 D´ emonsatration de l’´equivalence 4 Conclusions et Travaux Futurs TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 6 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Exploitation de l’approche MB-ATG TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 7 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de l’approche MB-ATG TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 8 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de l’approche MB-ATG TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 8 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de l’approche MB-ATG I Les propri´et´es et les hypoth`eses sont exprim´ees en utilisant les op´erateurs Simulink (Biblioth`eque SLDV). TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 9 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de l’approche MB-ATG I I Les propri´et´es et les hypoth`eses sont exprim´ees en utilisant les op´erateurs Simulink (Biblioth`eque SLDV). La conception de la propri´et´e (respectivement hypoth`ese H) est appel´ee ”Proof Objective” (respectivement ”Assumption”) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 9 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de l’approche MB-ATG D´emarche de tissage TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 10 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de l’approche MB-ATG outil de tissage TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 11 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de l’approche MB-ATG Le model checker Prover Plug-in I ´ Prend en entr´ee: L’automate Etats/Transitions du mod`ele Matlab/Simulink + les propri´et´es contraintes par des hypoth`eses TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 12 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de l’approche MB-ATG Le model checker Prover Plug-in I I ´ Prend en entr´ee: L’automate Etats/Transitions du mod`ele Matlab/Simulink + les propri´et´es contraintes par des hypoth`eses G´en`ere un contre-exemple si et seulement si la propri´et´e est viol´ee et les hypoth`eses sont `a ”vrai” TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 12 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de l’approche MB-ATG Le model checker Prover Plug-in I I I ´ Prend en entr´ee: L’automate Etats/Transitions du mod`ele Matlab/Simulink + les propri´et´es contraintes par des hypoth`eses G´en`ere un contre-exemple si et seulement si la propri´et´e est viol´ee et les hypoth`eses sont `a ”vrai” Utilise une extension de la m´ethode Stalmarck TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 12 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Int´ erˆ et de coupler les propri´ et´ es et les hypoth` eses (MC/DC: Niveau ASILD- ISO 26262-6) Propri´et´es et hypoth`eses P1: NOT((A AND B) OR C) P2: (A AND B) OR C P3: NOT(A AND B) P4: (A AND B) P5: NOT(C) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 13 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Int´ erˆ et de coupler les propri´ et´ es et les hypoth` eses (MC/DC: Niveau ASILD- ISO 26262-6) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 13 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Int´ erˆ et de coupler les propri´ et´ es et les hypoth` eses (MC/DC: Niveau ASILD- ISO 26262-6) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 13 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Int´ erˆ et de coupler les propri´ et´ es et les hypoth` eses (MC/DC: Niveau ASILD- ISO 26262-6) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 13 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Int´ erˆ et de coupler les propri´ et´ es et les hypoth` eses (MC/DC: Niveau ASILD- ISO 26262-6) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 13 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Int´ erˆ et de coupler les propri´ et´ es et les hypoth` eses (MC/DC: Niveau ASILD- ISO 26262-6) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 13 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Int´ erˆ et de coupler les propri´ et´ es et les hypoth` eses (MC/DC: Niveau ASILD- ISO 26262-6) Les contre-exemples (0,1,1) (1,0,0) (0,0,0) (1,1,0) (1,0,1) Les cas de test(oracle) (0,1,1) (1,0,0) (0,1,0) (1,1,0) (1,0,1) • Pas de correspondance entre les contre-exemples et les entr´ees de test TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 13 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Int´ erˆ et de coupler les propri´ et´ es et les hypoth` eses (MC/DC: Niveau ASILD- ISO 26262-6) Propri´et´es et hypoth`eses P1: NOT((A AND B) OR C) P2: (A AND B) OR C P3: NOT(A AND B) P4: (A AND B) P5: NOT(C) H1: (A OR B) H2: (A ∧ B) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 14 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Tissage des propri´ et´ es et des hypoth` eses selon MC/DC (Niveau ASILD - ISO 26262-6) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 15 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Tissage des propri´ et´ es et des hypoth` eses selon MC/DC (Niveau ASILD - ISO 26262-6) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 15 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Tissage des propri´ et´ es et des hypoth` eses selon MC/DC (Niveau ASILD - ISO 26262-6) Propri´et´es Contre-exemples Entr´ees de Test P1: NOT((A ∧ B) OR C) (0,1,1) (0,1,1) P2: (A ∧ B) OR C (1,0,0) (1,0,0) P3: NOT(A ∧ B) (0,1,0) (0,1,0) P4: (A ∧ B) (1,1,0) (1,1,0) P5: ¬(C) (1,0,1) (1,0,1) • Correspondance entre les entr´ ees de test et les contre-exemples TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 15 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de G´ en´ eration des contre-exemples Propri´et´es et hypoth`eses P1: NOT((A AND B) OR C) P2: (A AND B) OR C P3: NOT(A AND B) P4: (A AND B) P5: NOT(C) H1: (A OR B) H2: (A ∧ B) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 16 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de G´ en´ eration des contre-exemples I Une relation d’´equivalence est construite `a partir des hypoth`eses. TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 17 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de G´ en´ eration des contre-exemples I I Une relation d’´equivalence est construite `a partir des hypoth`eses. Les formules propositionnelles pr´esentant les propri´et´es sont affect´ees `a la classe d’´equivalence ”Vraie” ( Hi ⇐⇒ Pj avec Hi =1) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 17 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de G´ en´ eration des contre-exemples I I I Une relation d’´equivalence est construite `a partir des hypoth`eses. Les formules propositionnelles pr´esentant les propri´et´es sont affect´ees `a la classe d’´equivalence ”Vraie” ( Hi ⇐⇒ Pj avec Hi =1) Application de l’algorithme de saturation Stalmarck `a la relation d’´equivalence TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 17 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de G´ en´ eration des contre-exemples • La propri´ et´e P1: NOT((A AND B) OR C) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 18 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de G´ en´ eration des contre-exemples • La propri´ et´e P1: NOT((A AND B) OR C) • Transformation en n´ egation: not (not(A =⇒ not B) =⇒ C) ´equivalent `a (¬ (A =⇒ not B) =⇒ C) =⇒ false) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 18 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de G´ en´ eration des contre-exemples • La propri´ et´e P1: NOT((A AND B) OR C) • Transformation en n´ egation: not (not(A =⇒ not B) =⇒ C) ´equivalent `a (¬ (A =⇒ not B) =⇒ C) =⇒ false) • La classe d’´ equivalence `a v´erifier: (H1∧H2 ⇐⇒ ( not (A =⇒ not B) =⇒ C) =⇒ false) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 18 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Principe de G´ en´ eration des contre-exemples • La propri´ et´e P1: NOT((A AND B) OR C) • Transformation en n´ egation: not (not(A =⇒ not B) =⇒ C) ´equivalent `a (¬ (A =⇒ not B) =⇒ C) =⇒ false) • La classe d’´ equivalence `a v´erifier: (H1∧H2 ⇐⇒ ( not (A =⇒ not B) =⇒ C) =⇒ false) • Application de l’algorithme de Stalmarck sur les ´ etats o`u H1∧H2 `a ”Vraie” TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 18 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 0 TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 19 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 0 • Classe d’´ equivalence ` ´elimimer ”Fausse” → A TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 19 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 1 (Classe d’´equivalence ”Vraie” ) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 20 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 1 (Classe d’´equivalence ”Vraie” ) • 1∧1 ⇐⇒ (¬(0 =⇒ ¬ 1) =⇒ 1) =⇒ 0) ce qui donne 0 =⇒ 0 (Pas de contradiction) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 20 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 1 (Classe d’´equivalence ”Vraie” ) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 21 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 1 (Classe d’´equivalence ”Vraie” ) • 1∧1 ⇐⇒ (¬(1 =⇒ ¬ 1) =⇒ 0) =⇒ 0) ce qui donne 0 =⇒ 0 (Pas de contradiction) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 21 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 1 (Classe d’´equivalence ”Vraie” ) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 22 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 1 (Classe d’´equivalence ”Vraie” ) • 1∧1 ⇐⇒ (¬(1 =⇒ ¬ 0) =⇒ 1) =⇒ 0) ce qui donne 0 =⇒ 0 (Pas de contradiction) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 22 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 1 (Classe d’´equivalence ”Vraie” ) • TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 23 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 1 (Classe d’´equivalence ”Vraie” ) • 1∧1 ⇐⇒ (¬(1 =⇒ ¬ 1) =⇒ 0) =⇒ 0) ce qui donne 0 =⇒ 0 (Pas de contradiction) TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 23 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence • H1∧H2 = 1 (Classe d’´equivalence ”Vraie” ) • 1∧1 ⇐⇒ (¬(0 =⇒ ¬ 1) =⇒ 1) =⇒ 0) ce qui donne 1 =⇒ 0 (Contradiction) • Le triplet terminal est (0,1,1) qui repr´esente le contre-exemple TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 24 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Preuve d’´ equivalence Propri´et´es Contre-exemples Entr´ees de Test P1: NOT((A ∧ B) OR C) (0,1,1) (0,1,1) P2: (A ∧ B) OR C (1,0,0) (1,0,0) P3: NOT(A ∧ B) (0,1,0) (0,1,0) P4: (A ∧ B) (1,1,0) (1,1,0) P5: ¬(C) (1,0,1) (1,0,1) • Correspondance entre les entr´ ees de test et les contre-exemples TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 25 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Conclusions I Proposition d’une approche contralis´ee de Test Unitaire MB-ATG TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 26 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Conclusions I I I Proposition d’une approche contralis´ee de Test Unitaire MB-ATG R´ealisation de la premi`ere ´etape de l’outillage de la norme ISO 26262-6 D´emonstration de l’´equivalence entre les contre-exemples et les entr´ees de test assurant le crit`ere de couverture MC/DC TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 26 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Travaux Futurs I G´en´eration des propri´et´es et des hypoth`eses TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 27 / 29 Approche MB-ATG Cas d’´ etude D´ emonsatration de l’´ equivalence Conclusions et Travaux Futurs Travaux Futurs I I G´en´eration des propri´et´es et des hypoth`eses Extension de l’approche MB-ATG aux mod`eles Matlab/Simulink analogiques. TEKAYA and al. P & H ⇐⇒ donn´ ees de test / CC CAL 10-11 Juin 2014 - CNAM Paris 27 / 29 Merci pour votre attention Questions?
© Copyright 2024 ExpyDoc
