Invariant-driven specifications in Maude

Citations of this article
Mendeley users who have this article in their library.


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. © 2009 Elsevier B.V. All rights reserved.




Roldán, M., Durán, F., & Vallecillo, A. (2009). Invariant-driven specifications in Maude. Science of Computer Programming, 74(10), 812–835.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free