1
INTRODUCTION
Les méthodes formelles sont en plein essor notamment dans les applications critiques telles les centrales nucléaires, l'avionique ou le transport ferroviaire ([6] et [3]). Le défi posé par les applications critiques consiste à établir un niveau maximal de sûreté dans le fonctionnement de l'application. L'apport fondamental des méthodes formelles est d'offrir un cadre mathématique au processus de développement, ce qui permet de disposer d'une méthode permettant la production de logiciels corrects par construction grâce à un processus de développement vérifiable par des techniques de validation telles que la preuve ou l'exploration de modèle (model-checking). Pour cela, il faut évidemment décrire de façon précise les propriétés que le système informatique doit respecter.
L'idée de cette étude est de réaliser un lien entre la méthode formelle B et le langage de description VHDL. La première spécification formelle en B permettant d'exprimer les propriétés essentielles du circuit à réaliser, cette spécification est ensuite décomposée en sous spécifications, le raffinement est alors un moyen pour répartir les propriétés essentielles sur un nouvel ensemble de composants. Le processus est répété jusqu'à un niveau suffisamment concret de description physique permettant de générer une description VHDL afin de réaliser le circuit ou de permettre de s'intégrer à un autre processus de développement "métier". Ce processus basé sur un raffinement formalisé permet de démontrer qu'une synthése (au sens VHDL) est bien une réalisation de la spécification fonctionnelle et abstraite initiale.
Dans notre cas, les propriétés essentielles visées sont des propriétés de sécurité (safety properties) mais il est possible de prendre en compte différents types de propriétés (bon-fonctionnement) dès lors qu'elles s'expriment dans les termes du modèle élaboré.
La faisabilité de la modélisation de circuit numérique simples en B a déjà été explorée voir [4]. Dans [5], nous présentons les bases de la méthodologie permettant de plonger un modèle VHDL au sein de la méthode B. Ce plongement est réalisé au travers de la mise en place d'un ensemble de "machines abstraites" B qui permet de disposer des concepts introduits au sein de la bibliothèque IEEE STD_LOGIC_1164. Les circuits numériques que nous étudions sont des circuits numériques dit synchronisés. Nous supposons donc qu'une horloge extérieure se charge d'activer le circuit.
Après avoir poser le contexte de notre étude, dans une seconde partie nous présenterons la méthode B, le langage VHDL et l'intérêt du couplage B/VHDL. Le couplage entre B et VHDL sera décrit dans la troisième partie ainsi que la méthodologie utilisée. Cet article se termine par un exemple de conception sûre de composant numérique basée sur la notion de propriété.
2 CONTEXTE
2.1 VHDL (Very Speed Integrated Circuit Hardware Description Language)
Le langage VHDL ([2]) permet de décrire rigoureusement le comportement d'un circuit numérique. VHDL est un langage normalisé depuis 1987, créé spécifiquement pour[1] la conception matérielle et la description de systèmes électroniques logiques et analogiques. Il permet une description comportementale des fonctions d'un circuit (voir Figure 1.), laissant le soin au synthétiseur de générer les structures électroniques qui réaliseront matériellement ces fonctions. Il a pour avantage de pouvoir être simulé en vue d'une validation fonctionnelle de la description, puis d'être synthétisé en vue de sa réalisation sous forme d'Asic ou de composants programmables
Figure 1. un exemple de composant numérique.
Ce langage peut servir également a décrire des systèmes matériels à l'aide d'un haut niveau d'abstraction, il s'applique aux cartes de composants mais également à des systèmes entiers comprenant à la fois des parties matérielles et logicielles. Il permet enfin de décrire des algorithmes destinés à être implanté de manière physique. VHDL propose à la fois des instructions d'un langage de programmation comme les boucles, mais également des termes descriptifs de bas-niveau tels que par exemple 'wait' (qui spécifie le retard d'un signal) en réponse aux besoins de conceptions de circuits digitaux complexes avec des contraintes temporelles fortes.
LIBRARY ieee;
USE ieee.std_logic_1164.all;
USE ieee.std_logic_arith.all;
ENTITY
SPEC IS
PORT
( --
déclaration des entrées/sorties physiques
a, b, c : IN
STD_LOGIC ;
s1, s2 : OUT
STD_LOGIC
) ;
END SPEC ;
ARCHITECTURE IMP OF SPEC
IS -- description de
l'application
BEGIN
s1
<= a AND b ;
s2
<= (NOT a) OR (a AND b AND c) ;
END
IMP ;
Figure 2. Un exemple de circuit VHDL
Tout circuit peut être divisé en blocs possédant des entrées, des sorties et réalisant une fonction bien définie. Chaque bloc peut alors être vu comme une boîte noire. C'est la première étape dans la rédaction du code. Chaque bloc est déclaré au travers d'une entitée (ENTITY). A chaque bloc correspond la description de son comportement. C'est dans cette étape que les avantages de VHDL sont les plus notables. L'association d'une fonction à un bloc se fait en définissant une architecture (ARCHITECTURE).
De multiples approches ont été utilisées pour tenter de formaliser et vérifier les descriptions VHDL. F. Nicoli a utilisé ([12]) a proposé une méthode de preuve au moyen d'un démonstrateur automatique (Boyer-Moore) adapté pour traiter un sous ensemble de du langage VHDL.
Fuchs et Mendler ([13]) ont présenté une sémantique fonctionnelle de haut niveau. Les signaux dans cette approche sont représentés par des fluxs (streams) qui sont des historiques des valeurs prises par les signaux au cours des cycles successifs.
Read et Edwards ([14]) présentent une sémantique fonctionnelle exécutable d'un sous ensemble de VHDL appelé VHDL- expriméé également dans la logique de Boyer-Moore.
Van Tassel ([15]) utilise l'assistant de preuve HOL pour implanter la sémantique opérationelle d'un sous ensemble de VHDL, Femto-VHDL. Dans cette approche, on traite les signaux booléens, l'instruction if, la séquence d'instructions et l'affectation de signal, et une instruction concurrente pour traiter un processus avec une liste de sensibilité explicite.
VHDL est donc le plus important standard pour concevoir les circuits électroniques, il contient des bibliothèques riches qui permettent à l'utilisateur de se baser sur des composants électroniques très variés. Afin de créer son module, le programmeur peut profiter de bibliothèques standardisées qui font partie du noyau de VHDL ou de ses propres bibliothèques. Un objectif de notre projet est de fournir le support des biblotèques standards au sein de l'environnement B. Comme exemple, nous avons choisi de modéliser le paquetage standard STD_LOGIC_1164 qui est un de plus célèbre paquetage de VHDL.
VHDL est un langage puissant permettant l'écriture succincte de code
décrivant des ciircuits logiques complexes. Il offre en plus la possibilité de
créer des bibliothèques de composants réutilisables d'un projet à l'autre. Il
permet aussi le design modulaire d'une application. On peut créer des composants
qui seront eux-mêmes utilisés dans un composant plus complexe. L'utilité est
grande car le code de chaque composant peut être validé par simulation; la
recherche des erreurs dans un composant complexe est donc simplifiée. Il permet
de créer une fonction sans se préoccuper du composant dans laquelle elle sera
implémentée. Il ne faut donc pas devenir intimement familier avec
l'architecture d'un circuit particulier pour optimiser l'utilisation des
ressources et les performances. VHDL permet de simuler le comportement d'un
circuits. De part le caractère standard du langage, cette simulation peut être
effectuée au moyen de n'importe quel simulateur. Le circuit peut être programmé
par n'importe quel outils de synthèse et ce sur n'importe quel type d'ordinateur.
2.2 La méthode B
La méthode B ([1]) a été développée par Jean-Raymond Abrial, c'est une méthode formelle orientée modèle comme Z ([9]) et VDM ([7]) mais qui permet un développement incrémental de la spécification jusqu'au code, au travers de la notion de raffinement [8], et ceci dans un formalisme unique, le langage des machines abstraites. À chaque étape du développement B des obligations de preuves sont générées afin de garantir la validité du raffinement et la consistance de la machine abstraite. À partir du dernier raffinement (implémentation), le niveau de modélisation est suffisamment concret pour permettre l'utilisation d'un générateur automatique de code compilable (C, ADA et autre). Le (sous) langage B disponible au niveau implantation est appelé B0. Les restrictions syntaxiques et sémantiques portées sur le B0 permettent une construction directe du traducteur.
MACHINE B_ADD_COMPLET_1bit_0
ABSTRACT_CONSTANTS bin_to_dec
PROPERTIES
bin_to_dec : BOOL --> 0..1
&
bin_to_dec
= {(TRUE |-> 1), (FALSE|-> 0)}
DEFINITIONS
BV(xx)
== bin_to_dec(xx)
; Compute_(inA,
inB, Cin, Sum, Cout) == 2*BV(Cout) + BV(Sum) = BV(inA) + BV(inB) + BV(Cin)
CONCRETE_VARIABLES AA,BB,CIN,COUT,SS
INVARIANT
AA,BB,CIN
:
BOOL * BOOL*BOOL
& SS,COUT
:
BOOL * BOOL
& Compute_(AA,BB,CIN,SS,
COUT)
INITIALISATION
AA, BB, CIN, COUT, SS :( AA,BB,CIN
: BOOL * BOOL*BOOL & SS,COUT :
BOOL * BOOL
& Compute_(AA,BB,CIN,SS,
COUT)
)
OPERATIONS
in_AA(yy) =
PRE
yy
: BOOL
THEN
AA,
COUT, SS :( AA,COUT,SS : BOOL * BOOL * BOOL&AA = yy & Compute_(yy,BB,CIN,SS, COUT))
END;
in_BB(yy) =
PRE
yy
: BOOL
THEN
BB,
COUT, SS :(BB,COUT,SS : BOOL * BOOL * BOOL& BB = yy & Compute_(AA,BB,CIN,SS, COUT))
END;
in_CIN(yy) =
PRE
yy
: BOOL
THEN
CIN,
COUT, SS :( CIN,COUT,SS : BOOL*
BOOL* BOOL & CIN = yy &
Compute_(AA,BB,CIN,SS, COUT))
END;
xx <-- out_COUT = xx := COUT;
xx <-- out_SS = xx := SS;
END
Figure 3. La spécification d'un additionneur.
Les machines abstraites sont composées de trois parties: la partie déclarative, la partie de composition et la partie exécutive.
La partie déclarative permet de décrire l'état d'une machine abstraite au travers de variables, de constantes, d'ensembles, et surtout de propriétés que doit toujours vérifier l'état de la machine. Cette partie est basée sur la théorie des ensembles et les prédicats du premier ordre. Nous pouvons dès lors parler de "modèle" à état. Dans l'exemple suivant, la partie déclarative proposée est composée de la description d'une constante abstraite[2] et de 5 variables concrétes.
Les clauses de composition (SEES, INCLUDES, IMPORTS et EXTENDS) permettent de décrire les différents liens entre machines abstraites, chaque clause introduisant des règles de visibilité et d'accessibilité sur l'état et les opérations de la machine abstraite concernées.
La partie exécutive, quand à elle, contient l'initialisation et les opérations de la machine abstraite, elle est basée sur le langage des substitutions généralisées (dit GSL). La machine abstraîte introduite par la figure 3. décrit 5 opérations.
Les substitutions généralisées sont une extension du travail de Dijkstra [11] sur les substitutions. Les substitutions généralisées sont des transformateurs de prédicat, [S]P désigne le prédicat obtenu en appliquant la substitution S sur le prédicat P.
La méthode B est une méthode basée sur l'encapsulation, aisni les opérations doivent elles fournir l'ensemble des actions permettant de faire évoluer l'état de la machine concernée.
Outre sa relative simplicité sur la plan théorique, la force de la méthode B réside également dans la disponibilité d'ateliers logiciels qui prennent en compte chaque phase du développement B. Les ateliers commerciaux sont au nombre de deux, l'atelier B de la société ClearSy[3] et le BtoolKit de la société BCORE[4].
2.3 Intérêt du couplage B/VHDL
Les sections précédentes ont permis de montrer que l'on dispose de deux environnements différents mais complémentaires. En effet, la validation de composant VHDL est basée sur la notion de simulation ou de model-checking alors que pour la méthode B elle est basée sur la notion de preuve. Dans les deux cas, on cherche à montrer qu'un composant vérifie une (des) propriété(s). La force de la méthode B réside dans l'expression formelle de ces propriétés et par la génération automatique des obligations de preuves associées. VHDL reste le langage d'expression de circuit et dispose d'outils efficaces et reconnus.
La modélisation de chaque circuit numérique se fera au travers d'une machine abstraîte B qui introduira une opération permettant de faire évoluer chaque entrée et une opération permettant de récupérer la sortie du composant.
Les circuits numériques que nous étudions sont dit synchronisés, ce choix est du aux caractéristiques actuelles de la méthode B, qui reste une méthode pour développer des logiciels cycliques ininterruptibles.
La suite est consacrée à la mise en évidence des principes constitutifs de la méthodologie de modélisation des circuits numériques. Nous donnons les éléments permettant de construire la modélisation d'un nouveau circuit, indépendamment des exemples présentés et sans connaissance a priori des caractéristiques du circuit à modéliser. La faisabilité de ce processus à été démontré au travers de la réalisation d'exemples simples, pour plus d'information se rapporter à [4].
3 COUPLAGE B/VHDL
3.1 Méthodologie
Avant d'aborder les aspects techniques de la méthodologie utilisée, nous pouvons tout d'abord mettre en évidence Avant d'aborder les aspects techniques de la méthodologie utilisée, nous pouvons tout d'abord mettre en évidence l'analogie étroite au niveau méthodologique entre l'emploi de la méthode B et la spécification et synthèse de circuits numériques.
Cette analogie est résumée dans le tableau suivant :
|
Synthèse de
circuits |
Méthode B |
|
Spécification fonctionnelle |
Machine abstraite |
|
Comportement |
Raffinements |
|
Validation <<fonctionnel vs. matériel>> |
Preuve |
|
Description physique |
Machine d'implémentation |
|
|
|
|
Port |
Variable globale |
|
Connexion |
Invariant de collage entre variables |
|
Propagation du signal |
Appel d'opération (transmission de valeurs) |
|
Réutilisation |
Importation + Renommage |
|
|
|
|
<<Bottom up>> |
Les circuits intégrés à partir des portes logiques |
|
<<Top-down>> |
Les portes logiques intégrées à partir des transistors |
Figure 4. Lien entre la synthèse de circuit et B
La première partie du tableau exprime que la première étape de modélisation fonctionnelle du circuit numérique est réalisée en B par une spécification abstraite utilisant une ou plusieurs équations logiques définissant la fonction attendue du circuit modélisé.
L'étape de raffinement peut être l'occasion de proposer une modélisation du comportement attendu par une autre technique plus concrête telle que les tables de vérités.
La figure suivante propose une implémentation pour une porte OU utilisant une table de vérité (à la palce d'une évaluation booléenne directe) pour calculer la valeur de sortie. La table de vérité est ici représentée par un objet mathématique bien connu à savoir une relation. Nous pouvons remarquer que le modèle obtenu est plus concis.
IMPLEMENTATION
B_Or_3_n
REFINES
B_Or_3_0
INITIALISATION
in1 := TRUE
; in2 := TRUE
; out := { ((TRUE
,TRUE ) |-> TRUE )
, ((FALSE,TRUE
) |-> TRUE )
, ((FALSE,FALSE)
|-> FALSE)
, ((TRUE
,FALSE) |-> TRUE )
}
OPERATIONS
In_1 ( val ) = in1 := val;
In_2 ( val ) = in2 := val;
val <-- Out = val :=
out(in1,in2);
END
Figure 5. Exemple de définition de circuit basée sur une table de vérité
Sans explorer plus avant cette technique, notons simplement que celle-ci peut être avantageusement utilisée lors d'une éventuelle phase de test, la table de vérité constituant l'oracle. Toutefois, cette technique souffre de deux limitations : d'une part, elle devrait être limitée aux circuits de petite taille et d'autre part une structure réalisant une table de vérité risque de se révéler inadaptée à la phase de preuve. Enfin, l'implémentation B basée sur l'importation de modèles de bases permet de donner une synthèse matérielle du circuit spécifié jusqu'ici. Cette synthèse s'exprime par l'utilisation des circuits de bases disponibles. La preuve de cette implémentation doit ainsi permettre d'établir que la réalisation physique choisie (aspect matériel) réalise effectivement la fonction logique attendue (aspect fonctionnel). C'est cette phase essentielle de preuve qui n'est actuellement pas intégrée "naturellement" aux technologies du domaine.La seconde partie du tableau décrit le prolongement de cette méthodologie générale vers les structures de spécifications utilisées, c'est la méthodologie <<effective>>.
En résumé, tout circuit combinatoire (élémentaire ou complexe) peut être tout d'abord décrit par un modèle fonctionnel logique.
Ce modèle est constitué par :
• un certain nombre d'entrées que nous noterons in_i (i variera en fonction des besoins),
• d'un certain nombre de sorties que nous noterons out_i (i variera en fonction des besoins),
• un comportement observable qui se traduit par un jeu d'équations logiques sur les entrées et les sorties. Dans le cas particulier d'une unique sortie, nous avons une fonction logique donnant la valeur de sortie en fonction des seules entrées.
Les opérations fournies respectent les <<modes>> in ou out des ports ainsi modélisés. Ces modes déterminent des variables uniquement accessibles en lecture (in) ou en écriture (out). La modélisation de circuits combinatoires ne nécessite pas la mise en oeuvre d'un mode mixte in-out correspondant à une variable accessible en lecture/écriture[5]. Enfin, la <<fonction>> réalisée par le circuit est déterminée par des contraintes posées sur les valeurs en entrée et en sortie. L'équation logique correspondante est placée dans une définition dénommée compute_. Cette technique permet de disposer d'une <<opération locale>>, notion[6] absente du langage B. Cette notion d'opération locale est ici fondamentale car elle permet de réaliser les calculs nécessaires (fonction du circuit) dès qu'une entrée est modifiée. Elle permet donc de contourner l'interdiction faite en B qui ne permet pas d'appeler une opération opB dans une opération opA lorsque opA et opB appartiennent au même composant. Toutefois, ce contournement est d'ordre syntaxique et non sémantique car il est en fait constitué par une expansion lexicale de la définition (inlining).
Une fois le circuit numérique spécifié au travers d'une machine abstraite, il nous reste à réaliser une ou plusieurs étapes de raffinement afin d'obtenir une architecture du circuit réalisable par des composants (modèles) de base. Ce processus de raffinement est équivalent au processus de synthèse. Chaque étape de raffinement permet de préciser le comportement du circuit et de démontrer que chaque propriété essentielle st prise en compte et respecté par la nouvelle architecture.
La machine abstraite B_ADD_COMPLET_1bit_0 peut être raffinée simplement en passant de l'expression logique à une expression booléenne et en introduisant la description classique d'un additionneur. Le raffinement B_ADD_COMPLET_1bit_1 est décrit dans la figure 6. Cette description est donnée au travers de l'introduction des équations booléennes au sein de la clause DEFINITION. Le corps des opérations n'évolue pas par rapport à la spécification.
REFINEMENT B_ADD_1bit_Complet_1
REFINES B_ADD_1bit_Complet_0
DEFINITIONS
Val_(xx) == (xx
= TRUE)
; Somme_(inA,
inB, Cin, Sum) ==
(Sum = bool(
((not(Val_(inA)))&
((not(Val_(inB)) & (Val_(Cin)) or ((Val_(inB)) &
(not(Val_(Cin))))))
or (( Val_(inA)) & ((not(Val_(inB))
& not(Val_(Cin))) or ((Val_(inB)) & (Val_(Cin)))))
)
)
; Retenue_(inA,
inB, Cin, Cout) ==
( Cout = bool( ( (Val_(inA)) &
not(Val_(inB)) & Val_(Cin)) or
(not(Val_(inA))
&
(Val_(inB)) & Val_(Cin)) or
( (Val_(inA))
&
(Val_(inB))
)
)
)
; Compute_(inA,
inB, Cin, Sum, Cout) ==
( Somme_ (inA, inB, Cin, Sum)
& Retenue_(inA,
inB, Cin, Cout)
)
NVARIANT
AA,BB,CIN
:
BOOL * BOOL*BOOL
& SS,COUT
:
BOOL * BOOL
& Compute_(AA,BB,CIN,SS,
COUT)
...
END
Figure 6. Une description booléenne de l'addtionneur 1bit
De la même manière, l'implantation de l'additionneur est classiquement réalisée par composition de circuits de plus bas niveau, dans notre cas se sont des demi-additionneurs et un composant logique OR. Les composants de base sont instanciés au sein de la clause IMPORTS, les connections entre composant sont ralisées au sein de la clause INVARIANT. Le code à la forme suivante:
IMPLEMENTATION
B_ADD_1bit_Complet_n
REFINES
B_ADD_1bit_Complet_0
IMPORTS
add1.B_ADD_1bit_Demi_0
, add2.B_ADD_1bit_Demi_0
, OU1.B_Or_0
SEES
IEEE.B_STD_LOGIC_1164_0
, B_STD_ENTRIE
INVARIANT
AA
= add1.AA
& BB
= add1.BB
& add1.SS
= add2.AA
& CIN
= add2.BB
& add1.COUT = OU1.in1
& add2.COUT = OU1.in2
& COUT
= OU1.out
& SS
= add2.SS
INITIALISATION
....
END
Figure 7. Implantation de l'additionneur
3.2 La bibliothèque STD_LOGIC_1164
La bibliothèque STD_LOGIC_1164 est normalisée par l'IEEE. Elle sert à décrire les types de données intermédiaires. Ce paquetage est destiné à faciliter la portabilité des codes synthétisés.
Cette bibliothèque (ou paquetage) introduit plusieurs types de base, dont le type STD_ULOGIC qui est un typelogique à neuf valeurs et non seulement deux, comme le montre le tableau suivant. Les opérations logiques (AND, NOT, OR, ...) ont été redéfinies sur ces types, elles sont complétées par deux types de fonctions complémentaires, des opérations de conversion d'un type vers un autre type et deux fonctions pour déterminer les fronts montant (rising_edge ) ou descendant (falling_edge) d'un signal.
|
Notation VHDL |
Description |
Notation B |
|
U |
une valeur non initialisée |
UU |
|
X |
état inconnu |
XX |
|
0 |
0 fort |
OO |
|
1 |
1 fort |
II |
|
Z |
haute impédance |
ZZ |
|
W |
Inconnu faible |
WW |
|
L |
0 faible |
LL |
|
H |
1 faible |
HH |
|
D |
dont care |
DD |
Figure 8. Implantation du type STD_ULOGIC
La bibliothèque std_logic_1164 est spécifiée en B au travers de trois
machines abstraites. Nous avons décrit l'ensemble du développement dans [5].
B_STD_LOGIC_1164_0:
Dans cette machine un type principal qui contient les neuf valeurs est défini. Un "ensemble" est utilisée pour représenter ce type. Ensuite les sous-types sont définis en utilisant des sous-ensembles de l'ensemble précédent. Pour définir un sous-ensemble, la clause CONSTANTS (ou ABSTRACT_CONSTANTS) est utilisée pour introduire le nom et la clause PROPERTIES pour définir ses éléments. Cette méthode de déclaration diminue le nombre nécessaire de preuves parce que les définitions au-dessous de la clause PROPERTIES sont considérées comme des axiomes. les opérations logiques de la bibliothèque VHDL std_logic_1164 sont définies en utilisant des tableaux. Nous avons redéfini ces tableaux comme des fonctions mathématiques au sein de la clause PROPERTIES. L'opération logique est définie sous la clause OPERATIONS sur la base de l'utilisation des fonctions.
Au contraire de VHDL, la méthode B n'accepte pas le surchargement ("overloading", différentes opérations avec le même nom et avec différentes signatures). Dans ces cas nous avons ajouté le type de variable de la signature comme une partie du nom de l'opération. Par exemple, en VHDL six fonctions de signatures différentes sont appellées TO_X01. Dans cette machine seules deux opérations sont appellées From_BIT_to_X01 et From_std_ulogic_to_X01. Les quatre autres opérations/ fonctions sont définies dans la machine suivante.
B_STD_LOGIC_1164_Vector_0 :
Cette machine contient la définition de vecteurs[7] ("vectors", voir figure 10.) ainsi que les opérations correspondantes.
TYPE
std_ulogic_vector IS ARRAY ( NATURAL RANGE <> ) OF std_ulogic;
Figure 9. Un type VHDL utilisant les vecteurs.
En profitant de la clause SEES, toutes les constantes de la machine abstraite B_STD_LOGIC_1164_0 peuvent être vues par cette machine. Par conséquent, celle-ci peut accéder à toutes les tables qui définissent les opérations logiques. Pour généraliser ces fonctions, nous définissons une opération locale nommée Apply qui a quatre paramètres. Elle applique l'opération op sur tous les éléments des vecteurs in1 et in2 il compose les éléments du résultat dans le vector out. Le vecteur est défini comme une structure[8] composée de deux parties. La première est une fonction d'entier qui attache chaque indice d'un élément avec sa valeur. La deuxième est la taille du vecteur.
ABSTRACT_CONSTANTS
STD_LOGIC_VECTOR, STD_ULOGIC_VECTOR
,Max_Element
PROPERTIES
Max_Element:NAT1
& STD_LOGIC_VECTOR =
struct ( vector:
1..Max_Element-->STD_LOGIC, vector_size:NAT1 )
&
card(STD_LOGIC_VECTOR)<MAX_VECTOR
&
!xx.((xx:STD_LOGIC_VECTOR) => xx'vector_size<Max_Element)
Figure 10. Notre codage des vecteurs.
B_Signal_0 :
Afin de représenter un signal (voir figure 11.) cette machine utilise le concept de liste chainée[9]. Cette liste contient des éléments de type std_logic_1164.
La machine B_Signal_0 sert essentiellement dans le paquetage std_logic_1164 pour représenter les fonctions rising_edge et falling_edge.
ABSTRACT_CONSTANTS
SIGNAL_ULOGIC , SIGNAL_nil ,
F_SIGNAL
PROPERTIES
SIGNAL_ULOGIC
= struct ( value : STD_ULOGIC,next
: SIGNAL_ULOGIC)
& card(SIGNAL) <
MAX_SIGNAL
& SIGNAL_nil : SIGNAL_ULOGIC
& F_SIGNAL :
SIGNAL_ULOGIC --> SIGNAL\_ULOGIC
& F_SIGNAL(SIGNAL_nil)=
rec(value :DD, next:SIGNAL_nil)
Figure 11. La definition des signaux
La figure 12. présente les liens entre les composants de la bibliothèque.
B_STD_LOGIC_1164_0 B_STD_LOGIC_1164_0
Figure 12. Architecture des machines abstraîtes
4
DISCUSSION et
PERSPECTIVES
L'étude présentée ici est une application originale de la méthode B, méthode de spécification formelle de logiciel, au domaine de la spécification et description de circuits numériques.L'idée de cette étude est née de la mise en évidence d'une analogie étroite entre le processus B de développement par raffinements successifs et la synthèse de circuit numérique. L'originalité de l'approche proposée réside par son expression fondée sur l'utilisation systématique de cette analogie. En ce sens, bien qu'actuellement limitée par son caractère expérimental et non exhaustif en terme de modèles disponibles, cette approche propose les bases pour une réelle méthodologie c'est à dire une démarche quasi systématique pour traiter un problème de modélisation. De plus, en dépit des limitations décrites plus en détail dans la suite de cette discussion, l'intérêt mais également la difficulté de l'étude réside dans son positionnement à terme, entre le logiciel et le matériel.
Récemment, une étude analogue (actuellement non publiée [16]) propose une autre approche reliant la méthode B et le domaine de la conception de circuits électroniques. La démarche proposée par Jean-Raymond Abrial repose sur l'utilisation du B dit "évènementiel" ([17] et [18]).
De manière simplifiée, le B évènementiel est une évolution sémantique du B "usuel" dont la modification la plus sensible est le remplacement de la notion d'opération, action invoquée de l'extèrieur et de manière déterministe, par celle d'évènement, modification de l'état observable du système survenant de manière non-déterministe.
Bien que proposant une souplesse supplémentaire de modélisation notamment pas rapport à la spécification des successions d'états, il nous semble que l'approche utilisée bien que se basant sur une facilité technique de modélisation souffre d'un déficit d'adéquation méthodologique. En effet, nous pensons que la réussite de l'utilisation de la méthode B dans ce domaine particulier constitué par les techniques éprouvées de description et d'implantation de circuits, ne sera obtenue que par une adéquation forte avec la démarche "métier" pré-existante. En l'occurence, il ne s'agit pas de se substituer aux technologies déjà en place mais surtout d'apporter une aide complémentaire qui non seulement s'intègre dans une démacrhe de conception mais préserve une transition possible vers les standards utilisés (VHDL par exemple) et donc vers un processus non-nécessairement formel.
En ce sens, la validation de l'approche évènementielle devra répondre aux questions suivantes :
1. La modélisation évènementielle considère le système modélisé comme un tout "indivisible" et ne propose donc plus de mécanisme explicite de modularité. Or la conception matérielle est fondée sur la décomposition en systèmes physiques et la réutilisation de modèles/bibliothèques prédéfinis
2. La modélisation évènementielle ne traite que l'aspect modélisation et n'aborde pas actuellement les aspects implantation ou génération de modèles ou descriptions standards. Elle ne propose donc pas de continuité vers les technologies en place. Toutefois, il reste envisageable que cette approche soit utilisée en première modélisation abstraite, puis poursuivie, comme nous le proposons, par une approche plus classique vers les étapes d'implantation.
À l'heure actuelle, ces deux approches partagent néanmoins quelques défauts qu'il sera nécessaire de surmonter pour sortir du stade purement expérimental. Les perspectives essentielles de notre travail sont donc évidemment constituées par l'exploration des voies permettant sinon d'éliminer au moins d'atténuer ces limites .
o Traitement des aspects temporels
Actuellement, notre approche se place dans un cadre où le comportement temporel des circuits est idéalisé, ceci se traduisant par un délai nul de transition et de propagation des valeurs. Cette hypothèse de travail est évidemment sans rapport avec la réalité physique. Sur ce point, notre approche hérite d'une certaine lourdeur que n'a pas l'approche évènementielle en raison de la spécification explicite des transmissions de valeurs entre les ports. Toutefois, ce problème doit être modulé par
a) le fait que notre approche permet une automatisation (non réalisée actuellement) de la génération des modèles formels. Cette génération pouvant être assister par une interface graphique. Une étude de réutilisation d'outils graphiques pour la description de circuits numériques est en cours.
b) le fait que la formalisation des problèmes d'ordre temporel soit un sujet encore largement à l'étude. Il convient donc d'être prudent et de restreindre la portée de notre étude aux seules propriétés formalisables de manière satisfaisante dans le cadre que nous proposons. Ainsi, les propriétés relevant des préoccupations du temps réel sont ici difficilement abordables. Cette restriction nous semble devoir s'appliquer également à l'approche évènementielle car celle-ci ne fournit pas de traitement explicite et quantitatif du temps.
Seule une extension spécifique, orientée temps-réel, du formalisme B peut permettre d'envisager l'extension des modèles actuels pour intégrer ce type de préoccupations.
o Passage à l'échelle
Il est évident que la taille volontairement réduite des exemples fournis ne permet pas de conclure sur l'adéquation de notre approche indépendammant de la taille du circuit traité.
D'une part, nous devons insister ici sur le fait que l'objectif de l'approche proposé n'est pas de nécessairement de traiter l'intégralité de la modélisation et de la conception d'un circuit complexe mais, plus rationnellement, d'apporter une aide formelle et ponctuelle notamment dans le cadre de circuits ayant une spécification s'exprimant en terme de sûreté de fonctionnement, circuits dont la taille est généralement modeste ([19]).
Si la cible de notre approche n'est pas constituée par le domaine des technologies dites VLSI (très large
échelle d'intégration), en revanche elle est destinée à s'adapter à la frontière logiciel/matériel dans le contexte des applications dites critiques où les propriétés à respecter couvrent un large spectre difficile à maîtriser sans toutefois que le circuit concerné soient très complexe.
D'autre part, à l'inverse de l'approche évènementielle, notre approche devrait pouvoir subir une automatisation raisonnable, restreignant l'intervention de l'opérateur à l'expression des propriétés abstraites, à la proposition graphique des différentes architectures des raffinements du modèle étudié. Pour le type de circuit étudié jusqu'ici la phase de preuve est alors automatique. Pour des types de circuits plus sophistiqué (logique séquentielle), des résultats comparables sont prévisibles sous réserve de disposer du démonstrateur adapté en conséquence.
En conclusion, les travaux présentés ici doivent être étendus selon deux axes prioritaires si nous faisons abstraction de l'outillage proprement dit de la méthode proposée.
D'une part, la finalisation méthodologique de la génération de modèles VHDL à partir des spécifications formelles B au niveau implémentation sur la base des librairies prédéfinies présentées (§3.2). Cette finalisation reposera sur la définition de règles de transcription ou réécritures des modèles B en VHDL, l'ensemble de ces règles formant le traducteur B/HDL.
D'autre part, l'apport effectif de la démarche de modélisation proposée doit être évaluer par le traitement d' une étude de cas appartenant au domaine cible de prédilection indiqué précédemment un système critique de taille adéquate. Les travaux évoqués dans ([19]) nous semble un terrain propice d'expérimentation.
L'ensemble du matériel relatif à ces travaux est disponible à l'adresse: http://www3.inrets.fr/B@INRETS/BHDL/
5
REFERENCES
[1] J-R.
Abrial, "The B Book Assigning programs to meanings", Cambridge
University Press, ISBN 0-521-49619-5, 1996.
[2] R.
Airiau and J.-M. Bergé and V. Olive and J. Rouillard, "VHDL -- Langage,
modélisation, synthèse" , Presses Polytechniques et universitaires
romandes[10], Collection
Technique et scientifique des télécommunications 1998
[3] P. Behm, "Application d'une méthode formelle aux logiciels sécuritaires ferroviaires", Ateliers Logiciel Temps Reel 6èmes Jounées Internationales du Génie Logiciel, Part 5.1, 17-19 November 1993.
[4] Jean-Louis
Boulanger et Georges Mariano, "Modélisation formelle de circuit numériques
par la méthode B", INRETS Technical Report 1999-25-RT, 1999
[5] Jean-Louis
Boulanger
et Georges Mariano,
"Formalization of Digital Circuits Using the B Method", INRETS
Technical Report 2001-717-RT, 2001
[6] "Applications
of formal methods", M.G.
Hinchey and J.P. Bowen Editors, Prentice Hall, International Series in Computer
Science, 1995.
[7] Cliff
B.Jones,"Systematic Software Development using VDM" Prentice Hall
International;Second Edition, 1990.
[8] C.
Morgan, "Deriving programs from specifications", Prentice Hall
International; 1990.
[9] J. M.
Spivey, " The Z notation- a reference Manual," Prentice Hall
International; 1989.
[10] Christoph Kern and Mark
R. Greenstreet. "Formal verification in hardware design : A survey."
ACM Transactions on Design Automation of Electronic Systems, 1999.
[11] E.W
Dijkstra "A Discipline of Programming" Prentice Hall; 1976.
[12] Felix Nicoli, "Vérification Formelle de descriptions VHDL comportementales." , thèse, 1999.
[13] Max Fuchs and Michael Mendler. "A Functional Semantics of a
Verification Oriented Subset of VHDL." In Paolo E. Camurati and Hans
Eveking, editors, Correct Hardware Design and verification Methods, number 987
in LNCS, pages 293-310. Springer, October 1995.
[14] Simon Read and
Martyn Edwards. "A Formal Semantics of VHDL in Booyer-Moore Logic."
In Proceeding of the international Conference on Concurrent Engineering and
Electronic Design Automation (CEEDA 94), pages 395-40, 1994.
[15] John P. Van Tassel. "An Operational Semantics for a
subset of VHDL". In Carlos Delgado Kloos and Peter T. Breuer , editeur, "Formal
Semantics for VHDL", chapter3, pages 71-106. kluwer Academic, 1995.
[16] Jean-Raymond
Abrial. "Event driven circuit construction." MATISSE project, August
2000.
[17] Jean-Raymond
Abrial. "Event driven distributed program construction." MATISSE project,
August 2001
[18] Jean-Raymond
Abrial and L. Mussat, "Introducing Dynamic Constraints in B.", B'98 :
The 2nd International B Conference, pages 83--128, 1998
[19] M. Nicolaidis, N
Zaidan, T. Calin and D. Bied-Charreton, "ISIS: a Fail-Safe Interface Realised
in mart Power Technology", IEEE, pages 191--197 2000.