Automatisierte Testdatengenerierung hybrider diskret-kontinuierlicher eingebetteter Systeme
Veröffentlichungsdatum
2010-06-28
Autoren
Betreuer
Gutachter
Zusammenfassung
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.
Schlagwörter
Test Automation
;
Satisfiability Modulo Theories
;
DPLL
;
SAT
;
Interval Analysis
;
Fourier Motzkin elimination
;
bit-vectors
;
linear arithmetic
;
HYBIS constraint solver
;
HYLIS constraint solver
;
three-valued logic
;
Galois Connections
Institution
Fachbereich
Dokumenttyp
Dissertation
Zweitveröffentlichung
Nein
Sprache
Deutsch
Dateien![Vorschaubild]()
Lade...
Name
00011952.pdf
Size
3.95 MB
Format
Adobe PDF
Checksum
(MD5):7b2d034ebd74e402face0cbaa162e4b8