Hispanopedia Wiki
Articulo de referencia

Método de desarrollo de Viena

El Método de Desarrollo de Viena ( VDM ) es uno de los métodos formales más antiguos para el desarrollo de sistemas informáticos. Originado en el trabajo realizado en el Laborat...

Hispanopedia WikiContenido en espanolLectura gratuita

El Método de Desarrollo de Viena ( VDM ) es uno de los métodos formales más antiguos para el desarrollo de sistemas informáticos. Originado en el trabajo realizado en el Laboratorio IBM de Viena [ 1 ] en la década de 1970, ha evolucionado hasta incluir un conjunto de técnicas y herramientas basadas en un lenguaje de especificación formal: el Lenguaje de Especificación VDM (VDM-SL). Cuenta con una forma extendida, VDM++, [ 2 ] que admite el modelado de sistemas concurrentes y orientados a objetos . El soporte para VDM incluye herramientas comerciales y académicas para el análisis de modelos, incluyendo soporte para la prueba y demostración de propiedades de modelos y la generación de código de programa a partir de modelos VDM validados. Existe una larga trayectoria de uso industrial de VDM y sus herramientas, y un creciente cuerpo de investigación en el formalismo ha dado lugar a contribuciones notables a la ingeniería de sistemas críticos, compiladores , sistemas concurrentes y lógica para la informática .

Filosofía

En VDM-SL, los sistemas informáticos pueden modelarse con un nivel de abstracción superior al que se logra con los lenguajes de programación, lo que permite analizar los diseños e identificar características clave, incluidos los defectos, en una fase temprana del desarrollo del sistema. Los modelos validados pueden transformarse en diseños de sistemas detallados mediante un proceso de refinamiento. El lenguaje cuenta con una semántica formal que permite demostrar las propiedades de los modelos con un alto grado de fiabilidad. Además, dispone de un subconjunto ejecutable, de modo que los modelos pueden analizarse mediante pruebas y ejecutarse a través de interfaces gráficas de usuario, facilitando así su evaluación por expertos que no necesariamente estén familiarizados con el lenguaje de modelado.

Historia

Los orígenes de VDM-SL se encuentran en el Laboratorio IBM en Viena , donde la primera versión del lenguaje se denominó Lenguaje de Definición de Viena ( VDL). [ 3 ] El VDL se utilizó esencialmente para dar descripciones de semántica operacional en contraste con VDM-Meta-IV, que proporcionaba semántica denotacional. [ 4 ]

«Hacia finales de 1972, el grupo de Viena volvió a centrar su atención en el problema del desarrollo sistemático de un compilador a partir de la definición de un lenguaje. El enfoque general adoptado se ha denominado "Método de Desarrollo de Viena"... El metalenguaje adoptado ("Meta-IV") se utiliza para definir partes importantes de PL/1 (tal como se presenta en ECMA 74, curiosamente un "documento de estándares formales escrito como un intérprete abstracto") en BEKIČ 74.» [ 5 ]

No existe conexión entre Meta-IV , [ 6 ] y el lenguaje META II de Schorre , o su sucesor Tree Meta ; estos eran sistemas compilador-compilador en lugar de ser adecuados para descripciones formales de problemas.

Así pues, Meta-IV se utilizó para definir partes importantes del lenguaje de programación PL/I . Otros lenguajes de programación descritos retrospectivamente, o parcialmente, utilizando Meta-IV y VDM-SL incluyen BASIC , FORTRAN , APL , ALGOL 60, Ada y Pascal . Meta-IV evolucionó en varias variantes, generalmente conocidas como las escuelas danesa, inglesa e irlandesa.

La «Escuela Inglesa» surgió del trabajo de Cliff Jones sobre los aspectos de VDM no relacionados específicamente con la definición del lenguaje y el diseño del compilador (Jones 1980, 1990). Enfatiza el modelado del estado persistente [ 7 ] mediante el uso de tipos de datos construidos a partir de una rica colección de tipos base. La funcionalidad se describe típicamente mediante operaciones que pueden tener efectos secundarios en el estado y que se especifican mayoritariamente de forma implícita mediante una precondición y una postcondición. La «Escuela Danesa» ( Bjørner et al. 1982) ha tendido a enfatizar un enfoque constructivo con una especificación operacional explícita más utilizada. El trabajo en la escuela danesa condujo al primer compilador Ada validado europeo.

En 1996 se publicó una norma ISO para este lenguaje (ISO, 1996).

Características de VDM

La sintaxis y la semántica de VDM-SL y VDM++ se describen detalladamente en los manuales del lenguaje VDMTools y en los textos disponibles. La norma ISO contiene una definición formal de la semántica del lenguaje. En el resto de este artículo, se utiliza la sintaxis de intercambio (ASCII) definida por la ISO. Algunos textos prefieren una sintaxis matemática más concisa .

Un modelo VDM-SL es una descripción del sistema que se expresa en términos de la funcionalidad que se realiza sobre los datos. Consiste en una serie de definiciones de tipos de datos y funciones u operaciones que se ejecutan sobre ellos.

Tipos básicos: numéricos, de caracteres, de tokens y de comillas.

VDM-SL incluye tipos básicos de modelos, números y caracteres, como se indica a continuación:

Los tipos de datos se definen para representar los datos principales del sistema modelado. Cada definición de tipo introduce un nuevo nombre de tipo y proporciona una representación en términos de los tipos básicos o de los tipos ya introducidos. Por ejemplo, un tipo que modela los identificadores de usuario para un sistema de gestión de inicio de sesión podría definirse de la siguiente manera:

tipos ID de usuario = nat

Para manipular valores pertenecientes a tipos de datos, se definen operadores sobre dichos valores. Así, se proporcionan sumas, restas, etc., de números naturales, así como operadores booleanos como la igualdad y la desigualdad. El lenguaje no fija un número representable máximo o mínimo ni una precisión para los números reales. Estas restricciones se definen donde se requieren en cada modelo mediante invariantes de tipo de datos: expresiones booleanas que denotan condiciones que deben respetar todos los elementos del tipo definido. Por ejemplo, el requisito de que los identificadores de usuario no sean mayores que 9999 se expresaría de la siguiente manera (donde <=es el operador booleano "menor o igual que" sobre números naturales):

ID de usuario = nat inv uid == uid <= 9999

Dado que los invariantes pueden ser expresiones lógicas arbitrariamente complejas, y la pertenencia a un tipo definido se limita únicamente a aquellos valores que satisfacen el invariante, la corrección de tipos en VDM-SL no es automáticamente decidible en todas las situaciones.

Los otros tipos básicos incluyen `char` para caracteres. En algunos casos, la representación de un tipo no es relevante para el propósito del modelo y solo añadiría complejidad. En tales casos, los miembros del tipo pueden representarse como tokens sin estructura. Los valores de los tipos de token solo se pueden comparar para comprobar su igualdad; no se definen otros operadores sobre ellos. Cuando se requieren valores con nombre específicos, estos se introducen como tipos de comillas. Cada tipo de comillas consta de un valor con nombre del mismo nombre que el tipo en sí. Los valores de los tipos de comillas (conocidos como literales de comillas) solo se pueden comparar para comprobar su igualdad.

Por ejemplo, al modelar un controlador de semáforos, puede ser conveniente definir valores para representar los colores del semáforo como tipos de cita:

< Rojo > , < Ámbar > , < Ámbar intermitente > , < Verde >

Constructores de tipos: tipos de unión, producto y compuestos

Los tipos básicos por sí solos tienen un valor limitado. Los nuevos tipos de datos, más estructurados, se construyen utilizando constructores de tipos.

El constructor de tipos más básico forma la unión de dos tipos predefinidos. El tipo (A|B)contiene todos los elementos del tipo A y todos los del tipo B. En el ejemplo del controlador de semáforo, el tipo que modela el color de un semáforo podría definirse de la siguiente manera:

Color de la señal = < Rojo > | < Ámbar > | < Ámbar intermitente > | < Verde >

Los tipos enumerados en VDM-SL se definen como se muestra arriba, como uniones de tipos de cotización.

En VDM-SL también se pueden definir tipos de producto cartesiano. El tipo (A1*…*An)es el tipo compuesto por todas las tuplas de valores, cuyo primer elemento pertenece al tipo A1y el segundo al tipo, A2y así sucesivamente. El tipo compuesto o de registro es un producto cartesiano con etiquetas para los campos. El tipo

T :: f1:A1 f2:A2 ... fn:Un

es el producto cartesiano con campos etiquetados f1,…,fn. Un elemento de tipo Tpuede componerse a partir de sus partes constituyentes mediante un constructor, escrito mk_T. Por el contrario, dado un elemento de tipo T, los nombres de los campos pueden usarse para seleccionar el componente nombrado. Por ejemplo, el tipo

Fecha :: día:nat1 mes:nat1 año:nat inv mk_Date(d,m,y) == d<=31 y m<=12

modela un tipo de fecha simple. El valor mk_Date(1,4,2001)corresponde al 1 de abril de 2001. Dada una fecha d, la expresión d.monthes un número natural que representa el mes. Si se desea, se pueden incorporar restricciones sobre los días por mes y los años bisiestos en la invariante. Combinando estos:

mk_Date(1,4,2001).month = 4

Colecciones

Los tipos de colección modelan grupos de valores. Los conjuntos son colecciones finitas no ordenadas en las que se suprime la duplicación entre valores. Las secuencias son colecciones finitas ordenadas (listas) en las que puede haber duplicación y las asignaciones representan correspondencias finitas entre dos conjuntos de valores.

Conjuntos

El constructor de tipo conjunto (escrito set of Tdonde Tes un tipo predefinido) construye el tipo compuesto por todos los conjuntos finitos de valores extraídos del tipo T. Por ejemplo, la definición de tipo

UGroup = conjunto de UserId

Define un tipo UGroupcompuesto por todos los conjuntos finitos de UserIdvalores. Se definen varios operadores sobre conjuntos para construir su unión, intersecciones, determinar relaciones de subconjuntos propias y no estrictas, etc.

Secuencias

El constructor de tipo de secuencia finita (escrito seq of Tdonde Tes un tipo predefinido) construye el tipo compuesto por todas las listas finitas de valores extraídos del tipo T. Por ejemplo, la definición de tipo

Cadena = secuencia de caracteres

Define un tipo Stringcompuesto por cadenas finitas de caracteres. Se definen varios operadores sobre secuencias para construir concatenaciones, seleccionar elementos y subsecuencias, etc. Muchos de estos operadores son parciales, en el sentido de que no están definidos para ciertas aplicaciones. Por ejemplo, seleccionar el quinto elemento de una secuencia que contiene solo tres elementos no está definido.

El orden y la repetición de los elementos en una secuencia son significativos, por lo que [a, b]no es igual a [b, a], y [a]no es igual a [a, a].

Mapas

Una aplicación finita es una correspondencia entre dos conjuntos, el dominio y el rango, donde el dominio indexa los elementos del rango. Por lo tanto, es similar a una función finita. El constructor de tipos de aplicación en VDM-SL (escrito map T1 to T2donde T1y T2son tipos predefinidos) construye el tipo compuesto por todas las aplicaciones finitas de conjuntos de T1valores a conjuntos de T2valores. Por ejemplo, la definición de tipo

Cumpleaños = mapear cadena a fecha

Define un tipo Birthdaysque asigna cadenas de caracteres a Date. Nuevamente, se definen operadores en asignaciones para indexar dentro de la asignación, fusionar asignaciones, sobrescribir y extraer subasignaciones.

Estructuración

La principal diferencia entre las notaciones VDM-SL y VDM++ radica en la forma en que se gestiona la estructuración. En VDM-SL se utiliza una extensión modular convencional, mientras que VDM++ emplea un mecanismo de estructuración orientado a objetos tradicional con clases y herencia.

Estructuración en VDM-SL

En la norma ISO para VDM-SL hay un anexo informativo que contiene diferentes principios de estructuración. Todos ellos siguen los principios tradicionales de ocultación de información con módulos y se pueden explicar de la siguiente manera:

  • Nomenclatura de módulos : Cada módulo comienza sintácticamente con la palabra clave moduleseguida del nombre del módulo. Al final de un módulo endse escribe la palabra clave seguida nuevamente del nombre del módulo.
  • Importación : Es posible importar definiciones exportadas desde otros módulos. Esto se realiza en una sección de importaciones que comienza con la palabra clave importsy va seguida de una secuencia de importaciones de diferentes módulos. Cada una de estas importaciones de módulos comienza con la palabra clave fromseguida del nombre del módulo y una firma de módulo. La firma de módulo puede ser simplemente la palabra clave allque indica la importación de todas las definiciones exportadas desde ese módulo, o puede ser una secuencia de firmas de importación. Las firmas de importación son específicas para tipos, valores, funciones y operaciones, y cada una de ellas comienza con la palabra clave correspondiente. Además, estas firmas de importación nombran las construcciones a las que se desea acceder. También se puede incluir información de tipo opcional y, finalmente, es posible renombrar cada una de las construcciones al importarlas. Para los tipos, también es necesario usar la palabra clave structsi se desea acceder a la estructura interna de un tipo en particular.
  • Exportación : Las definiciones de un módulo a las que se desea que otros módulos tengan acceso se exportan mediante la palabra clave exportsseguida de una firma de módulo de exportación. La firma de módulo de exportación puede consistir simplemente en la palabra clave allo en una secuencia de firmas de exportación. Dichas firmas de exportación son específicas para tipos, valores, funciones y operaciones, y cada una de ellas comienza con la palabra clave correspondiente. Si se desea exportar la estructura interna de un tipo, structse debe utilizar la palabra clave.
  • Funcionalidades más avanzadas : En versiones anteriores de VDM-SL, las herramientas también admitían módulos parametrizados e instanciaciones de dichos módulos. Sin embargo, estas funcionalidades se eliminaron de VDMTools alrededor del año 2000, ya que apenas se utilizaban en aplicaciones industriales y presentaban numerosos problemas.

Estructuración en VDM++

En VDM++ la estructuración se realiza mediante clases y herencia múltiple . Los conceptos clave son:

  • Clase : Cada clase comienza sintácticamente con la palabra clave classseguida del nombre de la clase. Al final de una clase endse escribe la palabra clave seguida nuevamente del nombre de la clase.
  • Herencia : En caso de que una clase herede construcciones de otras clases, el nombre de la clase en el encabezado de la clase puede ir seguido de las palabras clave is subclass ofseguidas de una lista de nombres de superclases separadas por comas.
  • Modificadores de acceso : La ocultación de información en VDM++ se realiza de la misma manera que en la mayoría de los lenguajes orientados a objetos mediante modificadores de acceso. En VDM++, las definiciones son privadas por defecto, pero delante de todas las definiciones es posible utilizar una de las palabras clave de modificador de acceso: private, publicy protected.

Funcionalidad de modelado

Modelado funcional

En VDM-SL, las funciones se definen sobre los tipos de datos definidos en un modelo. La compatibilidad con la abstracción requiere que sea posible caracterizar el resultado que una función debe calcular sin tener que especificar cómo debe calcularse. El mecanismo principal para lograr esto es la definición implícita de funciones , en la que, en lugar de una fórmula que calcule un resultado, un predicado lógico sobre las variables de entrada y resultado, denominado postcondición , proporciona las propiedades del resultado. Por ejemplo, una función SQRTpara calcular la raíz cuadrada de un número natural podría definirse de la siguiente manera:

SQRT (x:nat)r: post real r*r = x

Aquí, la postcondición no define un método para calcular el resultado, rsino que indica qué propiedades se pueden asumir. Cabe destacar que esto define una función que devuelve una raíz cuadrada válida; no se requiere que sea la raíz positiva o negativa. La especificación anterior se cumpliría, por ejemplo, con una función que devolviera la raíz negativa de 4, pero la raíz positiva de todas las demás entradas válidas. Es importante mencionar que las funciones en VDM-SL deben ser deterministas, de modo que una función que cumpla con la especificación del ejemplo anterior siempre debe devolver el mismo resultado para la misma entrada.

Se obtiene una especificación de función más restringida al reforzar la postcondición. Por ejemplo, la siguiente definición restringe la función para que devuelva la raíz positiva.

SQRT (x:nat)r: post real r*r = x y r >= 0

Todas las especificaciones de funciones pueden estar restringidas por precondiciones , que son predicados lógicos sobre las variables de entrada únicamente y que describen restricciones que se supone que se cumplen cuando se ejecuta la función. Por ejemplo, una función para calcular la raíz cuadrada que solo funciona con números reales positivos podría especificarse de la siguiente manera:

SQRTP (x: real )r: real pre x >= 0 post r*r = x y r >= 0

La precondición y la postcondición, en conjunto, forman un contrato que debe cumplir cualquier programa que pretenda implementar la función. La precondición registra los supuestos bajo los cuales la función garantiza devolver un resultado que satisfaga la postcondición. Si se llama a una función con entradas que no satisfacen su precondición, el resultado es indefinido (de hecho, ni siquiera se garantiza la terminación).

VDM-SL también admite la definición de funciones ejecutables al estilo de un lenguaje de programación funcional . En una definición de función explícita , el resultado se define mediante una expresión sobre las entradas. Por ejemplo, una función que produce una lista de los cuadrados de una lista de números podría definirse de la siguiente manera:

SqList: seq de nat -> seq de nat SqList (s) == si s = [] entonces [] sino [( hd s) ** 2 ] ^ SqList ( tl s)

Esta definición recursiva consta de una firma de función que indica los tipos de entrada y resultado, y un cuerpo de función. Una definición implícita de la misma función podría adoptar la siguiente forma:

SqListImp (s:seq de nat)r:seq de nat post len ​​r = len s y para todo i en el conjunto inds s & r(i) = s(i) ** 2

La definición explícita es, en un sentido simple, una implementación de la función especificada implícitamente. La corrección de una definición de función explícita con respecto a una especificación implícita puede definirse de la siguiente manera.

Dada una especificación implícita:

f(p: T_p )r: T_r pre pre -f(p) post post -f(p, r)

y una función explícita:

f:T _p -> T_r

Decimos que satisface la especificación si y solo si :

para todo p en el conjunto T_p y pre -f(p) => f(p): T_r y post -f(p, f(p))

Por lo tanto, " fes una implementación correcta" debe interpretarse como " fsatisface la especificación".

Modelado basado en estados

En VDM-SL, las funciones no tienen efectos secundarios como cambiar el estado de una variable global persistente . Esta es una capacidad útil en muchos lenguajes de programación, por lo que existe un concepto similar; en lugar de funciones, se utilizan operaciones para cambiar las variables de estado (también conocidas como globales ).

Por ejemplo, si tenemos un estado que consta de una sola variable , podríamos definirlo en VDM-SL como:someStateRegister : nat

Registro estatal de algúnRegistroEstatal : fin de nat

En VDM++ esto se definiría como:

variables de instancia someStateRegister : nat

Una operación para cargar un valor en esta variable podría especificarse de la siguiente manera:

CARGAR (i:nat) text wr someStateRegister:nat post someStateRegister = i

La cláusula externalsext ( ) especifica a qué partes del estado puede acceder la operación; rdindicando acceso de solo lectura y wracceso de lectura/escritura.

En ocasiones es importante hacer referencia al valor de un estado antes de que fuera modificado; por ejemplo, una operación para agregar un valor a la variable puede especificarse como:

AGREGAR (i:nat) text wr someStateRegister : nat post someStateRegister = someStateRegister~ + i

Donde el ~símbolo en la variable de estado en la postcondición indica el valor de la variable de estado antes de la ejecución de la operación.

Ejemplos

La función max

Este es un ejemplo de definición de función implícita. La función devuelve el elemento más grande de un conjunto de enteros positivos:

max(s:conjunto de nat)r:nat pre tarjeta s > 0 post r en el conjunto s y para todo r' en el conjunto s y r' <= r

La postcondición caracteriza el resultado en lugar de definir un algoritmo para obtenerlo. La precondición es necesaria porque ninguna función podría devolver un r en el conjunto s cuando el conjunto está vacío.

multiplicación de números naturales

multp(i,j:nat)r:nat pre verdadero post r = i*j

Aplicar la obligación de prueba forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))a una definición explícita de multp:

multp(i,j) == si i= 0 entonces 0 sino si es -par(i) entonces 2 *multp(i/ 2 ,j) sino j+multp(i- 1 ,j)

Entonces la obligación de prueba se convierte en:

para todo i, j : nat & multp(i,j):nat y multp(i, j) = i*j

Esto se puede demostrar correctamente mediante:

  1. Demostrar que la recursión termina (esto a su vez requiere demostrar que los números se hacen más pequeños en cada paso).
  2. Inducción matemática

Tipo de datos abstracto de cola

Este es un ejemplo clásico que ilustra el uso de la especificación implícita de operaciones en un modelo basado en estados de una estructura de datos bien conocida. La cola se modela como una secuencia compuesta por elementos de un tipo Qelt. La representación es Qeltirrelevante y, por lo tanto, se define como un tipo de token.

tipos Qelt = token; Cola = secuencia de Qelt ;estado LaCola de q : Fin de la colaoperaciones ENQUEUE (e: Qelt ) ext wr q: Queue post q = q~ ^ [e];DEQUEUE ()e: Qelt ext wr q: Cola pre q <> [] post q~ = [e]^q;ES - VACÍO ()r:bool ext rd q: Cola post r <= > ( len q = 0 )

Ejemplo de sistema bancario

Como ejemplo sencillo de un modelo VDM-SL, consideremos un sistema para mantener los detalles de las cuentas bancarias de los clientes. Los clientes se representan mediante números de cliente ( CustNum ), y las cuentas mediante números de cuenta ( AccNum ). Se considera que la representación de los números de cliente es irrelevante, por lo que se modela mediante un tipo de token. Los saldos y los sobregiros se modelan mediante tipos numéricos.

AccNum = token; CustNum = token; Balance = int ; Overdraft = nat;AccData :: propietario : CustNum saldo : Saldoestado Banco de accountMap : mapear AccNum a AccData overdraftMap : mapear CustNum a Overdraft inv mk_Bank(accountMap,overdraftMap) == para todos los a en el conjunto rng accountMap y a.owner en el conjunto dom overdraftMap y a.balance >= -overdraftMap(a.owner)

Con las operaciones: NEWC asigna un nuevo número de cliente:

operaciones NEWC (od : Sobregiro )r : CustNum ext wr overdraftMap : map CustNum to Overdraft post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r | -> od};

NEWAC asigna un nuevo número de cuenta y establece el saldo en cero:

NEWAC (cu : CustNum )r : AccNum ext wr accountMap : map AccNum to AccData rd overdraftMap map CustNum to Overdraft pre cu in set dom overdraftMap post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r| -> mk_AccData(cu, 0 )}

ACINF devuelve todos los saldos de todas las cuentas de un cliente, como un mapa de número de cuenta a saldo:

ACINF (cu : CustNum )r : map AccNum to Balance ext rd accountMap : map AccNum to AccData post r = {an | -> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}

Soporte de herramientas

Varias herramientas diferentes son compatibles con VDM:

  • VDMTools fue la principal herramienta comercial para VDM y VDM++, propiedad de CSK Systems , que también se encargó de su comercialización, mantenimiento y desarrollo, basándose en versiones anteriores desarrolladas por la empresa danesa IFAD. Los manuales y un tutorial práctico, archivados el 19 de noviembre de 2008 en Wayback Machine , están disponibles. Todas las licencias son gratuitas para la versión completa de la herramienta. Esta versión incluye generación automática de código para Java y C++, biblioteca de enlace dinámico y compatibilidad con CORBA.
  • Overture es una iniciativa de código abierto basada en la comunidad, cuyo objetivo es proporcionar herramientas gratuitas para todos los dialectos VDM (VDM-SL, VDM++ y VDM-RT), originalmente sobre la plataforma Eclipse y posteriormente sobre Visual Studio Code. Su propósito es desarrollar un marco de trabajo para herramientas interoperables que resulten útiles para aplicaciones industriales, investigación y educación.
  • vdm-mode es una colección de paquetes de Emacs para escribir especificaciones VDM utilizando VDM-SL, VDM++ y VDM-RT. Admite resaltado y edición de sintaxis, comprobación de sintaxis en tiempo real, autocompletado de plantillas y compatibilidad con intérpretes.
  • SpecBox ( archivado el 7 de julio de 2011 en Wayback Machine) : Adelard ofrece comprobación de sintaxis, una sencilla verificación semántica y la generación de un archivo LaTeX que permite imprimir las especificaciones en notación matemática. Esta herramienta es gratuita, pero ya no recibe mantenimiento.
  • Existen macros de LaTeX y LaTeX2e que permiten presentar modelos VDM con la sintaxis matemática del lenguaje estándar ISO. Estas macros han sido desarrolladas y son mantenidas por el Laboratorio Nacional de Física del Reino Unido. La documentación y las macros están disponibles en línea.

Experiencia industrial

VDM se ha aplicado ampliamente en diversos ámbitos de aplicación. Las aplicaciones más conocidas son:

  • Compiladores Ada y CHILL : El primer compilador Ada validado en Europa fue desarrollado por Dansk Datamatik Center utilizando VDM. [ 8 ] Asimismo, la semántica de CHILL y Modula-2 se describió en sus estándares utilizando VDM.
  • ConForm: Un experimento realizado en British Aerospace que compara el desarrollo convencional de una puerta de enlace de confianza con un desarrollo que utiliza VDM.
  • Dust-Expert: Un proyecto llevado a cabo por Adelard en el Reino Unido para una aplicación relacionada con la seguridad, cuyo objetivo es determinar si la seguridad es adecuada en el diseño de plantas industriales.
  • Desarrollo de VDMTools: La mayoría de los componentes del conjunto de herramientas VDMTools se desarrollan utilizando VDM. Este desarrollo se ha realizado en el IFAD en Dinamarca y en CSK en Japón . [ 9 ]
  • TradeOne: Algunos componentes clave del sistema administrativo TradeOne, desarrollado por CSK Systems para la bolsa de valores japonesa, se desarrollaron utilizando VDM. Existen mediciones comparativas de la productividad de los desarrolladores y la densidad de defectos de los componentes desarrollados con VDM frente al código desarrollado de forma convencional.
  • FeliCa Networks ha informado sobre el desarrollo de un sistema operativo para un circuito integrado destinado a aplicaciones de telefonía celular .

Refinamiento

El uso de VDM comienza con un modelo muy abstracto y lo desarrolla hasta convertirlo en una implementación. Cada paso implica la reificación de datos y, posteriormente, la descomposición de operaciones .

La reificación de datos transforma los tipos de datos abstractos en estructuras de datos más concretas , mientras que la descomposición de operaciones transforma las especificaciones implícitas (abstractas) de operaciones y funciones en algoritmos que pueden implementarse directamente en el lenguaje de programación que se prefiera.

EspecificaciónImplementaciónTipo de datos abstracto→Reificación de datosEstructura de datosOperaciones→descomposición de la operaciónAlgoritmos{\displaystyle {\begin{array}{|rcl|}{\textbf {Especificación}}&&{\textbf {Implementación}}\\\hline {\text{Tipo de datos abstracto}}&\xrightarrow {\text{Reificación de datos}} &{\text{Estructura de datos}}\\{\text{Operaciones}}&{\xrightarrow[{\text{Descomposición de operaciones}}]{}}&{\text{Algoritmos}}\end{array}}}

Reificación de datos

La reificación de datos (refinamiento por pasos) implica encontrar una representación más concreta de los tipos de datos abstractos utilizados en una especificación. Puede haber varios pasos antes de llegar a una implementación. Cada paso de reificación para una representación de datos abstractos ABS_REPimplica proponer una nueva representación NEW_REP. Para demostrar que la nueva representación es precisa, se define una función de recuperaciónNEW_REP que se relaciona con ABS_REP, es decir . La corrección de una reificación de datos depende de probar una adecuación , es decirretr : NEW_REP -> ABS_REP

para todo a: ABS_REP & existe r: NEW_REP & a = retr(r)

Dado que la representación de datos ha cambiado, es necesario actualizar las operaciones y funciones para que operen sobre NEW_REP. Se debe demostrar que las nuevas operaciones y funciones conservan cualquier invariante de tipo de datos en la nueva representación. Para probar que las nuevas operaciones y funciones modelan las que se encuentran en la especificación original, es necesario cumplir dos obligaciones de prueba:

  • Regla de dominio:
para todo r: NEW_REP & pre - OPA (retr(r)) => pre - OPR (r)
  • Regla de modelado:
para todo ~r,r: NEW_REP & pre - OPA (retr(~r)) y post - OPR (~r,r) => post - OPA (retr(~r,), retr(r))

Ejemplo de reificación de datos

En un sistema de seguridad empresarial, a los trabajadores se les entregan tarjetas de identificación; estas se introducen en lectores de tarjetas al entrar y salir de la fábrica. Operaciones requeridas:

  • INIT()Inicializa el sistema, asumiendo que la fábrica está vacía.
  • ENTER(p : Person)registra que un trabajador está entrando en la fábrica; los datos del trabajador se leen de la tarjeta de identificación.
  • EXIT(p : Person)registra que un trabajador está saliendo de la fábrica.
  • IS-PRESENT(p : Person) r : boolComprueba si un trabajador específico se encuentra en la fábrica o no.

Formalmente, esto sería:

tipos Persona = ficha; Trabajadores = conjunto de Persona ;AWCCS estatal de pre: Trabajadores terminanoperaciones INIT () ext wr pres: Workers post pres = {};INTRODUCIR (p : Persona ) ext wr pres : Trabajadores pre p no está en el conjunto pres post pres = pres~ unión {p};SALIDA (p : Persona ) ext wr pres : Trabajadores pre p en conjunto pres post pres = pres~\{p};ES - PRESENTE (p : Persona ) r : bool ext rd pres : Trabajadores post r <= > p en set pres~

Como la mayoría de los lenguajes de programación tienen un concepto comparable a un conjunto (a menudo en forma de matriz), el primer paso de la especificación es representar los datos en términos de una secuencia. Estas secuencias no deben permitir repetición, ya que no queremos que el mismo trabajador aparezca dos veces, por lo que debemos agregar un invariante al nuevo tipo de datos. En este caso, el orden no es importante, por lo que [a,b]es lo mismo que [b,a].

El método de desarrollo de Viena es valioso para sistemas basados ​​en modelos. No es apropiado si el sistema se basa en el tiempo. Para estos casos, el cálculo de sistemas comunicantes (CCS) resulta más útil.

Véase también

Lecturas adicionales

  • Bjørner, Dines; Cliff B. Jones (1978). El método de desarrollo de Viena: El metalenguaje, Lecture Notes in Computer Science 61. Berlín, Heidelberg, Nueva York: Springer. ISBN 978-0-387-08766-5.
  • O'Regan, Gerard (2006). Enfoques matemáticos para la calidad del software . Londres: Springer. ISBN 978-1-84628-242-3.
  • Cliff B. Jones, ed. (1984). Lenguajes de programación y su definición — H. Bekič (1936-1982) . Lecture Notes in Computer Science . Vol.  177. Berlín, Heidelberg, Nueva York, Tokio: Springer-Verlag. doi : 10.1007/BFb0048933 . ISBN 978-3-540-13378-0. S2CID 7488558 . 
  • Fitzgerald, JS y Larsen, PG, Modelado de sistemas: herramientas y técnicas prácticas en ingeniería de software . Cambridge University Press , 1998 ISBN 0-521-62348-0(Edición japonesa pub. Iwanami Shoten 2003 ISBN 4-00-005609-3). [ 10 ]
  • Fitzgerald, JS , Larsen, PG, Mukherjee, P., Plat, N. y Verhoef, M., Diseños validados para sistemas orientados a objetos . Springer Verlag 2005. ISBN 1-85233-881-4Sitio web de apoyoArchivado el 2 de marzo de 2018 en Wayback Machine, incluye ejemplos y soporte de herramientas gratuitas. [ 11 ]
  • Jones, CB , Desarrollo sistemático de software mediante VDM , Prentice Hall , 1990. ISBN 0-13-880733-7También disponible en línea y de forma gratuita: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip Archivado el 17 de julio de 2011 en Wayback Machine .
  • Bjørner, D. y Jones, CB , Especificación formal y desarrollo de software, Prentice Hall International, 1982. ISBN 0-13-880733-7
  • J. Dawes, La guía de referencia de VDM-SL , Pitman 1991. ISBN 0-273-03151-1
  • Organización Internacional de Normalización , Tecnología de la información – Lenguajes de programación, sus entornos e interfaces de software de sistema – Método de desarrollo de Viena – Lenguaje de especificación – Parte 1: Lenguaje base Norma internacional ISO/IEC 13817-1, diciembre de 1996.
  • Jones, CB , Desarrollo de software: Un enfoque riguroso , Prentice Hall International, 1980. ISBN 0-13-821884-6
  • Jones, CB y Shaw, RC (eds.), Estudios de caso en el desarrollo sistemático de software , Prentice Hall International, 1990. ISBN 0-13-880733-7
  • Bicarregui, JC, Fitzgerald, JS , Lindsay, PA, Moore, R. y Ritchie, B., Demostración en VDM: una guía práctica . Springer Verlag Formal Approaches to Computing and Information Technology (FACIT), 1994. ISBN 3-540-19813-X.

Referencias

  1. ↑ Parte de ese trabajo, incluyendo un informe técnico TR 25.139 sobre " Una definición formal de un subconjunto PL/1 ", fechado el 20 de diciembre de 1974, se reimprime en Jones 1984, págs. 107-155. Cabe destacar la lista de autores en orden: H. Bekič, D. Bjørner, W. Henhapl, CB Jones, P. Lucas.
  2. ↑ El doble signo más se adopta del lenguaje de programación orientado a objetos C++ basado en C.
  3. ^ Bjørner&Jones 1978, Introducción , p.ix
  4. ↑ Observaciones introductorias de Cliff B. Jones (editor) en Bekič 1984, pág. vii
  5. ^ Bjørner&Jones 1978, Introducción , p.xi
  6. ^ Bjørner & Jones 1978, p.24.
  7. ↑ Consulte el artículo sobre persistencia para conocer su uso en informática.
  8. ↑ Clemmensen, Geert B. (enero de 1986). "Reorientación y reubicación del sistema compilador DDC Ada: un estudio de caso: el Honeywell DPS 6". ACM SIGAda Ada Letters . 6 (1): 22– 28. doi : 10.1145/382256.382794 . S2CID 16337448 . 
  9. ↑ Peter Gorm Larsen, "Diez años de desarrollo histórico mediante el "arranque" de VDMTools", archivado el 23 de enero de 2021 en Wayback Machine , en Journal of Universal Computer Science , volumen 7(8), 2001
  10. ↑ " Modelado de sistemas: herramientas y técnicas prácticas en ingeniería de software " . Archivado del original el 17 de mayo de 2012. Consultado el 8 de septiembre de 2007 .
  11. ↑ " Diseños validados para sistemas orientados a objetos " . Archivado del original el 2 de marzo de 2018. Consultado el 8 de septiembre de 2007 .