MISSCEL – Maude Interpreter and Simulator for SCEL

Maude-based modelling, state-space generation, simulation, qualitative and quantitative analysis of adaptive systems.

Summary

SCEL is a kernel formal language developed in the European project ASCENS to model adaptive systems. It brings together programming abstractions to address aggregations (how components interact to form ensembles), behaviours (how components progress) and knowledge manipulation, according to specific policies. This allows to program interaction, adaptation and self- and context-awareness.

SCEL comes with solid semantics foundations laying the basis for formal reasoning. MISSCEL, a faithful rewriting logic-based implementation of SCEL’s operational semantics, is a first step in this direction. MISSCEL is written in Maude, an instantiation of rewriting logic which allows to execute rewrite theories. What we obtain is thus an executable operational semantics for SCEL, that is an interpreter. By resorting to external schedulers we obtain probabilistic simulations, enabling statistical analysis.

Given a SCEL specification, thanks to MISSCEL it is possible to exploit the rich Maude toolset to perform:

  • automatic state-space generation;
  • qualitative analysis via Maude’s invariant and LTL model checkers;
  • debugging via animated probabilistic simulations;
  • quantitative analysis via the recently proposed MultiVeStA, a distributed statistical analyzer extending VeStA and PVeStA.

Publications

  1. Lenz Belzner, Rocco De Nicola, Andrea Vandin, Reasoning (on) Service Component Ensembles in Rewriting Logic, at Specification, Algebra and Software.

Talks

  1. Reasoning on Reasoning Robots, ASCENS General Meeting, July 3-5 2013, Lausanne.
  2. Maude .:° ASCENS, ASCENS General Meeting, March 4, 2011, Pisa.

Download

The implementation of simulator and of some simple examples can be downloaded here

Requirements

Usage

The archive contains the Maude implementation of the interpreter. Note, that also a Java wrapper exists allowing to access the interpreter programmatically, and enabling probabilistic simulations, and thus statistical analysis by resorting to the integration with the distributed statistical analyser MultiVeStA. It also allows to build the transition matrix among the states of the SCEL specification. For more details about this, please do not hesitate to contact us at the contacts provided below.

In order to use the command-line interpreter it is necessary to launch Maude, and to load the file containing the SCEL specification. Every file containing a SCEL has to import the root file “MISSCEL_TS.maude” (in Maude notation: in pathToFile/MISSCEL_TS.maude).

The root file already comes with some trivial SCEL specifications, thus we can just load it:

cd misscel
maude MISSCEL_TS.maude

Now, consider the predefined SCEL specification named “testSystem25” defined as:

eq testSystem25
 = SC( I(tId('SCId)),
       K((< tId('SCId) ; av(id('SC1)) >, < av(0) >, < av(1) >, < av(2) >)),
       Pi(INTERLEAVING-INTERACTION-PREDICATE),
       P((get(< ?x('y) >)@ self) . (put(< tId('ValueReceived) ; x('y) >)@ self) . nilP)
      ) .

This is a SCEL component having the tuple identifier “tId(‘SCId)” in its interface I. Interfaces allow SCEL components to “publish” part of their knowledge to other components. Note that a tuple identifier is a sort of pointer used to refer to a tuple in its knowledge.

The component has four tuples in its knowledge K: the first one contains its name (id(‘SC1)), while the other three contain the values “1”, “2” and “3”. Note that tuple identifiers are not mandatory, however only tuples with identifier can be exposed by the interface. Moreover, actual values are enclosed in the contructor “av”, while variables in the contructor “x”.

Then, Pi specifies that the component has the default policy, which allows processes of the component to evolve in a pure interleaving fashion only, and authorizes every access to and from other components.

Finally, the process contained in P specifies the behaviour of the component: it first get a tuple containing only a value from its knowledge (which is thus non-determinisically chosen among the three mentioned ones). Then, the value of the tuple is stored back in K, in a tuple having identifier “ValueReceived”.

For example, we can ask Maude to generate the state-space of “testSystem25” :

search in TEST-STATESPACEGENERATION : { testSystem25 } =>* X:ClosedSystem .

Obtaining:

search in TEST-STATESPACEGENERATION : {testSystem25} =>* X:ClosedSystem .

Solution 1 (state 0)
states: 1  rewrites: 32 in 0ms cpu (0ms real) (~ rewrites/second)
X:ClosedSystem --> {

SC(I(tId('SCId)),
   K((< av(0) >, < av(1) >, < av(2) >, < tId('SCId) ; av(id('SC1)) >)),
   Pi(INTERLEAVING-INTERACTION-PREDICATE),
   P(get(< ?x('y) >)@ self .
     put(< tId('ValueReceived) ; x('y) >)@ self))
}

Solution 2 (state 1)
states: 2  rewrites: 109 in 0ms cpu (0ms real) (~ rewrites/second)
X:ClosedSystem --> {

SC(I(tId('SCId)),
   K((< av(1) >, < av(2) >, < tId('SCId) ; av(id('SC1)) >)),
   Pi(INTERLEAVING-INTERACTION-PREDICATE),
   P(put(< tId('ValueReceived) ; av(0) >)@ self))
}

Solution 3 (state 2)
states: 3  rewrites: 157 in 0ms cpu (1ms real) (~ rewrites/second)
X:ClosedSystem --> {

SC(I(tId('SCId)),
   K((< av(0) >, < av(2) >, < tId('SCId) ; av(id('SC1)) >)),
   Pi(INTERLEAVING-INTERACTION-PREDICATE),
   P(put(< tId('ValueReceived) ; av(1) >)@ self))
}

Solution 4 (state 3)
states: 4  rewrites: 205 in 0ms cpu (1ms real) (~ rewrites/second)
X:ClosedSystem --> {

SC(I(tId('SCId)),
   K((< av(0) >, < av(1) >, < tId('SCId) ; av(id('SC1)) >)),
   Pi(INTERLEAVING-INTERACTION-PREDICATE),
   P(put(< tId('ValueReceived) ; av(2) >)@ self))
}

Solution 5 (state 4)
states: 5  rewrites: 263 in 0ms cpu (1ms real) (~ rewrites/second)
X:ClosedSystem --> {

SC(I(tId('SCId)),
   K((< av(1) >, < av(2) >, < tId('SCId) ; av(id('SC1)) >, < tId('ValueReceived) ; av(0) >)),
   Pi(INTERLEAVING-INTERACTION-PREDICATE),
   P(nilP))
}

Solution 6 (state 5)
states: 6  rewrites: 315 in 0ms cpu (2ms real) (~ rewrites/second)
X:ClosedSystem --> {

SC(I(tId('SCId)),
   K((< av(0) >, < av(2) >, < tId('SCId) ; av(id('SC1)) >, < tId('ValueReceived) ; av(1) >)),
   Pi(INTERLEAVING-INTERACTION-PREDICATE),
   P(nilP))
}

Solution 7 (state 6)
states: 7  rewrites: 367 in 0ms cpu (2ms real) (~ rewrites/second)
X:ClosedSystem --> {

SC(I(tId('SCId)),
   K((< av(0) >, < av(1) >, < tId('SCId) ; av(id('SC1)) >, < tId('ValueReceived) ; av(2) >)),
   Pi(INTERLEAVING-INTERACTION-PREDICATE),
   P(nilP))
}

No more solutions.
states: 7  rewrites: 406 in 0ms cpu (2ms real) (~ rewrites/second)

Authors

Andrea Vandin.

Acknowledgments

Our work is developed within and supported by the European Integrated Project 257414 ASCENS.

About

For suggestions, remarks, bugs, or to have more information about the usage of MISSCEL, of its Java wrapper, and of its integration with the distributed statistical analyser MultiVeStA, please do not hesitate to contact:

  • andrea.vandin@imtlucca.it