Formal Methods for the International Space Station ISS - Correct System Design: Recent Insights and Advances - page 356

Transputer Links
Transputer Links FromOutDist[0..3]

Link

Interfaces

ToInDist[0..3]

FromOutDist[4]

ToInDist[4] ASS

Interface

Input Output

InDist2OutDist

Distributor Distributor

InDist2Voter output

Voter

ToInDist[6]

Context.recovery

ASS
Context
Manager

FromOutDist[5]

Mode

Control

Context.control

ToInDist[5]

Fig. 2. FML processes allocated in each lane.

level. Section 3.2 describes abstraction methods that have been used to make the
verication process feasible, and in Section 3.3 we sketch how properties veried
for small software components can be composed to derive the global verication
goals.

3.1 Relating OCCAM to CSP Process Properties

To motivate how properties p on OCCAM level can be related to properties
A ( p ) on (untimed) CSP level it is important to note that the concepts of traces
and refusals are dened for OCCAM processes in a straightforward way: traces
are sequences of OCCAM channel events, a refusal after a trace s is a set of
OCCAM channels which are blocked since either one or both communication
partners are not ready to pass messages along them. Therefore the concepts of
trace renement and failures renement may be applied on OCCAM level as
well. We can even investigate trace and failures renement relations between
a CSP process Q andanOCCAMprocess P , if the alphabet of Q is dened
by the set of OCCAM channels with identical channel alphabets (on OCCAM
level you would call the channel alphabets \protocols"). Furthermore, it was
ensured in the AVI and FML OCCAM code that every loop has a constant
nite upper bound. As a consequence, divergence could only occur by execution
of unbounded chains of channel communications over cycles of internal channels
without any external interface communication interleaved. This means that the