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. Tiene su origen en el trabajo realizado en el Laboratorio IBM de Viena [1] en la década de 1970 y ha crecido hasta incluir un grupo de técnicas y herramientas basadas en un lenguaje de especificación formal: el lenguaje de especificación VDM (VDM-SL). Tiene una forma extendida, VDM++, [2] que admite el modelado de sistemas orientados a objetos y concurrentes. El soporte para VDM incluye herramientas comerciales y académicas para analizar modelos, incluido el soporte para probar y demostrar propiedades de modelos y generar código de programa a partir de modelos VDM validados. Existe una historia de uso industrial de VDM y sus herramientas y un creciente cuerpo de investigación en el formalismo ha llevado a contribuciones notables a la ingeniería de sistemas críticos, compiladores , sistemas concurrentes y en lógica para la ciencia informática .
Los sistemas informáticos pueden modelarse en VDM-SL a un nivel de abstracción más alto que el que se puede lograr con lenguajes de programación, lo que permite el análisis de diseños y la identificación de características clave, incluidos los defectos, en una etapa temprana del desarrollo del sistema. Los modelos que se han validado se pueden transformar en diseños de sistemas detallados mediante un proceso de refinamiento. El lenguaje tiene una semántica formal, lo que permite probar las propiedades de los modelos con un alto nivel de seguridad. También tiene un subconjunto ejecutable, de modo que los modelos se pueden analizar mediante pruebas y se pueden ejecutar a través de interfaces gráficas de usuario, de modo que los modelos pueden ser evaluados por expertos que no necesariamente están familiarizados con el lenguaje de modelado en sí.
Los orígenes de VDM-SL se encuentran en el Laboratorio IBM en Viena , donde la primera versión del lenguaje se llamó Vienna Definition Language (VDL). [3] El VDL se utilizó esencialmente para dar descripciones semánticas operacionales en contraste con el VDM – Meta -IV que proporcionaba semánticas denotacionales [4]
«A finales de 1972, el grupo de Viena volvió a centrarse en el problema de desarrollar sistemáticamente un compilador a partir de una definición de lenguaje. El enfoque general adoptado se denominó "Método de desarrollo de Viena"... El metalenguaje realmente adoptado ("Meta-IV") se utiliza para definir partes importantes de PL/1 (como se indica en ECMA 74, curiosamente un "documento de normas 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.
Por lo tanto, 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 el lenguaje de programación BASIC , FORTRAN , el lenguaje de programación APL , ALGOL 60, el lenguaje de programación Ada y el lenguaje de programación Pascal . Meta-IV evolucionó en varias variantes, generalmente descritas como las escuelas danesa, inglesa e irlandesa.
La "Escuela Inglesa" se deriva 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). Hace hincapié en el modelado de estados persistentes [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 a través de operaciones que pueden tener efectos secundarios en el estado y que en su mayoría se especifican implícitamente utilizando una condición previa y una condición posterior. La "Escuela Danesa" ( Bjørner et al. 1982) ha tendido a enfatizar un enfoque constructivo con una especificación operacional explícita utilizada en mayor medida. El trabajo en la escuela danesa condujo al primer compilador Ada validado europeo.
En 1996 se publicó una norma ISO para el lenguaje (ISO, 1996).
La sintaxis y la semántica de VDM-SL y VDM++ se describen en detalle en los manuales de lenguaje de 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 definida por ISO (ASCII). Algunos textos prefieren una sintaxis matemática más concisa .
Un modelo VDM-SL es una descripción del sistema 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 realizan sobre ellos.
VDM-SL incluye tipos básicos que modelan 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 en términos de los tipos ya introducidos. Por ejemplo, un tipo que modele identificadores de usuario para un sistema de gestión de inicio de sesión podría definirse de la siguiente manera:
tiposId. de usuario = natPara manipular valores pertenecientes a tipos de datos, se definen operadores sobre los valores. Por lo tanto, se proporcionan sumas, restas, etc. de números naturales, así como operadores booleanos como igualdad y desigualdad. El lenguaje no fija un número representable máximo o mínimo ni una precisión para los números reales. Dichas restricciones se definen cuando son necesarias en cada modelo por medio de invariantes de tipo de datos (expresiones booleanas que denotan condiciones que deben respetar todos los elementos del tipo definido). Por ejemplo, un requisito de que los identificadores de usuario no deben ser mayores que 9999 se expresaría de la siguiente manera (donde <=es el operador booleano "menor o igual a" en números naturales):
Id. de usuario = natinvuid ==uid <= 9999Dado que los invariantes pueden ser expresiones lógicas arbitrariamente complejas y la pertenencia a un tipo definido está limitada únicamente a aquellos valores que satisfacen el invariante, la corrección de tipo en VDM-SL no es decidible automáticamente 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 agregarí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 determinar su igualdad; no se definen otros operadores en 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 determinar su igualdad.
Por ejemplo, al modelar un controlador de señal de tráfico, puede ser conveniente definir valores para representar los colores de la señal de tráfico como tipos de comillas:
< Rojo > , < Ámbar > , < Ámbar intermitente > , < Verde >Los tipos básicos por sí solos tienen un valor limitado. Se crean tipos de datos nuevos y más estructurados mediante 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 señales de tráfico, el tipo que modela el color de una señal de tráfico 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 en tipos de comillas.
Los tipos de productos cartesianos también se pueden definir en VDM-SL. El tipo (A1*…*An)es el tipo compuesto por todas las tuplas de valores, cuyo primer elemento es del tipo A1y el segundo del 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:Unoes el producto cartesiano con campos etiquetados como f1,…,fn. Un elemento de tipo Tpuede estar compuesto por sus partes constituyentes mediante un constructor, escrito mk_T. A la inversa, dado un elemento de tipo T, los nombres de campo pueden usarse para seleccionar el componente nombrado. Por ejemplo, el tipo
Fecha:: día:nat1 mes:nat1 año:natinv mk_Date(d,m,y) == d<=31 y m<=12modela 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 al invariante. Combinando estos:
mk_Date(1,4,2001).mes = 4Los 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 producirse duplicación y las asignaciones representan correspondencias finitas entre dos conjuntos de valores.
El constructor de tipo de 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 en los conjuntos para construir su unión, intersecciones, determinar relaciones de subconjuntos adecuadas y no estrictas, etc.
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 todas las cadenas finitas de caracteres. Se definen varios operadores en secuencias para construir concatenaciones, selección de elementos y subsecuencias, etc. Muchos de estos operadores son parciales en el sentido de que no están definidos para ciertas aplicaciones. Por ejemplo, la selección del quinto elemento de una secuencia que contiene solo tres elementos no está definida.
El orden y la repetición de los elementos de una secuencia son significativos, por lo que [a, b]no es igual a [b, a], y [a]no es igual a [a, a].
Una asignación finita es una correspondencia entre dos conjuntos, el dominio y el rango, con el dominio que indexa los elementos del rango. Por lo tanto, es similar a una función finita. El constructor de tipo de asignación en VDM-SL (escrito map T1 to T2donde T1y T2son tipos predefinidos) construye el tipo compuesto por todas las asignaciones finitas de conjuntos de T1valores a conjuntos de T2valores. Por ejemplo, la definición de tipo
Cumpleaños = asignar cadena a fecha Define un tipo Birthdaysque asigna cadenas de caracteres a Date. Nuevamente, los operadores se definen en asignaciones para indexar en la asignación, fusionar asignaciones, sobrescribir y extraer subasignaciones.
La principal diferencia entre las notaciones VDM-SL y VDM++ es la forma en que se aborda la estructuración. En VDM-SL hay una extensión modular convencional, mientras que VDM++ tiene un mecanismo de estructuración orientado a objetos tradicional con clases y herencia.
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 pueden explicarse de la siguiente manera:
moduleseguida del nombre del módulo. Al final de un módulo endse escribe la palabra clave seguida nuevamente del nombre del módulo.importsy sigue con una secuencia de importaciones desde diferentes módulos. Cada una de estas importaciones de módulos se inicia con la palabra clave fromseguida del nombre del módulo y una firma del módulo. La firma del 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. Además, puede estar presente información de tipo opcional y, finalmente, es posible cambiar el nombre de cada una de las construcciones al importar. Para los tipos, también se necesita usar la palabra clave structsi se desea obtener acceso a la estructura interna de un tipo en particular.exportsseguida de una firma de módulo de exportaciones. La firma de módulo de exportaciones 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. En caso de que se desee exportar la estructura interna de un tipo, structse debe utilizar la palabra clave.En VDM++ la estructuración se realiza mediante clases y herencia múltiple. Los conceptos clave son:
classseguida del nombre de la clase. Al final de una clase endse escribe la palabra clave seguida nuevamente del nombre de la clase.is subclass ofseguidas de una lista separada por comas de nombres de superclases.private, publicy protected.En VDM-SL, las funciones se definen sobre los tipos de datos definidos en un modelo. El soporte para la abstracción requiere que sea posible caracterizar el resultado que una función debe calcular sin tener que decir cómo debe calcularse. El mecanismo principal para hacer esto es la definición de función implícita 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: publicación real r*r = x Aquí la poscondición no define un método para calcular el resultado r, sino que establece qué propiedades se pueden suponer que tiene. Nótese que esto define una función que devuelve una raíz cuadrada válida; no hay ningún requisito de que deba ser 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. Nótese que las funciones en VDM-SL deben ser deterministas, de modo que una función que satisfaga la especificación del ejemplo anterior siempre debe devolver el mismo resultado para la misma entrada.
Se llega a una especificación de función más restringida reforzando la condición posterior. 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 condiciones previas 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 de cálculo de raíz cuadrada que funciona únicamente 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 condición previa y la condición posterior forman juntas un contrato que debe ser satisfecho por cualquier programa que pretenda implementar la función. La condición previa registra los supuestos bajo los cuales la función garantiza devolver un resultado que satisface la condición posterior. Si se llama a una función con entradas que no satisfacen su condición previa, el resultado no está definido (de hecho, ni siquiera se garantiza la terminación).
VDM-SL también admite la definición de funciones ejecutables a la manera 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 [] de lo contrario [( hd s) ** 2 ] ^ SqList ( tl s) Esta definición recursiva consta de una firma de función que proporciona 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 después de len r = len s y para todo i en el conjunto inds s y 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".
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 someStateRegister : nat, podríamos definirlo en VDM-SL como:
Registro estatal de algúnRegistroEstatal : nat end En VDM++ esto se definiría como:
variables de instancia someStateRegister : natUna operación para cargar un valor en esta variable podría especificarse como:
CARGAR (i:nat) text wr algúnStateRegister:nat post algúnStateRegister = i La cláusula externaext ( ) especifica a qué partes del estado puede acceder la operación, rdlo que indica acceso de solo lectura y wres acceso de lectura y escritura.
A veces es importante hacer referencia al valor de un estado antes de que se modificara; 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.
Este es un ejemplo de una definición de función implícita. La función devuelve el elemento más grande de un conjunto de números enteros positivos:
máx(s:conjunto de nat)r:nat antes de la tarjeta s > 0 después de r en el conjunto s y para todo r' en el conjunto s y r' <= r La poscondició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.
multp(i,j:nat)r:nat pre verdadero post r = i*j Aplicación de 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 de lo contrario si es -par(i) entonces 2 *multp(i/ 2 ,j) de lo contrario j+multp(i- 1 ,j) Entonces la obligación de prueba pasa a ser:
para todo i, j : nat y multp(i,j):nat y multp(i, j) = i*jEsto se puede demostrar correctamente mediante:
Este es un ejemplo clásico que ilustra el uso de la especificación de operaciones implícitas en un modelo basado en estados de una estructura de datos conocida. La cola se modela como una secuencia compuesta de elementos de un tipo Qelt. La representación es Qeltinmaterial 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 cola operaciones ENQUEUE (e: Qelt ) ext wr q: Cola de mensajes q = q~ ^ [e]; DEQUEUE ()e: Qelt ext wr q: Cola pre q <> [] post q~ = [e]^q; IS - EMPTY ()r:bool ext rd q: Cola de mensajes r <= > ( len q = 0 ) Como ejemplo muy simple de un modelo VDM-SL, considere un sistema para mantener los detalles de la cuenta bancaria del cliente. Los clientes se modelan por números de cliente ( CustNum ), las cuentas se modelan por números de cuenta ( AccNum ). Las representaciones de los números de cliente se consideran inmateriales y, por lo tanto, se modelan por un tipo de token. Los saldos y sobregiros se modelan por tipos numéricos.
AccNum = token; CustNum = token; Saldo = int ; Sobregiro = nat; AccData :: propietario : CustNum saldo : Saldo estado Banco de accountMap : asigna AccNum a AccData overdraftMap : asigna CustNum a Overdraft inv mk_Bank(accountMap,overdraftMap) == para todos a en el conjunto rng accountMap y a.owner en el conjunto dom overdraftMap y a.balance >= -overdraftMap(a.owner) Con operaciones: NEWC asigna un nuevo número de cliente:
operaciones NEWC (od : Sobregiro )r : CustNum ext wr overdraftMap : asigna CustNum a Sobregiro post r no en el conjunto dom ~overdraftMap y 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 : asigna AccNum a AccData rd overdraftMap asigna CustNum a Sobregiro pre cu en el conjunto dom overdraftMap post r no en el conjunto dom accountMap~ y accountMap = accountMap~ ++ {r| -> mk_AccData(cu, 0 )} ACINF devuelve todos los saldos de todas las cuentas de un cliente, como un mapa del número de cuenta al saldo:
ACINF (cu : CustNum )r : asigna AccNum a Balance ext rd accountMap : asigna AccNum a AccData post r = {an | -> accountMap(an).balance | an en el conjunto dom accountMap y accountMap(an).owner = cu} Varias herramientas diferentes admiten VDM:
El VDM se ha aplicado ampliamente en una variedad de dominios de aplicación. Las aplicaciones más conocidas son:
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 luego la descomposición de las operaciones .
La reificación de datos desarrolla los tipos de datos abstractos en estructuras de datos más concretas , mientras que la descomposición de operaciones desarrolla las especificaciones implícitas (abstractas) de operaciones y funciones en algoritmos que pueden implementarse directamente en un lenguaje de computadora elegido.
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 abstracta 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 retr : NEW_REP -> ABS_REP. La corrección de una reificación de datos depende de demostrar la adecuación , es decir
![{\displaystyle {\begin{array}{|rcl|}{\textbf {Especificación}}&&{\textbf {Implementación}}\\\hline {\text{Tipo de datos abstractos}}&\xrightarrow {\text{Reificación de datos}} &{\text{Estructura de datos}}\\{\text{Operaciones}}&{\xrightarrow[{\text{Descomposición de operaciones}}]{}}&{\text{Algoritmos}}\end{array}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e7cfd927beebe328e3bd51537dffb7316579b2b7)
para todo a: ABS_REP & existe r: NEW_REP & a = retr(r) Dado que la representación de los datos ha cambiado, es necesario actualizar las operaciones y funciones para que operen en NEW_REP. Se debe demostrar que las nuevas operaciones y funciones conservan cualquier invariante de tipo de datos en la nueva representación. Para demostrar que las nuevas operaciones y funciones modelan las que se encuentran en la especificación original, es necesario cumplir con dos obligaciones de prueba:
para todos r: NEW_REP y pre - OPA (retr(r)) => pre - OPR (r) para todos ~r,r: NEW_REP y pre - OPA (retr(~r)) y post - OPR (~r,r) => post - OPA (retr(~r,), retr(r)) En un sistema de seguridad empresarial, los trabajadores reciben tarjetas de identificación, que se introducen en lectores de tarjetas al entrar y salir de la fábrica. Operaciones necesarias:
INIT()inicializa el sistema, asume que la fábrica está vacíaENTER(p : Person)registra que un trabajador está entrando a la fábrica; los datos de los trabajadores 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 está en la fábrica o no.Formalmente esto sería:
tipos Persona = token; Trabajadores = conjunto de Personas ; AWCCS estatal de pres: Los trabajadores terminan operaciones INIT () ext wr pres: Trabajadores post pres = {}; ENTER (p : Persona ) ext wr pres : Trabajadores pre p no está en el conjunto pres post pres = pres~ sindicato {p}; SALIR (p : Persona ) ext wr pres : Trabajadores pre p en el conjunto pres post pres = pres~\{p}; IS - PRESENTE (p : Persona ) r : bool ext rd pres : Trabajadores post r <= > p en conjunto 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 a partir de la especificación es representar los datos en términos de una secuencia. Estas secuencias no deben permitir la 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 útil para sistemas basados en modelos, pero no es adecuado si el sistema está basado en el tiempo. Para estos casos, el cálculo de sistemas comunicantes (CCS) es más útil.