TOOLS
C-REDUCER
C-Reducer is a tool for automatic c-reduction of object based modules for the Maude system. State space c-reductions exploit equivalence relations on states (possibly capturing system regularities) that preserve behavioral properties, and explore the induced quotient system. This is done by means of a canonizer function, which maps each state into a (non necessarily unique) canonical representative of its equivalence class. The approach is very general and supports not only traditional symmetry reductions, but also name reuse and name abstraction. The c-reducer tool implements part of the approach in Maude.
HSF-SPIN
HSF-SPIN an experimental model checker which can be seen as a directed model checking extension to Spin. It implements various heuristic estimates and algorithms in order to direct the search into a specific error situation. As consequence might be able to find shorter trails than blind depth-first search while finding errors in larger state spaces. HSF-SPIN is no more maintained but you can download () and install it and ask me for help.
CODE
MESS – Maude Ensemble Strategies Simulator
Adaptive self-assembling strategies are a crucial mechanism that allows groups of simple individual entities to act as a single complex entity exhibiting emergent behaviours. Notable examples include bacteria or insect swarms, modular and self-assembling robots and software components with dynamic coupling mechanisms. We face these kind of self-assembling strategies (for robots and not only) by (i) following our recently proposed conceptual framework for adaptation; (ii) exploiting the declarative and reflective features of the Maude language; and (iii) relying on the Maude tool framework for the analysis. MESS is our implementation of prototype self-assembling strategies to be simulated and analysed in early development phases.
Rule-Based Model-Transformation Styles
Rule-based programming has been shown to be very successful in many application areas. Two prominent examples are the specification of model transformations in model driven development approaches and the denition of structured operational semantics of formal languages. General rewriting frameworks such as Maude are exible enough to allow the programmer to adopt and mix various rule styles. The choice between styles can be biased by the programmer’s background. For instance, experts in visual formalisms might prefer graph-rewriting styles, while experts in semantics might prefer structurally inductive rules. We discussed such issues in a series of papers (1,). The code we used to evaluate the performance of different rule styles on a signicant benchmark taken from the literature on model transformation is available .