ldltools / dsl4sc

LDL-based DSL for statechart generation and verification

Summary

dsl4sc is a domain-specific language, based on LDL_f, primarily targeted at defining and verifying state transition models for event processing.

Each model in dsl4sc has the following unique characteristics:

• can include the following 3 different sort of declarations:
  • event protocol: regular pattern of acceptable event sequences
  • logical property: temporal LDL_f formula the model should meet.
  • ECA rule: triple of event, condition, and action that defines how to respond to the specified incoming event.
• has a clear semantics in terms of the LDL_f formalism.
• can be verified statically and formally against arbitrary requirements that are also defined in dsl4sc.
• can derive an executable statechart in SCXML.

Example: deuce -- Sharapova vs. Williams

Consider 2 professional tennis players, fictitiously called Sharapova and Williams, are fighting for winning a game. They are currently at deuce and either needs to win by 2 points ahead of her opponent.

To model what can happen through the game, let us start with the following protocol definition

protocol  
(sharapova; williams + williams; sharapova)*;  
(sharapova; sharapova + williams; williams);  
game ;;

This protocol defines that the game proceeds through 3 stages: (1) either takes an adavante but the other immediately evens the game, which repeats 0 or more times, and (2) either takes 2 points consecutively, and (3) the judge declares the game is taken.

Succeedingly, to define how computation proceeds through the game, we introduce a variable, state, which ranges over 0 through 2 and denotes if the games is either at deuce (0), advantaged (1), or taken (2). In terms of this varible, we define a set of formulas, as properties of the model, as follows,

variable  
state : nat(3); // nat(3) = {0, 1, 2}  
  // 0: deuce, 1: advantage with either sharapova or williams, 2: ahead by 2 points  
property  
<{state != 2}*; {state = 2}; {state = 2}> last; // state = 2  only in the last 2 steps  
state = 0 && [](last -> state = 2); // initial and final conditions  
[] !(<{state = 0}> state = 0 || <{state = 1}> state = 1); // state = 0/1 never repeats

By combining all of these, we derive a state-transition model illustrated as follows.

Once a model is defined, we can formally verify the model in various ways. For examples, we can verify the following formulas all hold.

• protocol sharapova; sharapova; game ;; : straight-win (reachable)
• property <{state = 0}; {state != 0}*> state = 2; : straight-win (reachable)
• property []<> state = 2; : liveness

Take a look at this for the detail.

You can also check out more examples if you are interested.

Installation on Docker (recommended)

• run docker build --target builder -t ldltools/ldlsat-dev . in the ldlsat directory
• run docker build -t ldltools/dsl4sc . in this directory

Installation on Debian/Ubuntu

Prerequisites

To run dsl4sc for static verification, you need the following tools.

• ocaml (v4.05 or higher. tested with 4.07.1)
  run: apt-get install ocaml
  Alternatively, you can install a particular version of the compiler using opam
  run: opam switch 4.07.1 for example
• opam (ocaml package manager)
  run: apt-get install opam
• ocaml packages: ocamlfind sedlex menhir yojson ppx_deriving ppx_deriving_yojson xml-light z3
  for each of these packages,
  run: opam install <package>
• ldlsat (v1.0.4 or higher)
  run: git clone https://github.com/ldltools/ldlsat
  build & install the tool by running make && make install in the top directory.
  By default, its library modules will be installed to /usr/local/lib/ldlsat.
• mona (v1.4)
  run: wget http://www.brics.dk/mona/download/mona-1.4-17.tar.gz
  expand the archive, and build/install the tool as is instructed.
• xqilla and xmllint
  run: apt-get install xqilla libxml2-utils

Prerequisites (optional)

To test generated SCXML files, you further need to install scxmlrun.

• scxmlrun
  run: git clone https://github.com/ldltools/scxmlrun
  build & install the tool by running make && make install in the top directory.
  By default, the binaries will be installed into /usr/local/bin.

Build

• run make && make install in the top directory
  Tools will be created and installed into /usr/local/bin.
  To change the installation directory, run make PREFIX=<prefix> install instead (default: PREFIX=/usr/local).

Installation on macOS (Darwin)

In addition to the tools listed above, you also need the following GNU tools:

• GNU common utilities
  run: brew install coreutils debianutils
• GNU sed/awk
  run: brew install gnu-sed gawk
• GNU make (v4.1 or higher)
  run: brew install remake
  and build with MAKE=remake remake instead of make

Testing

• run: make -C tests test
  run test cases using rulessat, rulesmc, and rules2scxml.