Due to the high complexity of modern software systems, a complete formal verification can hardly be accomplished in general. For safety-critical systems, however, it may be required to prove the validity of at least some relevant application-specific properties.
Software components are self-contained units with a well-defined interface which can be assembled to a complete system. The advantage of such an approach is the possibility of re-using components which may also be provided by external suppliers. Both the re-usability of proven components and the higher clarity of component-based structures contribute to simplify the problem of handling high system complexity.
Furthermore, such a component-based concept helps reducing the verification effort. For this purpose, verified component properties are first to be documented; on their basis and by means of an overall system model, target application properties may be derived. In case envisaged system properties are not directly derivable from documented component properties, additional component properties may be required and, if necessary, enforced by means of component wrappers.
Initially, the project examined available component and system description languages. For this purpose, a number of Architectural Description Languages (ADLs) were analysed and comparatively evaluated, especially in the light of their expressiveness concerning actors and sensors (as well as their interaction) to be controlled by components. In particular, it was investigated whether the languages considered allow a system-independent component description.
A formal model for describing component behaviour was successively developed, allowing to be mapped to a Kripke structure by simple transformation. This yields a formal basis with deduction rules for the derivation of system properties from component properties.
On this basis it was examined to which extent the compliance of relative time requirements may be checked by use of a model checker. Such requirements may concern a. o. the consistency of operational calls and component states, as well as the order of given operational calls. For this purpose a technique has been developed for determining for each relative time requirement a corresponding set of statements in Computation Tree Logic (CTL), which have to be successively checked for validity. This approach allows inferring already during component integration under which specific conditions given relative time requirements may be violated at runtime.
Sub-project A: Evaluation and Comparison of Techniques for Analysing the Explanatory Power of Model Checking Proofs
Within this sub-project a number of techniques for analysing the significance of model checking proofs were examined (a. o. vacuity detection, model checking coverage, witness generation). The techniques identified were compared, especially in terms of their underlying temporal logic and of the explanatory power of the information derived, a. o. for the purpose of fault detection. In order to ease the application of the techniques examined a tool was developed implementing a selection of the approaches considered on the basis of the model checker NuSMV as well as providing a visualisation of the results.
Next steps: Future work will focus on the problem of deducing system properties from component properties and, where required, of identifying additional component properties enabling to infer conclusions on the validity of the system properties envisaged.