Tests du circuit trigger

1. Circuit trigger

Cet exemple est tiré de l'article [CBRP96]. Le graphe STG qui décrit la spécification du contrôleur trigger et le graphe d'états sont donnés dans la figure 1.

2. Analyse instanciée

2.1. Descriptions d'entrée sortie

• Dans le tableau présenté ci-dessous, nous présentons l'ensemble des descriptions d'entrée sortie de l'outil VHDL2TA employées dans les tests effectués sur le circuit trigger. Les détails des tests sont donnés dans exp-trigger.
  
  

  Tests	VHDL	Délais	Env	HyTech	IMITATOR-2	UPPAAL	Propriétés TCTL
  test 1	trigger.vhd	trigger.temp	trigger.env	trigger.hy	trigger.imi	trigger.ta	trigger.q
  test 2	"	"	trigger.env	trigger.hy	trigger.imi	trigger.ta	trigger.q

  
  

• A titre d'exemple, les descriptions en UPPAAL, en HyTech et en IMITATOR-2 du premier test sont générées en utilisant, respectivement, les commandes présentées ci-dessous :

  • vhdl2ta trigger.vhd -e env1.env -t delay.temp 2 -m ta -o trigger.ta -taf upl

  • vhdl2ta trigger.vhd -e env1.env -t delay.temp 2 -m ta -o trigger.hy -taf hy

  • vhdl2ta trigger.vhd -e env1.env -t delay.temp 2 -m ta -o trigger.imi -taf imi2

2.2. Résultats d'analyse

• Le tableau mentionné ci-dessous récapitule pour chaque test :

  • les résultats de model-checking des propriétés TCTL sur le modèle généré décrit en UPPAAL, en utilisant le model-checker d'UPPAAL.

  • l'analyse d'accessibilité en utilisant l'outil d'analyse HyTech sur le modèle décrit dans le langage de description de cet outil.

  • l'analyse d'accessibilité en utilisant l'outil de synthèse paramétrée IMITATOR-2 sur le modèle décrit dans le langage de description de cet outil, ainsi le format graphique du graphe d'atteignabilité (graphe de régions) produit par IMITATOR-2.

  
  

  Tests	Model-checking TCTL	analyse avec HyTech	analyse avec IMITATOR-2	graphe accessibilité
  test 1	MC-TCTL-1	RA-HY-1	RA-IMI2-1	Graphe-Region-1
  test 2	MC-TCTL-2	RA-HY-2	RA-IMI2-2	Graphe-Region-2

  
  

• Les analyses avec UPPAAL, HyTech et IMITATOR-2 dans ces tests ont été effectués en utilisant, respectivement, les commandes présentées ci-dessous :

  • verifyta trigger.ta query.q

  • hytech trigger.hy

  • IMITATOR trigger.imi -mode reachability

Références