Using formal methods for ensuring quality requirements of systems

摘要

Die Sicherstellung der Einhaltung funktionaler und sicherheitsbezogener Anforderungen von Systemen ist ein Thema, dem in letzter Zeit verstärkt Aufmerksamkeit gewidmet wird. Dies geschieht besonders im Umfeld sicherheitskritischer Anwendungen. In diesem Beitrag wird der Einsatz formaler Methoden zur Überprüfung der Korrektheit von Software im Bezug auf funktionale und sicherheitsbezogene Anforderungen beschrieben. Dabei schlagen die Autoren die Verwendung von Model-Checkern als Tool zur formalen Verifikation und zur automatisierten Erzeugung von Testfällen vor. In heutigen Entwicklungsprozessen wird Verifikation eingesetzt um die Korrektheit eines Designs zu gewährleisten. Da es jedoch wichtig ist, die Funktionalität des Gesamtsystems bestehend aus Hardware, Software und Betriebssystem zu überprüfen, ist das Testen zusätzlich zur Verifikation unerlässlich. Der beschriebene Ansatz kombiniert nun Verifikation und Testen. Die Autoren berichten von Erfahrungen, die in Zusammenarbeit mit einer im sicherheitskritischen Umfeld ansässigen österreichischen Firma entstanden sind.%Ensuring a system's safety, security and functional requirements are important tasks with growing interests in industry. These interests hold especially for companies that deal with safety critical systems. In this article we focus on proving the correctness of safety and functional requirements using formal methods. In particular the paper describes the use of model-checking for verification and its use to automated test-case generation. Whereas verification is of use mainly for checking the correctness of designs, the latter is important to check the functionality of the whole system comprising hardware and software including the operating systems. The generation of test-cases is performed by using the verification model together with mutation testing. We further show how such a combined verification/testing system is used in a practical setting and report a case study that has been carried out together with an Austrian company working in the safety-critical embedded systems domain.