by Sergio Montenegro
For safety-critical applications, special measures are required to avoid software errors in crucial control systems. Where extremely high safety requirements must be met, the use of formal methods is recommended. And, in future, their use in such application fields will actually be called for, the 'classical' development of safety-critical systems being too error-prone. These ever-increasing requirements cause high costs. Thus, an adequate tool support based on formal notations together with an appropriate development method must be designed. The integrated project ESPRESS (Engineering of Safety-Critical Embedded Systems), funded by the German Federal Ministry for Education, Science, Research and Technology and coordinated by Daimler-Benz Research, is designed to fill this gap.
The ESPRESS project seeks to broadly improve productivity when developing complex safety-critical embedded systems and to enhance system reliability itself. The main concern here is to provide a uniform, methodical, tool-supported software platform. The suitability and practical orientation of such a platform will be ensured by accompanying tests and the stepwise improvement of components, concepts and the corresponding tools. This will be achieved by conducting practically relevant industrial case studies, based on real applications of the project partners in the areas of electronic automobile and traffic systems.
Overall Methodology
The envisaged methodology for developing safety-critical embedded systems may be outlined as follows (see figure): The essentials are an explicit separation of functional and safety requirements, the combination of graphical (Statecharts) and formal (Z) techniques for specification, the (semi-) automated verification, code generation and the execution of systematic tests.
Engineering of safety-critical embedded systems.
The successful application of formal techniques calls for the explicit formalization of background knowledge about the application domain -knowledge that is generally only available in the experts' heads. But it is only with such knowledge, taking into account real-time and distributedness aspects, that the relevant physicotechnical constraints can be given adequate consideration in safety requirements.
Such safety requirements and the correctness of the development steps performed are checked using available verification techniques. System validation is done by systematic testing where the determination of test cases and the test execution and evaluation are automated to a high extend. The application of formal specification techniques in the early development phases is utilized to automate subsequent development steps and to avoid errors or identify them early on so that they can be eliminated at reasonable cost.
Extensive prototypical tool support is provided to ensure the efficient application of the overall methodology. Using commercially available tools, the overall tool environment offers a uniform and sophisticated framework supporting all phases of development.
Please contact:
Sergio Montenegro - GMD
Tel: +49 30 6392 1878
E-mail: sergio.montenegro@gmd.de