Computation Sequence Chart: ein Konzept zur anforderungsbezogenen Testfallgenerierung

Abstract

Anforderungen an das Verhalten eines software-gesteuerten Systems wie auch hinsichtlich weiterer qualitativer Eigenschaften werden im industriellen Kontext nach wie vor in nicht formaler Form, häufig in freiem Text, beschrieben und sind somit semantisch nicht oder nicht hinreichend präzise definiert. Eine Beschreibung in formaler Form, in einer hinsichtlich Syntax und Semantik klar definierten Sprache, beruht i.a. auf einem Axiomensystem, aus dessen Axiomen und Schlussfolgerungen wohldefinierte Systeme gebildet werden, die vorgegebenen Gesetzen folgen [HB01]. Derzeit gibt es keinen praktikablen und gleichzeitig formal korrekten Ansatz, um einen Bezug zwischen nicht-formaler Anforderung und den aus der formalen Spezifikation generierten Testfällen zu ermöglichen. Dieser Bezug würde es erlauben, eine Aussage über die korrekte Umsetzung der nicht-formalen Anforderung in dem getesteten System zu treffen. Die existierenden Verfahren sind entweder zu aufwändig oder nicht formal genug, um durch sie anforderungsbezogene Testfälle generieren zu können. Die vorliegende Arbeit präsentiert ein Konzept zur anforderungsbezogenen Testfallgenerierung. Eine formale Notation, genannt Computation Sequence Chart (CSC), stellt einen Bezug zwischen nicht-formaler und formaler Anforderung her. CSCs können bei der Testfallgenerierung berücksichtigt werden. Um dies zu erreichen, werden die CSCs in eine Logik übersetzt und beim Model-Checking zur Testfallgenerierung in den Prozess integriert. Das theoretisch entwickelte und praktisch validierte Konzept umfasst • die Definition einer graphischen Notation (CSC) zur Verlinkung nicht-formaler Anforderungen und formaler Testmodelle, • Definitionen, Sätze, Regeln und Softwaremodule zur Transformation der Notation in Prädikatenlogik oder Timed Branching Time Logic und • die Einbindung von CSCs in die Generierung von Testfällen am Beispiel zweier Model-Checking Verfahren auf Basis von Timed Statecharts und Timed Automata.