Un entorno de modelado online para el model checker SPIN

Abstract

[ES] Las herramientas de verificación de modelos model checking existentes ofrecen ciertas facilidades para el análisis y comprensión del proceso de verificación de sistemas hardware y software. Este es el caso del verificador algorítmico SPIN, que permite al usuario inspeccionar detalles de la verificación formal a través de interfaces gráficas como las que ofrecen las herramientas iSpin o xSpin. Cuando el intento de verificación de una propiedad falla, dichos sistemas devuelven, a modo de contraejemplo, una traza de su ejecución que demuestra que la propiedad analizada es falsa. Sin embargo, las interfaces actuales ofrecen facilidades de inspección limitadas y su uso requiere unos conocimientos avanzados sobre el diseño de SPIN y de las diferentes configuraciones que el sistema puede soportar. El objetivo de este trabajo es desarrollar una herramienta online que, además de permitir al usuario modelar y verificar en SPIN las propiedades temporales de un sistema, soporte una exploración flexible e interactiva de las ejecuciones del model checker. El entorno estará focalizado en facilitar el aprendizaje del funcionamiento de SPIN y la comprensión de los contraejemplos generados, que pueden ser visualizados en forma gráfica. La herramienta permite al usuario interactuar con dicha representación para ayudarle a comprender las causas de los fallos de verificación. En primer lugar, se ofrece un modo de exploración global que permite a los usuarios obtener una vista general del grafo para comprender su funcionamiento a alto nivel. En segundo lugar, la herramienta soporta un modo de exploración local que permite al programador interactuar con el verificador. Además de permitir el escrutinio de los estados de la traza, el sistema desarrollado ofrece una interfaz de consulta que permite filtrar y destacar regiones específicas del grafo.

[EN] Model checking tools currently offer several facilities for the analysis and understanding of the verification process of hardware systems and software systems. This is the case of the algorithmic verifier SPIN, which allows the user to inspect specific details of the formal verification by means of a graphical interface such as the iSpin and xSpin ones. When the attempt to verify a property fails, these systems return, as a useful counterexample, an execution trace showing that the analyzed property is false. However, the current interfaces offer limited inspection facilities, and moreover, their use requires advanced knowledge of the SPIN design and of the configurations it supports The objective of this work is to develop an online tool that, besides supporting the user in modeling and verifying the temporary properties of a system using SPIN, supports the interactive exploration of the model checker executions un a flexible way. The environment is aimed at helping non-expert users learn how to use SPIN and to understand the delivered counterexamples, which can be graphically displayed. The user is allowed to interact with this graphical representation to understand the causes of a verification failure. First, a global inspection mode has been implemented that provides users with a general, high-level overview of the graph. Second, a local inspection mode facilitates the interactive use of the verifier. Besides allowing the trace states to be scrutinized, a query interface is also provided that allows the user to filter and highlight specific regions of the graph.

[CA] Les eines de verificació de models existents ofereixen unes certes facilitats per a l’anàlisi i comprensió del procés de verificació de sistemes hardware i software. Aquest és el cas del verificador algorítmic SPIN, que permet a l’usuari inspeccionar detalls de la verificació formal a través d’interfícies gràfiques com les que ofereixen les eines iSpin o xSpin. Quan l’intent de verificació d’una propietat falla, aquests sistemes retornen, a manera de contraexemple, una traça de la seua execució que demostra que la propietat analitzada és falsa. No obstant això, les interfícies actuals ofereixen facilitats d’inspecció limitades i el seu ús requereix uns coneixements avançats sobre el disseny de SPIN i de les diferents configuracions que el sistema pot suportar. L’objectiu d’aquest treball és desenvolupar una eina en línia que, a més de permetre a l’usuari modelar i verificar en SPIN les propietats temporals d’un sistema, suporte una exploració flexible i interactiva de les execucions del model checker. L’entorn estarà focalitzat a facilitar l’aprenentatge del funcionament de SPIN i la comprensió dels contraexemples generats, que poden ser visualitzats en forma gràfica. L’eina permet a l’usuari interactuar amb aquesta representació per a ajudar-lo a comprendre les causes de les fallades de verificació. En primer lloc, s’ofereix una manera d’exploració global que permeta als usuaris obtindre una vista general del graf per a comprendre el seu funcionament a alt nivell. En segon lloc, l’eina suporta una manera d’exploració local que permeta al programador interactuar amb el verificador. A més de permetre l’escrutini dels estats de la traça, el sistema desenvolupat ofereix una interfície de consulta que permet filtrar i destacar regions específiques del graf.