Experiencias con el uso de Alloy en proyectos del mundo real.

Question

Hace algún tiempo que estoy interesado en los métodos formales.He utilizado métodos formales para razonar sobre algunas subáreas muy específicas de algunos proyectos en los que he estado trabajando.Nunca pude convencer a otros miembros del equipo para que intentaran lo mismo y mucho menos especificar un dominio completo con un método formal.

Un método que he encontrado particularmente interesante es Aleación.Creo que puede "escalar" mejor como base para un proyecto completo porque está conceptual y notariamente muy cerca de los lenguajes de programación reales.Además, las herramientas son bastante sólidas, por lo que los beneficios de la verificación del modelo están fácilmente disponibles.

Me interesaría mucho conocer cualquier experiencia del mundo real que ustedes hayan tenido con el uso de Alloy en sus proyectos.¿Sientes que te ha ayudado a diseñar un mejor modelo de dominio?¿Encontró errores en el modelo de su dominio durante la verificación?¿Lo usarías de nuevo?

Answer 1

Sí, lo he usado y es primos aleación industrial. Aleación ha sido de gran ayuda para convencerme de que mis modelos no eran tremendamente equivocada --- o, más bien, que me llevó donde estaban mal y dieron lugar a resultados tontas. Otros más herramientas específicas, como Atenea y Guttman de Song y CPSA de Ramsdell han sido más útiles en sus dominios estrechos. ¿Qué más le gustaría?

Answer 2

He usado aleación en algunos proyectos y lo he encontrado muy útil; en algunos, pero no todos los proyectos que he sido capaz de persuadir a otras personas involucradas utilizar aleación así, o al menos para trabajar con los modelos de aleación que escribí. Estos proyectos pueden ser o no ser lo que usted tiene en mente en pedir proyectos 'mundo real', pero ciertamente tuvo lugar en el marco de los trabajos del mundo real en el que.

En 2006 y 2007, que creó un modelo de la aleación parcial para el proyecto actual en ese momento de la especificación W3C XProc; por lo que pude ver, la mayoría de los miembros del grupo de trabajo nunca leyeron el documento que escribí (en http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html ); La frase "Oh, hemos cambiado esa parte de la especificación de la semana pasada, así que lo que dice el modelo ya no es relevante". Sin embargo, el papel se las arregló para convencer al editor de la especificación de que el nivel abstracto 'componente' se describe en el primer borrador de la especificación fue lamentablemente underspecified y necesitaba ser bien especificado totalmente o se ha caído. La dejó caer, con (creo) con resultados buenos para la legibilidad y facilidad de uso de la especificación.

En 2010 I hizo un modelo de la aleación de la XPath de datos 1.0 modelo , que dejó al descubierto algunos problemas en la especificación. La reacción de la mayoría de las partes interesadas (incluyendo el grupo de trabajo del W3C responsable del mantenimiento de la especificación XPath 1.0) tiene, por desgracia, no ha sido alentadora.

Un proyecto de investigación que estoy involucrado con la aleación ha utilizado para modelar la superposición MLCD Corpus, una colección de documentos de muestra e información relacionada estamos creando (hipervínculos suprimidos por la insistencia de SO); el modelo de la aleación encontró un par de errores en nuestro diseño inicial para el catálogo corpus, así que valió la pena el esfuerzo.

Y también hemos utilizado la aleación de formalizar unos trabajos de modelaje que hemos hecho de la naturaleza de la transcripción y de la extensión del tipo / distinción de contadores a la estructura del documento (para nuestro papel, aspecto para el proceso 2010 de balisage: El marcado de Conferencia). Esto se encuentra un poco fuera de la zona habitual de aleación de aplicación, ya que no tiene nada que ver con el diseño de software, pero la capacidad de la aleación para comprobar los modelos de consistencia y generar instancias ha sido muy valioso que nos muestra algunas de las consecuencias lógicas de una u otra posible axioma para nuestro modelo.

Para responder a sus preguntas específicas: sí, aleación me ha ayudado a definir los modelos de dominio más limpio, y sí, se ha encontrado errores y problemas técnicos. A menudo han sido pequeños, por las razones Daniel Jackson explica en su libro Las abstracciones de software : en primer lugar, si utiliza modelos durante el diseño, es detectar los errores temprano, cuando todo es todavía pequeña. Y, en segundo lugar (en palabras de Jackson), "En retrospectiva, la mayoría de los problemas de diseño de software son triviales."

Y continúa: "Pero si no se ocupan de ellos de frente, temas triviales tienen la mala costumbre de ser trivial." Mi experiencia con creces lo confirma. Mucho mejor para atajar estos problemas a tiempo. Así que sí, voy a utilizar la aleación de nuevo.

Answer 3

Añadiendo tardíamente a este hilo...Eunsuk Kang ha aplicado recientemente Alloy para realizar análisis de seguridad de API web para algunas empresas emergentes (después de muchas aplicaciones de Alloy en seguridad, como Apurva). análisis de OAuth y Barth et al. Análisis de mecanismos de seguridad basados ​​en navegador. para CSRF, etc.);Pamela Zave ha estado trabajando en un Impresionante análisis de Chord., un sistema de almacenamiento de igual a igual, y recientemente ha escrito una solución al algoritmo original.