Herramienta simple de verificación de modelos

Question

¿Existe una herramienta simple de Comprobador de modelos? Estoy planeando implementar una herramienta de verificación de modelos que analizará el código de algunas de las propiedades predefinidas.

Answer 1

Una herramienta importante es SPIN , con el idioma Promela. Si usa LaTeX, también hay TLA + .

Estos no analizarán su código, pero le permitirán expresar un modelo para sus suposiciones y transiciones de estado, y luego analizarán los estados no válidos. En otras palabras, detectarán problemas en su modelo, no la implementación de su modelo.

He visto una demostración de Goanna , pero no lo hago ' No sé si está disponible (comercial o de otro tipo); esto tiene la ventaja de analizar realmente su código fuente.

Solo mirando su pregunta, y los comentarios en su pregunta nuevamente, parece que realmente debería leer algo de la literatura primero. Quizás, The Spin Model Checker , o Especificación de sistemas (descargable desde sitio web de Leslie Lamport ). Debe replantear su problema para no intentar resolver el problema de detención.

Answer 2

CBMC es una herramienta simple, soy consciente de eso en realidad opera en código. La verificación de modelos en general es un campo muy investigado, pero como la gente ya ha comentado, esta amplitud hace que sea difícil sugerir algo con la información proporcionada. Hay miles de solucionadores SAT, herramientas formales para la verificación de máquinas HDL / estado y muchos analizadores comerciales de fuentes estáticas.

En cualquier caso, CBMC es una buena herramienta, pero no confíe en mi palabra; Ed Clarke, el principal miembro de la facultad detrás de este trabajo, ganó el Premio Turing este año ;-)