FMSE
Formal
Methods in
Software Engineering
Tools dsml Anonymous  Login

This tool exhibits the use of the executable K semantics for several DSML examples.

For now, only the xSPEM example is available. Here are some examples of commands which can be used to experiment the definition of xSPEM:

  • Kompile - compiles the K semantics into a rewrite Maude module. Select first either file from the k-generated subfolder.
  • Conformance: checks if the initial model conforms to the metamodel.
    The content of the <k> ... </k> cell from XSPEM.k must be equal to "checkConformance". (You find it at the end of the file).
  • Search: exhaustive executes the K semantics of xSPEM in order to reach a model, where all activities of some process are finished within their expected time limits, from the initial model represented in the file XSPEMModel.m.
    The content of the <k> ... </k> cell from XSPEM.k must be equal to "run". (You find it at the end of the file).

  • This command requires a Maude search command (including the surrounding quotes) as the following:
    "search [3,300] initConfig =>* < T > B:Bag  < trace > L:List [String \"reached\"(.List{K})] </ trace > </ T >"

    If you modify any file, save it first and then Kompile the definition.


Examples
Loading ...
Path : 

Input
     Params:
   StdIN:
  

Output:
@FMSE 2010-2011