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

focusing on the aspects which were considered to be most important. This was
achieved by using application-dependent metrics : instead of trying to maximise
a standard coverage measure { such as branch coverage on specication or code
level { tests focused on maximising the coverage of dierent load proles and of
possible interleavings of exceptions with normal behaviour executions. We are
convinced that the problems listed above could not have been uncovered if test
executions had been designed to maximise a standard metrical value.
With respect to the time needed to prepare the tests, it was interesting
to observe that the preparation of formal test specications did only consume
a small fraction (less than 10%) of the full preparation time: the main eort
was spent on programming the test application layer described above and on
connecting to the MIL-STD 1553 bus driven by the frame protocol.

5.3 Future Work and Trends

Tool Support for Abstraction Techniques. Our practical experience has shown
that software code verication will always remain an important issue: instead
of modelling and verifying critical sections of the detailed design in a formal
way right from the start, formal methods are mostly applied a posteriori as a
re-engineering eort, when the code produced from informal design specica-
tions has turned out to be too buggy to be trusted without special verication
measures. As a consequence, preparing program code for formal verication will
remain an important part of the verication suite, and the eort required for
this preparation cannot be neglected. Though at rst glance it might seem at-
tractive to develop model checkers directly interpreting programming languages
in order to avoid having to perform the transformation into a formal speci-
cation language, we are convinced that the formal analysis should be kept on
the level of formal specication languages such as CSP or Petri Nets: program-
ming languages do not provide sucient support for abstraction and renement,
therefore problem simplications by abstraction would be rarely possible on that
level. As a consequence, it seems unlikely that model checkers could process com-
plex verication problems on programming language level without running into
state explosion problems. To increase the degree of automation for verication by
abstraction techniques and model checking, we advocate the following approach:

{ For dierent programming languages, front-ends transforming programs into
formal specications should be developed. To allow a high degree of automa-
tion for this step, it should not include complex abstraction techniques, but
instead lift the program code nearly in one-to-one fashion into the formal
specication language representation.
{ The formal specication language representation obtained from the code
transformation front end will in general be too complex to be managed by
a model checker. However, the new representation has the advantage to be
already in the domain of the formal language and its semantics. Now a library
of abstraction techniques structured by dierent types of verication goals
could be applied in order to simplify the formal representation of the original