Eggers, Andreas (2014) Direct handling of ordinary differential equations in constraint-solving-based analysis of hybrid systems. PhD, Universität Oldenburg.

Preview

Volltext (1705Kb)

Abstract

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.

["eprint_fieldname_title_plus" not defined]

Direkte Behandlung gewöhnlicher Differentialgleichungen in erfüllbarkeitsbasierter Analyse hybrider Systeme

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Hybrides System, Bounded Model Checking, Erfüllbarkeitsproblem, Gewöhnliche Differentialgleichung, Numerische Integration, Validierung
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	15 Aug 2014 12:01
Last Modified:	15 Aug 2014 12:01
URI:	https://oops.uni-oldenburg.de/id/eprint/1911
URN:	urn:nbn:de:gbv:715-oops-19928
DOI:
Nutzungslizenz:

Actions (login required)

View Item