Zsfassung in dt. Sprache ; Oldenburg, Univ., Diss., 2014
HochschulschriftHybrides SystemBounded Model CheckingErfüllbarkeitsproblemGewöhnliche DifferentialgleichungNumerische IntegrationValidierungDifferentialgleichungKontinuierliches SystemDiskretes SystemNP-vollständiges ProblemModel CheckingValiditätRichtigkeit von ErgebnissenIntegration
In dieser Arbeit werden hybrid diskret-kontinuierliche Systeme mittels endlicher Abrollungen ihrer Transitionssysteme analysiert. Die dabei entstehenden Formeln enthalten dabei, im Gegensatz zu Ansätzen aus der Literatur, direkt gewöhnliche Differentialgleichungen. Die Arbeit und die ihr zu Grunde liegenden Publikationen führen hierzu die Formelklasse "Satisfiability modulo ODE" ein und beschreiben die Kombination des iSAT-Erfüllbarkeitsprüfers für boolesche Kombinationen nichtlinearer arithmetischer Bedingungen mit der VNODE-LP-Programmbibliothek für die Berechnung sicherer Einschließungen der Lösungsmengen gewöhnlicher Differentialgleichungen. Der resultierende iSAT-ODE-Erfüllbarkeitsprüfer enthält algorithmische Verfeinerungen wie die Speicherung von Zwischenergebnissen und beantworteter Anfragen, Einhüllendensysteme, sowie Deduktion von Trajektorienrichtungen. Diese werden experimentell anhand akademischer Fallstudien evaluiert und mit der Literatur verglichen. <dt.>
In this thesis, the behavior of hybrid discrete-continuous systems is analyzed using a Bounded Model Checking (BMC) approach, i.e. by finitely unwinding the systems' transition relations as formulae. Contrary to earlier BMC approaches for hybrid systems, we allow Ordinary Differential Equations (ODEs) directly in the formula, introducing the problem class of Satisfiability (SAT) modulo ODE. The main contribution of the thesis and its underlying publications is the direct handling of SAT modulo ODE formulae by combining the iSAT solver for boolean combinations of non-linear arithmetic constraints with the VNODE-LP library for computing validated numerical enclosures for ODE solutions. This iSAT-ODE solver comprises several algorithmic enhancements, like caching of intermediate results and previous queries, bracketing systems, and the deduction of trajectory directions, all of which are subjected to evaluation on academic case studies and compared with results from the literature. <engl.>
