Syntax and Semantics

In order to provide the required input for the framework, we have to create a text file with the following structure.

[commandchars=\\\{\},
       numbers=left,numbersep=3pt, fontsize=\footnotesize,
       xleftmargin=10mm,xrightmargin=10mm]
{\bf  \it program} programName

{\bf  \it  var }
{\bf  \it bool} var1; 
{\bf  \it int} var2=0, {\bf  \it domain }  0 .. 1;



// The structure of process pName
{\bf  \it  process  } pName
{\bf  \it  begin } 
  guard1 ->  statement1;
    | 
  guard2 ->  statement2;
    |
    .
    .
    .
    |
  guardk ->  statementk;

{\bf  \it read}  list of variables that pName can read;
{\bf  \it write} list of variables that pName can write;
{\bf  \it end} 

// Faults are represented as a process.

{\bf  \it fault } faultName
{\bf  \it  begin}
  guard1 ->  statement1,
    |
    .
    .
    .
    |
  guardM ->  statementM,
{\bf  \it end}

// The invariant of the program.
{\bf  \it invariant }
  A state predicate S in terms of program variables.

// The specification of the program is specified in three parts starting 
// with {\it specification} keyword.

{\bf  \it specification}

// The {\it destination} part identifies a set of states that every 
// transition that reaches it violates safety.

{\bf  \it destination }

  A state predicate that identifies a set of states which the program 
  should not reach.

// The {\it relation} part identifies a set of transitions that violate safety.

{\bf  \it relation }

  A state predicate that identifies a set of transitions that 
  the program is not allowed to execute.
 
// The {\it init} section is used for specifying the initial states.

{\bf  \it init }
// Each initial state is specified using the {\it state} keyword.

{\bf  \it state }

{\bf  \it state }

In the rest of this section, we describe each part of the input file, respectively (cf. Appendix for the grammar of the input language). In the structure of the input file, we have shown all the keywords in italics. Also, in this section, we represent keywords in italics form. The input text file consists of the following sections: program Name, variable declaration, process specification, fault specification, the invariant, the specification, and the initial states. We show the structure of the program as the following BNF statement.

  ( ProgramDeclarator() ) 

		  ( VariableDeclarator() ) 

		  ( ProcessDeclarator() )+ 

		   (FaultDeclarator()) 

		   (Invariant()) 

		  (Specification())

		  (Initialization())

The syntax of program the ProgramDeclarator is as follows.

  ProgramDeclarator() :  "program"  Name() 

After the program keyword, we write a user-defined name. In the variable declaration section, we have to specify all program variables. Each variable should be declared as follows.

  varType varName [= initValue], domain lb .. ub; 

In this version, we only provide Boolean (denoted bool) and integer (denoted int) types for variables. Also, we have the option to initialize the variables in the declaration. For integer variables, we need to identify the domain of each variable. Since we assume that the domain of each variable is finite, we specify the domain of each integer variable as a closed interval from a lower bound to an upper bound (denoted lowerbound .. upperbound). To specify a process, we use the following syntax.

  process processName begin processBody read readRestriction; 

		 write writeRestrictions; end 

The processName is an arbitrary identifier that becomes the name of the process. The syntax of the processBody consists of a set of actions. Each action consists of a guard and a statement (cf. the Appendix for the detail grammar). After the specification of program actions, we have to identify the read/write restrictions imposed on the process. The read keyword should follow by a list of variables that the process is allowed to read, and the write keyword should follow by a list of variables that the process is allowed to write. In this list of variables, each variable is separated from other variables by a comma. The program may contain more than one process. Thus, we use the above syntax to specify all the program processes. We specify faults similar to process specification. The only difference is that we specify no read (respectively, write) restrictions for faults. Thus, we again use guarded commands to specify faults in the body of a process structure. We represent the invariant of a program as a set of states. Thus, in the input file, we have to write a Boolean condition in the invariant section that identifies the set of states that belong to the invariant. The syntax of this section is as follows.

  invariant  BooleanExpression() 

In order to represent the safety specification of the fault-intolerant program, we use the following structure.

  specification ( destination  BooleanExpression() | noDestination ) 

		(relation BooleanExpression()   | noRelation ) 

The keyword specification shows the start of the specification section. The destination section is followed by a Boolean expression that represents a set of states where the program should not reach. The relation keyword is followed by a Boolean condition that represents a set of transitions that the program should not execute. If, for a particular problem, the specification does not need a destination (respectively, relation) section then we just write the keyword noDestination (respectively, noRelation). Note that the Boolean expressions that we specify in the specification section are in terms of the modified names of the program variables. We attach the letter d to the name of the variables that are involved in the Boolean expression that we write in the destination section. Also, since the relation section identifies a set of safety-violating transitions in the state space of the program, we need to identify the value of different variables at the source and the destination of the safety-violating transitions. Thus, in the Boolean expression that follows the keyword relation, we attach the letter s (respectively, the letter d) to variables where they represent a value at the source (respectively, destination) state. In order to illustrate this issue, we present a concrete example in the next section.