Information Technology Reference
In-Depth Information
Application
Application
Application
Application
ASS
ASS
ASS
ASS
FML
FML
FML
FML
AVI
AVI
AVI
AVI
MIL-BUS
Fig. 1.
FTC architecture
3. For data calculated by all lanes (congruent source messages) all non-faulty
lanes get the correct(ed) message,
4. For data calculated by one lane (single source messages) all non-faulty lanes
get the correct message if the originator is not faulty.
The software architecture of the FML in one lane consists of a number of
processes which communicate over a set of channels and jointly use a global
memory and a separate global buer. Figure 2 presents a simplied overview of
this architecture. Each of the main processes itself is built from smaller subpro-
cesses not shown in the gure, which communicate over local channels. For the
AVI, similar architectural concepts have been used.
3
Verication Techniques
As indicated in the introduction above, formal verication for the FTC became
manageable by an approach combining abstraction, verication of local proper-
ties by model checking, compositional reasoning and application of generic the-
ories. This approach will be described in more detail in this section. It focuses
on the correctness properties deadlock freedom, livelock freedom and correct im-
plementation of the Byzantine protocol. This verication could be performed by
analysis of the AVI and FML software sub-system only, since the ASS had been
(informally) veried with respect to deadlock/livelock freedom beforehand by
the DASA team and the application layer was not under DASA responsibility.
The verication of the Byzantine protocol could even focus on the FML alone,
since none of the other layers contribute to its implementation.
In Section 3.1, correctness properties dened on programming language level
{ in case of AVI and FML verication, OCCAM program properties { are related
to corresponding properties on formal specication language { in our case, CSP {
Search WWH ::
Custom Search