Technical topic: SDL2IF/OBS2IF

From TASTE
Jump to: navigation, search

Introduction

sdl2if translates SDL processes representing the behavior of TASTE functions or TASTE observers into respectively IF processes or IF observers.

sdl2if is developed as a back-end of OpenGEODE, from which it re-uses the SDL parser and the AST representation. It is developed in Python 3.x and uses single-dispatch generic functions (functools/singledispatch) to structure the translation.

Usage

sdl2if is invoked as follows

 $ sdl2if [--output-dir dir] file1.pr [ ... file_n.pr]

and produces a unique .if file containing the translation of the SDL process defined in file1.pr (... file_n.pr) as an IF process. The file will be created in the output-directory if specified, else in the current working directory. The name of the .if file is the lowercase name of the SDL process.


Key Features

  • supports a significant part of SDL including expressions on data variables with ASN.1 types, hierarchical and parallel states, inner procedures, task for loops, decisions, floating labels, etc
  • preserves the structure of the input model, that is, each SDL concept is mapped 1-to-1 into an equivalent IF concept, whenever possible - e.g., variables, hierarchical states, transitions, actions - and therefore facilitates the inspection and the understanding of the generated code
  • preserves the operational semantics, that is, traceability between executions in TASTE and executions in IF, as much as possible
  • generates IF processes slightly optimized for exhaustive model-checking, by limiting the increase of the state vector and/or state space due to auxiliary variables
  • in observers, supports success, error and ignore states
  • in observers, supports both simple and generic input/output transition triggers; the generic triggers are expanded at translation using auto-generated -Event types in observer.asn
  • in observers, translates SDL timers as IF clocks and allow checking properties dealing explicitly with real time


Known Limitations

  • no entry/exit procedures in hierarchical state machines
  • no mutually recursive inner procedures
  • no 'NEXTSTATE -' in transitions from / with floating labels
  • restricted input/output event triggers and/or system state expressions in observers


Examples

An SDL process

Memoryscrub.png

process memoryscrub(1);

var running boolean := true public;
var sender pid := nil;
var par EnableDisable public;

state start #start ;
  task running := false;
    nextstate disabled;
endstate;

state disabled;
  input memoryscrub_enableordisable (par, sender);
    nextstate u_decision_1;
endstate;

state u_decision_1 #unstable ;
  provided (par = EnableDisable_scrubon);
    task running := false;
    nextstate enabled;
  provided (par = EnableDisable_scruboff);
    task running := false;
    nextstate disabled;
endstate;

state enabled;
  input memoryscrub_enableordisable (par, sender);
    nextstate u_decision_2;
  provided (not running) and true;
    task running := true;
    informal "input_none";
    // writeln ;
    task running := false;
    nextstate enabled;
endstate;

state u_decision_2 #unstable ;
  provided (par = EnableDisable_scrubon);
    task running := false;
    nextstate enabled;
  provided (par = EnableDisable_scruboff);
    task running := false;
    nextstate disabled;
endstate;

endprocess;

An SDL observer

Droppick.png

intrusive observer droppick;

var running boolean := true public;
var sender pid := nil;
var aux_signal t_if_signal;
var cmd Roboticarmstatus public;

state start #start ;
  task running := false;
    nextstate wait;
endstate;

state checkdrop;
  provided (not running);
    match input rarmcontrol_roboticarm_request (cmd, sender) in {rarmcontrol}0;
    task running := true;
    nextstate u_decision_1;
endstate;

state u_decision_1 #unstable ;
  provided (cmd.predicate = RoboticarmPred_roboticarm_picking);
    task running := false;
    nextstate error;
  provided (cmd.predicate = RoboticarmPred_roboticarm_dropping);
    task running := false;
    nextstate wait;
  provided not ((cmd.predicate = RoboticarmPred_roboticarm_picking) or (cmd.predicate = RoboticarmPred_roboticarm_dropping));
    task running := false;
    nextstate checkdrop;
endstate;

state error #error ;
endstate;

state wait;
  provided (not running);
    match input rarmcontrol_roboticarm_request (cmd, sender) in {rarmcontrol}0;
    task running := true;
    nextstate u_decision_2;
endstate;

state u_decision_2 #unstable ;
  provided (cmd.predicate = RoboticarmPred_roboticarm_picking);
    task running := false;
    nextstate checkdrop;
  provided (cmd.predicate = RoboticarmPred_roboticarm_dropping);
    task running := false;
    nextstate error;
  provided not ((cmd.predicate = RoboticarmPred_roboticarm_picking) or (cmd.predicate = RoboticarmPred_roboticarm_dropping));
    task running := false;
    nextstate wait;
endstate;

endobserver;

Transformation Rules

Declarations

ClipCapIt-220721-085615.PNG


State Machines

States

ClipCapIt-220721-085658.PNG


Labels

ClipCapIt-220721-085736.PNG

Inner Procedures

ClipCapIt-220721-085907.PNG

Actions

Input

ClipCapIt-220721-090403.PNG

Continuous Signal

ClipCapIt-220721-090434.PNG

Task

ClipCapIt-220721-090515.PNG
ClipCapIt-220721-090551.PNG

Output

ClipCapIt-220721-090622.PNG

Procedure Call: Inner SDL Procedure

ClipCapIt-220721-090722.PNG

Procedure Call: External Protected Interfaces (C Implementation)

ClipCapIt-220721-090814.PNG

Writeln

ClipCapIt-220721-090855.PNG

Set, Reset

ClipCapIt-220721-090930.PNG

Decision

ClipCapIt-220721-091010.PNG

Terminator

ClipCapIt-220721-091043.PNG

Comment

ClipCapIt-220721-091105.PNG

Expressions

Constants

ClipCapIt-220721-091145.PNG

Binary Operators

ClipCapIt-220721-091234.PNG

Conditional Expressions

ClipCapIt-220721-091416.PNG

Math Operators

ClipCapIt-220721-091457.PNG

Sequence/Of Operators

ClipCapIt-220721-091552.PNG

Choice Operators

ClipCapIt-220721-091634.PNG

Other Operators

ClipCapIt-220721-091747.PNG

Implementation

The sdl2if implementation is located under the Taste / IF Model Checking git repository within the modules/sdl2if directory.

The tool entry point is defined within sdl2if.py and the core implementation is located within IfGenerator.py. At top level, sdl2if uses the opengeode parser to construct the AST of the input SDL files, then it proceeds with the transformation on the first SDL process, by doing:

ast, warnings, errors = opengeode.parse(options.files)
IfGenerator.generate(ast.processes[0], output_dir=options.output_dir)

The implementation of the model transformation is recursive on the AST representation of the SDL process as constructed by opengeode. Single-dispatch generic functions are used to handle the various AST objects, and produce (fragments of) the IF process(es) and related IF definitions, as summarized below:

Single-dispatch generic transformation functions
Function ogAST Classes
tr_process ogAST.Process, ogAST.Procedure
tr_state_machine ogAST.Process, ogAST.CompositeState, ogAST.Procedure
tr_state ogAST.Process, ogAST.CompositeState, ogAST.Procedure, ogAST.FloatingLabel
tr_transition ogAST.Input, ogAST.ContinuousSignal, ogAST.Transition, ogAST.Terminator
tr_action ogAST.Input, ogAST.ContinuousSignal, ogAST.Label, ogAST.Task*, ogAST.Output, ogAST.ProcedureCall, ogAST.Decision
tr_expression ogAST.Expr*, ogAST.Prim*

The resulting IF process(es) and related definitions are represented using dedicated data structures. That is, in a first step, an IF model is progressively constructed while traversing the AST, then, in a second step, the IF model is written into a textual .if file.

The implementation provides the classes IfSignal, IfVariable, IfGuard, IfAction, IfTransition, IfState, IfProcess to represents structurally the corresponding IF concepts. In addition, the class IfWeb allows to store an IF state machine fragment with potentially any number of pending entry and exit transitions and provides specific methods to glue such fragments into bigger ones, ultimately leading to complete state machines.

Finally, the implementation relies on several helper functions with dedicated functionalities, the most important being summarized in the table below:

Helper functions
Functions Provided Functionality
ctxt_* access information about the transformation context
if_*_name get names for different concepts at IF level
idx_* unique indexing of AST objects
auxvar_* handling auxiliary variables
forloopvar_* handling ogAST.TaskForLoop variables
inosig_* output forwarding from inner procedures
is_input_*, *_discard_* auto-completion with discard transitions
*_observer_*, *_match_* observer specific access and/or transformation

Extensions

In general, extending the transformation for a new AST concept would require the implementation of the corresponding transformation function(s), in the appropriate category(-ies). Nevertheless, extending the transformation with a new predefined call expression operator can be simpler:

  • if the new operator is going to be supported in IF through a (homonym) abstract function (with extern C implementation) then, it would be enough to extend the list of predefined operator names defined within tr_expression // _prim_call so that to include the new operator name,
  • otherwise, if the new operator is going to be supported by built-in expansion into an IF expression then, this operator shall be handled specifically within the tr_expression // _prim_call, in a similar way as the operators present, exists, etc.