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

2 Logic-Based Approach

How can dierent notations and formal methods for real-time systems be tied
together ? We argue here that a logic-based approach helps to clarify the concepts
involved and is useful for proving properties of the systems.
Our basic assumption is that a real-time system can be described by a set of
time dependent observables obs which are functions

obs Time −! D obs

:

where Time is a continuous time domain , here the nonnegative real numbers

0 ,and

D obs is the type or data domain of obs . For example, a gas valve might

be described using a Boolean valued observable

gas : Time −! f 0 ; 1 g

indicating whether gas is present or not [30], a railway track by an observable

track Time −! f empty; appr; crossg

:

where means that it is crossing

the gate [29], and the current communication trace of a reactive system by an
observable

appr means a train is approaching and cross

Time −! Comm tr :

Comm denotes the set of all nite sequences over a set where of possible

communications [34,35]. Thus depending on the choice of observables we can
describe a real-time system at various levels of abstraction.
To describe properties of observables we use predicates of a suitable logic. As
a consequence of such a logic-based approach the semantics of dierent syntactic
descriptions of a real-time system can be given in terms of predicates in the same
logic. The advantage is that then correctness can be expressed simply as logic
implication between predicates. For any two syntactic descriptions

Comm

term 1 and

term 2 we write

term 1 V term 2

if the semantic predicate associated with term 1 logically implies the semantic

predicate associated with term 2 . Conceptually, this means that term 1 satises

or renes all the properties of term 2 , i.e. is correct w.r.t. term 2 .

For example, if term 2 is a requirement req and term 1 is a design specication

spec then

spec req

expresses that spec correctly renes req , and if term 2 is a specication spec and

term 1 is a program prog then

prog spec