¿Cuál es su experiencia con la verificación de modelos de software? [cerrado]

Question

• ¿Para qué tipo de aplicaciones ha utilizado verificación de modelos para?
• ¿Qué herramienta de verificación de modelos usaste?
• ¿Cómo resumiría su experiencia con la técnica, específicamente al evaluar su efectividad en la entrega de software de mayor calidad?

En el curso de mis estudios, tuve la oportunidad de usar Spin , y surgió mi curiosidad acerca de cuánto está sucediendo la verificación real del modelo y cuánto valor están obteniendo las organizaciones. En mi experiencia laboral, he trabajado en aplicaciones comerciales, donde (naturalmente) no hay consideración de aplicar la verificación formal a la lógica. Realmente me gustaría aprender sobre la experiencia de comprobación del modelo de personas SO y sus pensamientos sobre el tema. ¿La verificación de modelos se convertirá alguna vez en una práctica de desarrollo más utilizada que deberíamos tener en nuestro kit de herramientas?

Answer 1

Acabo de terminar una clase sobre verificación de modelos y las grandes herramientas que usamos fueron Spin y SMV . Terminamos usándolos para verificar propiedades en problemas comunes de sincronización, y encontré que SMV es un poco más fácil de usar.

Aunque estas herramientas fueron divertidas de usar, creo que realmente brillan cuando las combina con algo que impone dinámicamente restricciones en su programa (por lo que es un poco más fácil verificar cosas 'útiles' sobre su programa). Terminamos tomando el framework de WebFlow de Spring , que utiliza XML para escribir un archivo tipo máquina de estado que especifica qué páginas web pueden realizar la transición a otras y usar SMV para poder realizar la verificación en dichas aplicaciones ( enchufe descarado aquí ).

Para responder a su última pregunta, creo que es definitivamente útil tener una verificación de modelos, pero me inclino más por utilizar las pruebas de unidades como una técnica que me hace sentir cómodo al entregar mi producto final.

Answer 2

Hemos utilizado varios verificadores de modelos en enseñanza, diseño de sistemas y desarrollo de sistemas. Nuestra caja de herramientas incluye SPIN, UPPAL, Java Pathfinder, PVS y Bogor. Cada uno tiene sus fortalezas y debilidades. Todos encuentran problemas con modelos que son simplemente imposibles de descubrir para los seres humanos. Su facilidad de uso varía, aunque la mayoría son pulsadores automatizados.

¿Cuándo usar un verificador de modelos? Diría que cada vez que esté describiendo un modelo que debe tener (o no tener) propiedades particulares y es más grande que un puñado de conceptos. Cualquiera que piense que puede describir y entender algo más grande o más complejo se está engañando a sí mismo.

Answer 3

  

¿Para qué tipo de aplicaciones ha utilizado la verificación de modelos?

Utilizamos el verificador de modelos Java Path Finder para verificar algunas propiedades de seguridad (interbloqueo, condición de carrera) y temporales (usando la lógica temporal lineal para especificarlas). Admite aserciones clásicas (como NotNull) en Java (bytecode), es para la verificación del modelo de programa.

  

¿Qué herramienta de verificación de modelos usaste?

Utilizamos Buscador de rutas de Java (con fines académicos). Es un software de código abierto desarrollado inicialmente por la NASA.

  

¿Cómo resumiría su experiencia con la técnica, específicamente al evaluar su efectividad en la entrega de software de mayor calidad?

La verificación del modelo del programa tiene un problema importante con la explosión del espacio de estado (uso de memoria y disco). Pero hay una amplia variedad de técnicas para reducir los problemas, para manejar grandes artefactos, como la reducción parcial de pedidos, la abstracción, la reducción de simetría, etc.

Answer 4

Usé SPIN para encontrar un problema de concurrencia en el software PLC. Encontró una condición de carrera insospechada que habría sido muy difícil de encontrar por inspección o prueba.

Por cierto, ¿hay un " SPIN para Dummies " ¿libro? Tuve que aprenderlo de " El verificador de modelos SPIN " Libro y varios tutoriales en línea.

Answer 5

He realizado algunas investigaciones sobre ese tema durante mi tiempo en la universidad, ampliando el Exploración del estado Verificador de modelo de ensamblaje .

Utilizamos una máquina virtual para recorrer todas y cada una de las rutas / estados posibles del programa, utilizando A * y algunas heurísticas, según el tipo de error (punto muerto, errores de E / S, ...)

Se inspiró en Java Pathfinder y funcionó con código C ++. (Todo lo que GCC podría compilar)

Pero en nuestras experiencias, este tipo de tecnología no se utilizará pronto en aplicaciones comerciales, debido a problemas relacionados con la GUI, el trabajo necesario para crear un entorno de prueba inicial y los enormes requisitos de hardware. (Necesitas mucha RAM y espacio en disco, debido al gigantesco espacio de estado)