Invariant-driven specifications in Maude |
| |
Authors: | Manuel Rold n, Francisco Dur n,Antonio Vallecillo |
| |
Affiliation: | aDpto. de Lenguajes y Ciencias de la Computación, Universidad de Málaga, Spain |
| |
Abstract: | This work presents a general mechanism for executing specifications that comply with given invariants, which may be expressed in different formalisms and logics. We exploit Maude’s reflective capabilities and its properties as a general semantic framework to provide a generic strategy that allows us to execute Maude specifications taking into account user-defined invariants. The strategy is parameterized by the invariants and by the logic in which such invariants are expressed. We experiment with different logics, providing examples for propositional logic, (finite future time) linear temporal logic and metric temporal logic. |
| |
Keywords: | Execution strategies Invariants Rewriting logic Maude Reflection |
本文献已被 ScienceDirect 等数据库收录! |