Framework für CounterExample Validierung und Testfallgenerierung für die Verifikation von eingebetteter Software

01.04.2010 - 30.09.2013
Research funding project
Verifikation und Validierung von eingebetteter Software ist signifikant um einwandfreie Funktion von intelligenten Computersystemen, wie sie in Automobilen, Aufzügen, Flugzeugen, medizinischen Geräten, Roboter, usw. angetroffen werden. Der weit-verbreitete, übliche Ansatz in der Industrie basiert auf dem Testen von einzelnen Testfällen, sog. "corner cases". Obwohl weitläufig bekannt ist, dass mit diesem Ansatz nur ein sehr limitierter Bereich des gesamten Zustandsraums des Systems erfasst werden kann, ist bislang noch kein vollständiger Ansatz entwickelt worden. Formale Verifikationsmethoden wie Modelchecking kombiniert mit Techniken der Zustandsraumreduzierung haben in letzter Vergangenheit deutliche Verbesserungen hervorgebracht. Wie auch immer, formale Verifikation von eingebetteten Systemen spielt in der Praxis leider immer noch eine untergeordnete Rolle. Praktische Einschränkungen dieser Ansätze sind: (i) Das Problem der manuellen Erstellung des Systemmodells, (ii) die resultierenden großen Zustandsräume aber auch (iii) das Auftreten von falsch-Negativen die auf die angewandten Abstraktionstechniken zurückzuführen sind. Der neuartige Ansatz in diesem Projekt fokussiert auf die Entwicklung eines Hardwareframeworks um Modelchecking von Assemblercode und statische Analyse zu unterstützen. Die Innovation besteht aus (a) der automatischen Validierung von Gegenbeispielen, (b) der Verwendung der "Counterexample guided abstraction refinement" Methode, (c) der automatischen Testfallgenerierung und (d) der automatischen Ausführung dieser Testfälle auf der Zielplattform. Dabei fokussiert (a) auf die Beseitigung der falsch-Negativen durch Gegenprüfung der Gegenbeispiele durch die reale Zielplattform (Einem adaptierten Mikrocontroller IP-core). Weiters unterstützt (b) die Reduktion der Zustandsraumexplosion für die Anwendung von Assemblercode Modelchecking und (c+d) behandeln das Problem der Testfallerstellung für Akzeptanztests von eingebetteter Software.

People

Project leader

Project personnel

Institute

Förderungmittel

  • FFG - Österr. Forschungsförderungs- gesellschaft mbH (National) Österreichische Forschungsförderungsgesellschaft mbH (FFG)

Research focus

  • Computer Engineering: 100%

Keywords

GermanEnglish
Counterexample-Validierungcounterexample validation
Testfallgenerierungtest case generation
statische Analyse und Modelchecking von Assemblercodeassembly code static analysis and modelchecking
formale Verifikationformal verification
eingebettete Softwareembedded systems software

External partner

  • RWTH Aachen
  • FH Technikum Wien

Publications