Correct Real-Time Software for Programmable Logic Controllers - Correct System Design: Recent Insights and Advances - page 340

PROGRAM PRG_FES
VAR
state

: INT := 0; (* 0:=N, 1:=T, 2:=X *)

timer : TP;

ENDVAR
IF state=0 THEN
%output:=N;
IF %input = tr THEN
state:=1;
%output:=T;
ELSIF %input = Error THEN
state:=2;
%output:=X;

ENDIF
ELSIF state=1 THEN
timer(IN:=TRUE,PT:=t#5.0s);
IF (%input = no_tr AND NOT timer.Q) THEN
state:=0;
%output:=N;
timer(IN:=FALSE,PT:=t#0.0s);
ELSIF %input = Error THEN
state:=2;
%output:=X;
timer(IN:=FALSE,PT:=t#0.0s);

ENDIF

ENDIF

Fig. 6. ST program for the lter FES

7.1 A Real-Time Logic

We use Duration Calculus (abbreviated DC), a real-time interval temporal logic
and calculus developed by Zhou Chaochen and others [37,31,15], to describe
properties of real-time systems. This choice is partly motivated by our previous
experience with this logic, and partly by the convenience with which the interval
and continuous time aspects of DC allow us to express and reason about reaction
times of components.

Syntax. Formally, the syntax of Duration Calculus distinguishes terms , duration
terms and duration formulae . Terms have a certain type and are built from

time dependent observables obs like gas or track , rigid variables x representing

time independent variables, and are closed under typed operators op :

::= obs j x j op ( )

where is a vector of terms. Terms of Boolean type are called state assertions .

We use S for a typical state assertion.