Automatisierte Testdatengenerierung hybrider diskret-kontinuierlicher eingebetteter Systeme

Abstract

In this dissertation we present an incremental approach to solve the Satisfiability (SAT) Problem for the automated test case generation of hybrid discrete and continuous embedded systems using background theory solvers of the linear arithmetic (LA) and fixed-size bit-vectors (BV) for quantifier-free first-order formulae. Both of these theory solvers extend the Davis-Putnam-Logemann-Loveland decision procedure (DPLL), which was initially designed to solve the satisfiability problem in the propositional logic, to the first-order logic. Furthermore the both theory solvers can be integrated in a lazy SMT-Theorem Prover - also known as Satisfiability Modulo Theory - as a decision procedure for the conjunction of literals in their specified theories and implement theory-driven deduction, learning and backjumping techniques to enhance the efficiency of the SMT-Theorem Prover.