Worldlex Wiki La méthode de développement viennoise ( VDM ) est l'une des méthodes formelles les plus anciennes pour le développement de systèmes informatiques. Issue des travaux menés au laboratoire IBM de Vienne dans les années 1970, elle s'est développée pour inclure un ensemble de techniques et d'outils basés sur un langage de spécification formel : le langage de spécification VDM (VDM-SL). Il existe une version étendue, VDM++ , qui prend en charge la modélisation de systèmes orientés objet et concurrents. La VDM est prise en charge par des outils commerciaux et académiques d'analyse de modèles, notamment pour tester et prouver les propriétés des modèles et générer du code à partir de modèles VDM validés. L'utilisation industrielle de la VDM et de ses outils est bien établie, et un nombre croissant de recherches sur ce formalisme a permis des contributions notables à l'ingénierie des systèmes critiques, des compilateurs , des systèmes concurrents et de la logique informatique .
IBM de Vienne , où la première version du langage s'appelait le Vienna Definition Language (VDL). Le VDL était essentiellement utilisé pour fournir des descriptions sémantiques opérationnelles , contrairement au VDM – Meta-IV qui fournissait une sémantique dénotationnelle .« Vers la fin de 1972, le groupe viennois s’est de nouveau intéressé au problème du développement systématique d’un compilateur à partir d’une définition de langage. L’approche globale adoptée a été appelée « méthode de développement viennoise »… Le métalangage effectivement adopté (« Meta-IV ») est utilisé pour définir des parties importantes de PL/1 (tel que présenté dans ECMA 74 – un document de normes formelles rédigé sous forme d’interpréteur abstrait) dans BEKIČ 74. »
Il n'y a pas de lien entre Meta-IV , et le langage META II de Schorre , ou son successeur Tree Meta ; il s'agissait de systèmes compilateur-compilateur plutôt que d'être adaptés aux descriptions formelles de problèmes.
Ainsi, Meta-IV a servi à définir une grande partie du langage de programmation PL/I . D'autres langages de programmation, tels que BASIC , FORTRAN , APL , ALGOL 60, Ada et Pascal , ont été décrits a posteriori, en tout ou en partie, à l'aide de Meta-IV et VDM-SL. Meta-IV a donné naissance à plusieurs variantes, généralement désignées comme les écoles danoise, anglaise et irlandaise.
L’« école anglaise » s’inspire des travaux de Cliff Jones sur les aspects de la modélisation de l’état persistant (VDM) non spécifiquement liés à la définition du langage et à la conception du compilateur (Jones 1980, 1990). Elle privilégie la modélisation de l’état persistant à travers l’utilisation de types de données construits à partir d’une riche collection de types de base. La fonctionnalité est généralement décrite par des opérations pouvant avoir des effets de bord sur l’état et qui sont le plus souvent spécifiées implicitement à l’aide d’une précondition et d’une postcondition. L’« école danoise » ( Bjørner et al. 1982) a eu tendance à privilégier une approche constructive, avec une spécification opérationnelle explicite plus fréquente. Les travaux de l’école danoise ont abouti au premier compilateur Ada européen validé.
Une norme ISO pour ce langage a été publiée en 1996 (ISO, 1996).
fonctionnalités VDM
La syntaxe et la sémantique de VDM-SL et VDM++ sont décrites en détail dans les manuels de langage de VDMTools et dans les ouvrages de référence. La norme ISO contient une définition formelle de la sémantique du langage. Dans la suite de cet article, la syntaxe d'échange (ASCII) définie par l'ISO est utilisée. Certains ouvrages privilégient une syntaxe mathématique plus concise .
Un modèle VDM-SL est une description de système exprimée en termes de fonctionnalités appliquées aux données. Il se compose d'une série de définitions de types de données et de fonctions ou opérations qui leur sont appliquées.
Types de base : types numériques, caractères, jetons et guillemets
VDM-SL inclut les types de modélisation de base des nombres et des caractères comme suit :
bool | booléens | faux, vrai | |||
nat | nombres naturels (y compris zéro) | entiers | nombres rationnels | nombres réels | |
T1 | T2 | ... | Tn | Union des typesT1,...,Tn | ||||
T1*T2*...*Tn | Produit cartésien de typesT1,...,Tn | ||||
T:: f1:T1 ... fn:Tn | Type composite (enregistrement) |
Le constructeur de type le plus simple forme l'union de deux types prédéfinis. Le type (A|B)contient tous les éléments du type A et tous les éléments du type B. Dans l'exemple du contrôleur de feux de circulation, le type modélisant la couleur d'un feu de circulation pourrait être défini comme suit :
Les types produits cartésiens peuvent également être définis dans VDM-SL. Le type (A1*…*An)est le type composé de tous les tuples de valeurs, dont le premier élément appartient au type A1et le second au type, A2et ainsi de suite. Le type composite ou type enregistrement est un produit cartésien avec des étiquettes pour les champs.
{a, b, c}a, betc{x | x:T & P(x)}xde type Ttel queP(x){i, ..., j}i0 et 1.je in set seest un élément de l'ensemblese not in set sen'est pas un élément de l'ensembless1 union s2s1ets2s1 inter s2s1ets2s1 \ s2s1ets2dunion sss1 psubset s2s2s1 subset s2s2card ssSéquences
Le constructeur de type séquence finie (écrit seq of Toù Test un type prédéfini) construit le type composé de toutes les listes finies de valeurs tirées du type T. Par exemple, la définition de type
[a, b, c]a, betc[f(x) | x:T & P(x)]f(x)pour chaque xtype (numérique) Ttelle que ( valeurs prises dans l'ordre numérique P(x))xhd sstl sslen sselems sss(i)ième élément desinds sss1^s2s1ets2Cartes
Une application finie est une correspondance entre deux ensembles, le domaine et l'image, le domaine indexant les éléments de l'image. Elle est donc similaire à une fonction finie. Le constructeur de type `map` en VDM-SL (écrit `map` map T1 to T2où `a` T1et ` T2b` sont des types prédéfinis) construit le type composé de toutes les applications finies d'ensembles de T1valeurs vers des ensembles de T2valeurs. Par exemple, la définition de type
{a |-> r, b |-> s}acorrespond à r, bcorrespond às{x |-> f(x) | x:T & P(x)}xmappe à f(x)pour tout xpour type Ttel queP(x)dom mmrng mmm(x)mappliqué àxm1 munion m2m1et m2( m1, m2doit être cohérente là où elles se chevauchent)m1 ++ m2m1écrasé parm2Structuration
La principale différence entre les notations VDM-SL et VDM++ réside dans la manière dont la structuration est gérée. VDM-SL utilise une extension modulaire classique, tandis que VDM++ emploie un mécanisme de structuration orienté objet traditionnel avec classes et héritage.
Structuration dans VDM-SL
La norme ISO relative au VDM-SL contient une annexe informative présentant différents principes de structuration. Ces principes s'appuient tous sur les techniques traditionnelles de dissimulation d'informations par modules et peuvent être expliqués comme suit :
- Nommage des modules : Chaque module commence par le mot-clé
modulesuivi de son nom. À la fin d’un module,endon écrit à nouveau le mot-clé suivi du nom du module. - Importation : Il est possible d'importer des définitions exportées d'autres modules. Cette opération s'effectue dans une section d'importations , précédée du mot-clé `import`
importset suivie d'une séquence d'importations provenant de différents modules. Chaque importation de module commence par le mot-clé `import`,fromsuivi du nom du module et d'une signature de module. Cette signature peut être soit simplement le mot-cléallindiquant l'importation de toutes les définitions exportées de ce module, soit une séquence de signatures d'importation. Les signatures d'importation sont spécifiques aux types, valeurs, fonctions et opérations, et chacune commence par le mot-clé correspondant. De plus, ces signatures d'importation nomment les constructions auxquelles on souhaite accéder. Des informations de type optionnelles peuvent également être présentes, et il est possible de renommer chaque construction lors de l'importation. Pour les types, il est également nécessaire d'utiliser le mot-clé `init`structsi l'on souhaite accéder à la structure interne d'un type particulier. - Exportation : Les définitions d’un module auxquelles on souhaite que d’autres modules aient accès sont exportées à l’aide du mot-clé `export`
exportssuivi d’une signature de module `export`. Cette signature peut se limiter au mot-clé ` export`allou être une séquence de signatures `export`. Ces signatures sont spécifiques aux types, aux valeurs, aux fonctions et aux opérations, et chacune commence par le mot-clé correspondant. Pour exporter la structure interne d’un type,structil faut utiliser le mot-clé `export`. - Fonctionnalités plus exotiques : Les versions précédentes de VDM-SL prenaient également en charge les modules paramétrés et leurs instanciations. Cependant, ces fonctionnalités ont été retirées de VDMTools vers l’an 2000, car elles étaient rarement utilisées dans les applications industrielles et présentaient de nombreux problèmes de compatibilité avec l’outil.
Structuration dans VDM++
Dans VDM++, la structuration s'effectue à l'aide de classes et de l'héritage multiple . Les concepts clés sont :
- Classe : Chaque classe commence par le mot-clé `
classclass`, suivi de son nom. À la fin du nom d’une classe,endon écrit à nouveau le mot-clé `class`, suivi du nom de la classe. - Héritage : Dans le cas où une classe hérite de constructions d'autres classes, le nom de la classe dans l'en-tête de classe peut être suivi des mots-clés
is subclass ofsuivis d'une liste de noms de superclasses séparés par des virgules. - Modificateurs d'accès : Le masquage d'informations en VDM++ s'effectue de la même manière que dans la plupart des langages orientés objet, à l'aide de modificateurs d'accès. En VDM++, les définitions sont privées par défaut, mais il est possible d'utiliser l'un des mots-clés modificateurs d'accès suivants devant chaque définition : `private`
private, ` private`publicet `protectedprivate`.
Fonctionnalités de modélisation
Modélisation fonctionnelle
En VDM-SL, les fonctions sont définies sur les types de données définis dans un modèle. La prise en charge de l'abstraction exige qu'il soit possible de caractériser le résultat qu'une fonction doit calculer sans avoir à préciser comment ce calcul doit être effectué. Le principal mécanisme permettant cela est la définition implicite de fonction, dans laquelle, au lieu d'une formule calculant un résultat, un prédicat logique sur les variables d'entrée et de résultat, appelé postcondition , définit les propriétés du résultat. Par exemple, une fonction SQRTcalculant la racine carrée d'un nombre naturel pourrait être définie comme suit :
SqList : séquence de nat -> séquence de nat SqList (s) == si s = [] alors [] sinon [( hd s) ** 2 ] ^ SqList ( tl s)
Cette définition récursive se compose d'une signature de fonction précisant les types des entrées et du résultat, et d'un corps de fonction. Une définition implicite de cette même fonction pourrait prendre la forme suivante :
pour tout p dans l'ensemble T_p & pré -f(p) => f(p): T_r et post -f(p, f(p))
Ainsi, « fest une implémentation correcte » doit être interprété comme « fsatisfait aux spécifications ».
Modélisation basée sur les états
En VDM-SL, les fonctions n'ont pas d'effets de bord, comme la modification de l'état d'une variable globale persistante . Cette fonctionnalité étant utile dans de nombreux langages de programmation, un concept similaire existe : au lieu de fonctions, ce sont des opérations qui permettent de modifier les variables d'état (également appelées variables globales ).
Par exemple, si nous avons un état constitué d'une seule variable , nous pourrions le définir en VDM-SL comme suit :someStateRegister: nat
Type de données abstrait de file d'attente
Il s'agit d'un exemple classique illustrant l'utilisation de la spécification implicite des opérations dans un modèle à états d'une structure de données bien connue. La file d'attente est modélisée comme une séquence composée d'éléments d'un type donné Qelt. La représentation de ce type est Qeltsans importance et est donc définie comme un type jeton.
expérience industrielle
La technologie VDM a été largement utilisée dans divers domaines d'application. Parmi les plus connues, citons :
- Compilateurs Ada et CHILL : Le premier compilateur Ada validé européen a été développé par Dansk Datamatik Center à l'aide de VDM. De même, la sémantique de CHILL et de Modula-2 a été décrite dans leurs normes à l'aide de VDM.
- ConForm : une expérience menée chez British Aerospace comparant le développement conventionnel d'une passerelle de confiance avec un développement utilisant VDM.
- Dust-Expert : Un projet réalisé par Adelard au Royaume-Uni pour une application liée à la sécurité, visant à déterminer si la sécurité est appropriée dans l'aménagement des installations industrielles.
- Développement de VDMTools : La plupart des composants de la suite d’outils VDMTools sont eux-mêmes développés à l’aide de VDM. Ce développement a été réalisé au IFAD au Danemark et au CSK au Japon .
- TradeOne : Certains composants clés du système de back-office TradeOne, développé par CSK Systems pour la bourse japonaise, ont été conçus à l’aide de VDM. Des mesures comparatives existent concernant la productivité des développeurs et la densité de défauts des composants développés avec VDM par rapport au code développé de manière conventionnelle.
- FeliCa Networks a annoncé le développement d'un système d'exploitation pour un circuit intégré destiné aux applications de téléphonie cellulaire .
Raffinement
L'utilisation de VDM commence par un modèle très abstrait et le développe en une implémentation. Chaque étape implique la réification des données , puis la décomposition des opérations .
La réification des données transforme les types de données abstraits en structures de données plus concrètes , tandis que la décomposition des opérations transforme les spécifications implicites (abstraites) des opérations et des fonctions en algorithmes qui peuvent être directement implémentés dans un langage informatique de choix.
Réification des données
La réification des données (raffinement progressif) consiste à trouver une représentation plus concrète des types de données abstraits utilisés dans une spécification. Plusieurs étapes peuvent être nécessaires avant d'aboutir à une implémentation. Chaque étape de réification d'une représentation de données abstraite ABS_REPimplique la proposition d'une nouvelle représentation NEW_REP. Afin de démontrer l'exactitude de cette nouvelle représentation, une fonction de récupération est définie, qui se rapporte NEW_REPà la ABS_REPreprésentation initiale . La validité d'une réification des données dépend de la preuve de l'adéquation de cette fonction .retr: NEW_REP -> ABS_REP
- Règle de domaine :
pour tout r : NEW_REP & pre - OPA (retr(r)) => pre - OPR (r)
- Règle de modélisation :
forall ~r,r: NEW_REP & pre - OPA (retr(~r)) and post - OPR (~r,r) => post - OPA (retr(~r,), retr(r))
Exemple de réification des données
Dans un système de sécurité d'entreprise, les employés reçoivent des cartes d'identification ; celles-ci sont insérées dans des lecteurs à l'entrée et à la sortie de l'usine. Opérations requises :
INIT()initialise le système, en supposant que l'usine est videENTER(p: Person)enregistre l'entrée d'un travailleur dans l'usine ; les informations relatives aux travailleurs sont lues sur leur carte d'identité.EXIT(p: Person)enregistrements indiquant qu'un travailleur quitte l'usineIS-PRESENT(p: Person) r: boolvérifie si un travailleur spécifié est présent ou non dans l'usine.
Formellement, cela donnerait :
[a,b]même que [b,a].La méthode de développement viennoise est précieuse pour les systèmes à base de modèles. Elle n'est pas appropriée si le système est temporel. Dans ce cas, le calcul des systèmes communicants (CCS) est plus pertinent.