For sound engineering reasons, complex systems are built out of simpler components with the correctness of the system as a whole dependent on properties of the components, rather than on precise implementation details. For properly designed systems, this structure can be exploited to reduce the work involved in checking the system. For example, suppose we can write
SYSTEM = F(C_1, C_2)
for some components C_1 and C_2, and that we wish to check
that
SPEC [= SYSTEM
and that the properties of the subcomponents can be expressed as
S_1 and S_2.
Then we can establish the result we require by three simpler tests,
namely
S_1 [= C_1 S_2 [= C_2 SPEC [= F(S_1, S_2)
since
SPEC [= F(S_1, S_2) [= F(C_1, C_2) = SYSTEM
follows by the compositional nature of the CSP operators.
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.