• search hit 1 of 2
Back to Result List

Using Constraint Logic Programming for Modeling and Verifying Hierarchical Hybrid Automata

  • Hybrid systems are the result of merging the two most commonly used models for dynamical systems, namely continuous dynamical systems defined by differential equations and discrete-event systems defined by automata. One can view hybrid systems as constrained systems, where the constraints describe the possible process flows, invariants within states, and transitions on the one hand, and to characterize certain parts of the state space (e.g. the set of initial states, or the set of unsafe states) on the other hand. Therefore, it is advantageous to use constraint logic programming (CLP) as an approach to model hybrid systems. In this paper, we provide CLP implementations, that model hybrid systems comprising several concurrent hybrid automata, whose size is only straight proportional to the size of the given system description. Furthermore, we allow different levels of abstraction by making use of hierarchies as in UML statecharts. In consequence, the CLP model can be used for analyzing and testing the absence or existence of (un)wanted behaviors in hybrid systems. Thus in summary, we get a procedure for the formal verification of hybrid systems by model checking, employing logic programming with constraints.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Ammar Mohammed, Frieder Stolzenburg
Series (Volume no.):Arbeitsberichte, FB Informatik (2009,6)
Document Type:Part of Periodical
Date of completion:2009/06/24
Date of publication:2009/06/24
Publishing institution:Universität Koblenz, Universitätsbibliothek
Release Date:2009/06/24
Tag:constraint logic programming; hybrid systems
Number of pages:21
Institutes:Fachbereich 4
Fachbereich 4 / Institut für Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):License LogoEs gilt das deutsche Urheberrecht: § 53 UrhG