ABSTRACT
Hybrid systems, in which digital controllers interact with a physical, continuous world show increasing presence in various safety-critical applications, e.g., in the automotive sector, in aviation or in automated plants. This chapter focuses on approaches based on iterative forward reachability computations; for models in which the evolution of the quantities over time follows non-linear functions, these methods are also known as flowpipe-construction-based techniques. The chapter extends by generalizing some formalisms and extending method by specific approaches to handle model parts within the expressivity of rectangular automata: It develops data structures for rectangular automata, a subclass of hybrid automata that are more expressive than timed automata but for which there are more efficient reachability analysis methods, The chapter implements tailored methods for the one-step reachability analysis of rectangular automata, and extends dynamic decomposition methods to detect and handle subspaces with rectangular dynamics automatically.
