Tests du circuit SR-latch1 (avec nor)

1. Circuit SR-latch1 (avec nor)

La spécification du circuit sr-latch (avec nor) et son implémentation en portes logiques sont données ci-dessous. On note que les figures sont tirées de wikipédia [Wiki].

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 SR-latch1. Les détails des tests sont donnés dans exp-SR-latch1.
  
  

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

  
  

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

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

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

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

2.2. Résultats d'analyse

• Le tableau mentionné ci-dessous récapitule :

  • 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

  
  

• L'analyse avec HyTech et l'analyse avec IMITATOR-2 dans ce test ont été effectués en utilisant, respectivement, les commandes présentées ci-dessous :

  • verifyta sr_latch.ta query.q

  • hytech sr_latch.hy

  • IMITATOR sr_latch.imi -mode reachability

Références