| Título: | Model checking TLR guarantee formulas on infinite systems |
| Autores: | Martín, Óscar |
| Tipo de documento: | texto impreso |
| Fecha de publicación: | 2013 |
| Dimensiones: | application/pdf |
| Nota general: |
cc_by_nc info:eu-repo/semantics/openAccess |
| Idiomas: | |
| Palabras clave: | Estado = No publicado , Materia = Ciencias: Informática: Software , Materia = Ciencias: Informática: Lenguajes de programación , Tipo = Trabajo Fin de Máster |
| Resumen: |
Presentamos la implementación de un model checker para sistemas con una cantidad de estados potencialmente infinita. Se ha desarrollado sobre el lenguaje y el sistema Maude, basado en lógica de reescritura. Los sistemas que se quieran analizar también han de estar especificados como módulos Maude. El model checker funciona con estados explícitos. Así,en sistemas infinitos, no podemos esperar que la comprobación acabe en todos los casos. De hecho, solo proporciona un semi-algoritmo para validar fórmulas de garantía (o, equivalentemente, para invalidar fórmulas de seguridad). Para evitar entrar en caminos infinitos, las búsquedas siempre se llevan a cabo con profundidad acotada. La lógica temporal que usamos es TLR* (Temporal Logic of Rewriting). Esta lógica es una generalización de CTL* que usa proposiciones atómicas no solo sobre estados, sino también sobre transiciones, proporcionando así una mayor potencia expresiva. Como paso intermedio, presentamos un lenguaje de estrategias para Maude. Las fórmulas de garantía se traducen primero a expresiones de estrategia y, entonces, se hace evolucionar en paralelo al sistema y a la estrategia para buscar cómputos que satisfagan la estrategia y, por tanto, la fórmula. Se incluyen varios ejemplos para mostrar la utilidad de nuestra herramienta. En particular, se presenta un ejemplo más largo, relativo a protocolos de coherencia de caché. Las tres ideas en las que se basa este trabajo —el model checker, TLR* y el lenguaje de estrategias— son propuestas tomadas de [21]. [ABSTRACT] We present the implementation of a model checker for systems with a potentially infinite number of states. It has been developed in the rewriting-logic language and system Maude. The systems to be analysed need also be specified as Maude modules. The model checker is explicit-state, that is, not symbolic. Thus, in infinite systems, we cannot expect it to finish in every case. Indeed, it only provides a semi-decision algorithm to validate guarantee formulas (or, equivalently, to falsify safety ones). To avoid getting lost in infinite paths, search is always done within bounded depth. The temporal logic to which the formulas belong is TLR*, the Temporal Logic of Rewriting. This is a generalization of CTL* that uses not only atomic propositions on states but also on transitions, providing, in this way, a richer expressive power. As an intermediate step, a strategy language for Maude is presented. The guarantee formulas are first translated into strategy expressions and, then, the system and the strategy evolve in parallel searching for computations that satisfy the strategy and the formula. A number of examples are included, showing the usefulness of the tool. In particular, a longer example on cache coherence protocols is presented. The three ideas on which this work is based, that is, the model checker, TLR*, and the strategy language, are proposals taken from [21]. |
| En línea: | https://eprints.ucm.es/id/eprint/22647/1/master_thesis_-_two_sides_-_for_printing.pdf |
Ejemplares
| Estado |
|---|
| ningún ejemplar |
