DownloadUser ManualBasic ExamplesReference Manual

Contents

Index

Reference Manual

Input Format: STG Format

At the beginning STG used a subset of the IF syntax, with various conventions adopted to support differences between IOSTS and IF. Now we are using our own language to described IOSTS. This allows us to have a well designed language for our formal model. For backward compatibility with files that were written with the old language, the syntax of the new one is rather the same than the old one.

General structure

A system is defined by the following components:

- the system identifier

- the set of constants

- the set of data types

- the set of synchronization gates

- the set of processes

<system>

::= system <system-id> ;
[const <constant>+]
[type <type>+]
gate <gate>+
<process>+

System Declarations

System Constants

Usual constant declaration, such as N=10, that could be used in expressions and to specify containers capacity

<constant>

::= <constant-id> = <constant-body> ;
<constant-body> ::= true
 | false
 | <integer>
 |  <constant-id>

System Types

The predefined types are the boolean type and integer type. The user can specify his on type. Each new type must have an unique name.

<type>

::= <type-id> = <type-body> ;
<type-body> ::= enum <enum-decl-list>
 | range [-]{<integer>  | <constant-id> } .. [-]{<integer>  | <constant-id> }
 | record { <field-id> : <type-id> }+ end
 | array [ [<integer>  | <ident>] ]of <type-id>

enum and array types are not implemented in the current version of STG

System Gates

Gates are used for synchronization between processes. Gates are defined by a name and the type of the messages.

<gate>

::= <gate-id> [ { ( <type-id> { <type-id> }*) }0/1 ] ;

Processes

An STG process is defined by:

- a name

- a set of input actions

- a set of output actions

- a set of internal actions

- a set of parameters

- a set of local variables

- a set of control states

- a set of transitions

The actions used in a process must have been declared as a gate of the system, except in the case of TAU which is implicitly declared.

<process>

:= process <process-id> ;
input <gate-id>+
output <gate-id>+
internal <gate-id>+ [tau]
[parameters <params>+]
[variables <vars>+]
state <state>+
transition <transition>+

Process Declarations

<params>

::= <ident-name> : <type> ;
<vars> ::= <ident-name> : <type> ;
<state> ::= init : <state-id> ;
 |  <state-id>
<state-id> ::= <ident>
 | <integer>

Transitions

Transitions is fired between two control states. A transition is composed from three parts: the guard, the action and the body.

- the guard is a boolean expression evaluated to true/false. If missing, it is considered by default to be true.

- the action is a synchronous way of communication, a rendez-vous with other processes

- the body is composed from parallel assignments to local variables

<transition>

::= from <state-id>
[ <guard> ]
[ <action> ]
[ <statement> ]
to <state-id> ;

<guard>

::= if <expression>

<action>

::= sync <action-type>
<action-type> ::= <internal-action>
 |  <other-action>
<internal-action> ::= <gate>
 |  tau
<other-action> ::= <gate> { ?  | ! } <io-list>
<io-list> ::= ( { <mess-id> { , <mess-id>}+ }* )
<mess-id> ::= <ident>
 |  <constant-id>

<statement>

::= do { <inst> {| <inst>}+ }
 |  do <inst>
<inst> ::= <expression> := <expression>

Expressions

<expression>

::= <constant-value>
 |  <name>
 |  + <expression>  | - <expression>
 |  not <expression>
 |  <expression> [ <expression> ]
 |  <expression> . <expression>
 |  <expression> -> <expression>
 |  ( <expression> )
 |  <expression> <binop> <expression>
<binop> ::= or  | and  | =  | = <>
 |  <  | <=  | >=  | >
 |  +  | -  | * | /  | %
<name> ::= IDENT

Example

Here is the source code of the Coffee Machine specification seen before.


system CoffeeMachine;

gate   
        Coin(int); 
        Cancel();
        ChooseBeverage(bool);   /* true for coffee false for tea */
        Return(int);
        Deliver(bool);

process CoffeeMachine;
input
 Coin, Cancel, ChooseBeverage;

output
 Return, Deliver;

internal
 tau;

parameters
  price         : int;          /* price of coffee/tea */ 

variables
  total         : int;          /* sum of val */
  drink         : bool;         /* variable to memorize the beverage */

state
        init : Start;
        Begin;
        Idle;
        Pay;
        Choose;
        Return;
        Delivery;
 
transition
        from Start 
          if (price > 0)
        to Begin;

        from Begin 
          sync tau
          do
                total:=0
          
        to Idle;

        from Idle
          if (coin>0)
          sync Coin?(coin)
          do   
                total:=total+coin /* accumulation of coin values */
          
        to Pay;

        from Idle
          sync Cancel?()
        to Return;
                
        from Return 
          if (moneyBack = total)
          sync Return!(moneyBack)
        to Begin;

        from Pay  
          if ((total < price) and (moneyBack = total))
          sync Return!(moneyBack)
          do 
             total := 0
          
        to Idle;

        from Pay  
        if ((total >= price) and (moneyBack = total - price))
          sync Return!(moneyBack)
         do
                total := price
          
        to Choose;

        from Choose
          if (total = price)
            sync ChooseBeverage?(drinkRequest)
          do
                drink := drinkRequest
          
        to Delivery;

        from Choose 
          sync Cancel?()
        to Return;

        from Delivery
          if (drink = drinkRequest)
          sync Deliver!(drinkRequest)
        to Begin;


process TP;
input
  ChooseBeverage, 
  Cancel;

output
  Deliver, 
  Return;

parameters
  price         : int;  /* price of coffee/tea */
  total         : int;  /* sum of val */

state
  init : Start;
  Begin; 
  Accept; 
  Reject;
        
transition

        from Start
        to Begin;

        from Begin 
          if (mBev = true)    /* COFFEE */
          sync Deliver!(mBev)
        to Accept;
 
        from Begin
          sync Cancel?()
        to Reject;

        from Begin
          if(total < price)
          sync Return!(mRemVal)
        to Reject;


process TP_pre;
input
  ChooseBeverage,Coin,
  Cancel;

output
  Deliver, 
  Return;

internal
  tau;

parameters
  price         : int;  /* price of coffee/tea */
  total         : int;  /* sum of val */

state
  init : Start;
  Begin; 
  Accept; 
  Reject;
        
transition

        from Start
        to Begin;

        from Begin 
          if (not(total = price -1))
          sync Return!(mRet)
        to Begin;  

        from Begin 
          if (total = price -1)
          sync Return!(mRet)
        to Accept;


Command-Line Interpreter Syntax

STG provides a text-based command processor that offers all of the basic operations necessary to manipulate IOSTS's for test generation. The basic syntax is based on variables, function-like operators and assignment.

Commands

Assignment: ident := iosts

Evaluates iosts and assigns the result to ident. The iosts is an expression built up from the following:
getiosts(process): Converts an STG process to an IOSTS.
iosts * iosts: Computes the product of two IOSTS's.
complete (iosts1 , iosts2): Computes an IOSTS that is iosts1 completed with respect to the actions of iosts2.
close(iosts): Computes the closure of iosts with respect to internal actions.
tobdd(iosts): Transforms iosts with its expression expressed as bdd.
reach(iosts): applies reachability analysis performed by NBAConto iosts, returns the resulting iosts.
coreach(iosts): applies coreachability analysis performed by NBACto iosts, returns the resulting iosts.
show(iosts): displays the graphical iosts in a dot window.
tojava(iosts): translates the test case into java.

Example

Here is an example of a typically sequence of commands for a test case generation:


  
     s  := getstg(CoffeeMachine);
     tp := getstg(TP); 

     tp':= complete(tp);
     p  := s*tp';
     p' := close(p);

     pbdd := tobdd(p');
     r := reach(pbdd);
     cr := coreach(r);
     ra := reach(cr);

     show(ra);
     tojava(ra)
   

Invocation

The command line syntax for STG is as follows:

stg [-options] file[.stg]

Output Formats

Each IOSTS handled by STG could be displayed textually or graphically from command interpreter of STG. Test Cases can also be translated into Java programs. See commands for more details.

Java Test Cases execution

Executing test cases is a non trivial process since it requires a run time support which depends of the application under tests. Moreover the run time support includes a solver (LUCKY) for resolving constraints in order to generate input values at run time. The run time support is written in Sjava (Synchronous Java) and resolves the synchronisation problems between the test case and the implementation. So, executing a test case against an implementation under test needs:

Instructions are given in the test execution framework which is called backend_sjava in the distribution.


F Ployette, F-X Ponscarme, May 19, 2009


DownloadUser ManualBasic ExamplesReference ManualContentsIndex