Invariant-driven specifications in Maude

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

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

Cite

CITATION STYLE

APA

Roldán, M., Durán, F., & Vallecillo, A. (2009). Invariant-driven specifications in Maude. Science of Computer Programming, 74(10), 812–835. https://doi.org/10.1016/j.scico.2009.03.003

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