Languages Browser friendly
version
Back to Contents
This chapter contains BNF grammars of languages used in the Times tool. Note that words made of capital letters represent non-terminals.

Modeling Language
The input language of the Times tool is a network of timed automata extended with real-time tasks. Each timed automata is represented as a process instantiated from a template with the set of arguments. In addition there is a task table describing various task parameters.
  • Declarations

    Declarations can be either local or global. Local declarations relate to the different templates while global ones belong to the whole system. Every declaration must have an identifier, type and optionally an initial value. An identifier must satisfy the following regular expression:

                     ID:   [a-zA-Z]([a-zA-Z0-9_])*
    
    In this document non-terminals CLOCK, INTEGER, CHANNEL, URGENT_CHANNEL, EXTERNAL_CHANNEL and CONSTANT denote identifiers of the respective declaration types. The valid declaration types are:
       DECLARATION_TYPE:   clock
                         | int
                         | int[CONST_EXPR,CONST_EXPR]
                         | chan
                         | urgent chan
                         | extern chan
                         | const
    
    where int[...,...] is a bounded integer with lower and upper bounds defined as constant expressions. Constant expressions have the following syntax:
             CONST_EXPR:   CONST_TERM{+|-}CONST_TERM
             CONST_TERM:   CONST_UNAR{*|/}CONST_UNAR
             CONST_UNAR:   CONST_ELEM
                         | -CONST_ELEM
             CONST_ELEM:   NATURAL
                         | CONSTANT
                         | (CONSTANT_EXPR)
                NATURAL:   ([0-9])+
    
    Declaration identifiers of types clock, int and int[,] defined:
            CLOCK_ARRAY:   ID[CONST_EXPR]
          INTEGER_ARRAY:   ID[CONST_EXPR]
    
    represent arrays of clocks and integers respectively. The size of array is set equal to the value of the constant expression given in square brackets. Declaration initial value is specified as a constant expression. In case of arrays the same value is assigned to all the elements in the array.

  • Processes and Templates

    Processes are templates instantiated with the set of arguments. Process has the following attributes:

           PROCESS_NAME:   ID_WITH_SPACES
       PROCESS_TEMPLATE:   ID
      PROCESS_ARGUMENTS:   [ID(,ID)*]
    
    where ID_WITH_SPACES is an identifier with spaces allowed:
         ID_WITH_SPACES:   [a-zA-Z]([a-zA-Z0-9_ ])*
    
    Note that during process instantiation spaces in the process name are replaced with underscores. Be sure that you use underscores instead of spaces specifying properties in verifier.

    Attributes of a template include the template name and the list of formal parameters, defined as following:

          TEMPLATE_NAME:   ID
    TEMPLATE_PARAMETERS:   [TEMPLATE_PARAMETER(;TEMPLATE_PARAMETER)*]
     TEMPLATE_PARAMETER:   DECLARATION_TYPE ID
    
  • Locations

    The location attributes are:

          LOCATION_NAME:   [ID_WITH_SPACES]
          LOCATION_TASK:   [TASK_NAME]
     LOCATION_INVARIANT:   INVARIANT_LIST
    
    where:
         INVARIANT_LIST:   [INVARIANT(,INVARIANT)*]
              INVARIANT:   CLOCK{<|<=}INTEGER_EXPR
    
    and the syntax of the integer expression is:
           INTEGER_EXPR:   INTEGER_TERM{+|-}INTEGER_TERM
           INTEGER_TERM:   INTEGER_UNAR{*|/}INTEGER_UNAR
           INTEGER_UNAR:   INTEGER_ELEM
                         | -INTEGER_ELEM
           INTEGER_ELEM:   INTEGER
                         | CONSTANT
                         | (INTEGER_EXPR)
                         | (INTEGER_GUARD?INTEGER_EXPR:INTEGER_EXPR)
          INTEGER_GUARD:   INTEGER_EXPR RELATION INTEGER_EXPR
               RELATION:   !=
                         | <
                         | <=
                         | ==
                         | >=
                         | >
    
    The name of the location is an optional attribute; if not given, assigned automatically in the form Sx, where 'x' is a zero-based index. The name of the task associated with the location is also optional; if not specified, no task is released for execution when the automaton reaches given location.

  • Transitions

    The transition attributes are:

        TRANSITION_NAME:   [ID_WITH_SPACES]
       TRANSITION_GUARD:   GUARD_LIST 
        TRANSITION_SYNC:   {CHANNEL|URGENT_CHANNEL|EXTERNAL_CHANNEL}{?|!}
      TRANSITION_ASSIGN:   ASSIGNMENT_LIST
    
    where the syntax of the guard is:
             GUARD_LIST:   [GUARD(,GUARD)*]
                  GUARD:   INTEGER_GUARD
                         | CLOCK_GUARD
            CLOCK_GUARD:   CLOCK RELATION CLOCK_EXPR_WITH_INT
    CLOCK_EXPR_WITH_INT:   CLOCK ({+|-} CONST_TERM)*
                         | INTEGER_EXPR
    
    and the syntax of the assignment is:
        ASSIGNMENT_LIST:   [ASSIGNMENT(,ASSIGNMENT)*]
             ASSIGNMENT:   INTEGER := INTEGER_EXPR
                         | CLOCK := CLOCK_EXPR
                         | (INTEGER_GUARD?CLOCK_RESET)
             CLOCK_EXPR:   CLOCK ({+|-} CONST_TERM)*
                         | CONST_EXPR (should be equal to zero)
            CLOCK_RESET:   CLOCK := CONST_TERM (should be equal to zero)
    
  • Tasks

    Tasks and their parameters are defined in the task table. The name of the task should satisfy the identifier's regular expression and should be different from the channel names declared in the system.

  • Reserved Words

    The following words are reserved and cannot be used as identifiers, names of locations, transitions or tasks:

    assign, commit, externalDecl, globalDecl, graphinfo, guard, hide, imports
    init, invariant, localDecl, location, locationName, paramList, procAssign,
    process, rate, state, sync, system, systemDef, templateName, trans, int, 
    clock, chan, urgent, extern, const
    

Query Language

The syntax of the query string is as follows:

     QUERY:   A[] PROP_EXPR
            | A<> PROP_EXPR
            | E[] PROP_EXPR
            | E<> PROP_EXPR
            | PROP_EXPR -> PROP_EXPR
 PROP_EXPR:   PROPERTY
            | not PROP_EXPR
            | (PROPERTY)
            | PROP_EXPR or PROP_EXPR
            | PROP_EXPR and PROP_EXPR
            | PROP_EXPR imply PROP_EXPR
  PROPERTY:   ID.ID
            | CLOCK RELATION CLOCK_EXPR
            | INTEGER_GUARD
            | deadlock

See also:

Times Editor | Analysis

(C) 2004 DARTS, IT Dept, CS, Uppsala University, Sweden