The Formal Methods & Tools group of ISTI-CNR has collaborated on a number of joint projects with ALSTOM FERROVIARIA SpA, with the objective of introducing formal specification and verification tools into the software development process of railway signalling products. The most recent collaborations have investigated the feasibility of automatic code generation, starting from a specification of the system's logic using the SCADE tool developed by Esterel Technologies. The focus has been on issues of performance of specific proprietary hardware architectures and on integration with existing software modules. These collaborations have provided the opportunity for some additional research into the introduction of diversity with the aim of improving the level of safety in the design and development process.
The introduction of diversity has been considered in those cases where an analysis of the safety measures employed to limit design faults has revealed possible weaknesses in the development process. A formal model of the (components of the) equipment is first developed using SCADE, with the added possibility of simulating the model and using model checking to verify that there are no software faults. Code is then generated by the SIL 4 validated SCADE code generator. A first possible weakness of this process has been identified in the supporting software: the underlying operating system and the compilation environment, which are not validated software components. We therefore introduced the first form of diversity at the level of the compilation of the generated code, with the aim of discovering possible faults due either to the compilation environment or to the underlying operating system (Figure 1). Two different compilation environments running on two different operating systems have been employed: the proprietary embedded platform with its dedicated compiler and a commercial compiler on the Windows platform. Parallel testing of the two versions with the same set of tests (taken from the official suite of acceptance tests) has been employed in order to reveal differences in how the generated code interfaces with the operating system or in how it is compiled.
However, even when sophisticated verification tools such as model checking are used, it cannot be guaranteed that the process of writing a formal model has faithfully captured the (informal) system requirements. Diversity can help at this stage as well, by considering two independent formal specifications. A second form of diversity can thus be introduced at the level of specification; this will impact the whole development process.
The application of this idea to the railway signalling domain has provided a direct way of conceiving diverse specifications: the relay schemas that still constitute a common language for railway signalling engineers have been used for one version, while a more 'modern' and increasingly popular notation - UML sequence diagrams have been used for the other. From these two specifications, two independent chains of verification/code generation/compilation/deployment have been implemented (Figure 2). The final comparison is made by running the set of official acceptance tests for the equipment developed on both versions.
The results of our experiments on the introduction of diversity in compilation have been encouraging, and their relatively low cost should facilitate industrial acceptance of the approach. In fact, the added cost of the first approach is limited to repeat compilation and testing on a Windows-based machine, with practically no cost for additional hardware or software resources. Moreover, replication of compilation and testing can be automated to a high extent.
In contrast, the introduction of diversity in specifications requires at least the additional effort of writing an independent specification. The overall cost of producing diverse specifications is therefore twice that of a single formal specification process. However, the higher costs of this form of diversity can be justified by lower testing and debugging costs due to the early discovery of design faults, and by the higher level of safety achieved.
Link:
http://fmt.isti.cnr.it
Please contact:
Stefania Gnesi
ISTICNR, Italy
E-mail: stefania.gnesi
isti.cnr.it
