Logic and compositional verification of hybrid systems (invited tutorial)

Hybrid systems are models for complex physical systems
and have become a widely used concept for understanding
their behavior. Many applications are safety-critical,
including car, railway, and air traffic control,
robotics, physical-chemical process control, and
biomedical devices. Hybrid systems analysis studies how
we can build computerised controllers for physical
systems which are guaranteed to meet their design
goals. The continuous dynamics of hybrid systems can be
modeled by differential equations, the discrete
dynamics by a combination of discrete state-transitions
and conditional execution. The discrete and continuous
dynamics interact to form hybrid systems, which makes
them quite challenging for verification.

 In this tutorial, we survey state-of-the-art
verification techniques for hybrid systems. In
particular, we focus on a coherent logical approach for
systematic hybrid systems analysis. We survey theory,
practice, and applications, and show how hybrid systems
can be verified in the hybrid systems verification tool
KeYmaera. KeYmaera has been used successfully to verify
safety, reactivity, controllability, and liveness
properties, including collision freedom in air traffic,
car, and railway control systems. It has also been used
to verify properties of electrical circuits. 

@inproceedings{DBLP:conf/cav/Platzer11,
	pdf = {pub/lahs-tutorial.pdf},
	slides = {pub/lahs-tutorial-slides.pdf},
	author = {['André Platzer']},
	title = {Logic and Compositional Verification of
               Hybrid Systems
               (Invited Tutorial)},
	booktitle = {CAV},
	longbooktitle = {Computer Aided Verification, 23rd
               International Conference,
               CAV 2011, Snowbird, UT, USA, July 14-20,
               2011, Proceedings},
	year = {2011},
	pages = {28-43},
	month = {},
	editor = {['Ganesh Gopalakrishnan', 'Shaz Qadeer']},
	publisher = {Springer},
	series = {LNCS},
	volume = {6806},
	doi = {10.1007/978-3-642-22110-1_4},
	abstract = {
    Hybrid systems are models for complex physical systems
    and have become a widely used concept for understanding
    their behavior. Many applications are safety-critical,
    including car, railway, and air traffic control,
    robotics, physical-chemical process control, and
    biomedical devices. Hybrid systems analysis studies how
    we can build computerised controllers for physical
    systems which are guaranteed to meet their design
    goals. The continuous dynamics of hybrid systems can be
    modeled by differential equations, the discrete
    dynamics by a combination of discrete state-transitions
    and conditional execution. The discrete and continuous
    dynamics interact to form hybrid systems, which makes
    them quite challenging for verification.

     In this tutorial, we survey state-of-the-art
    verification techniques for hybrid systems. In
    particular, we focus on a coherent logical approach for
    systematic hybrid systems analysis. We survey theory,
    practice, and applications, and show how hybrid systems
    can be verified in the hybrid systems verification tool
    KeYmaera. KeYmaera has been used successfully to verify
    safety, reactivity, controllability, and liveness
    properties, including collision freedom in air traffic,
    car, and railway control systems. It has also been used
    to verify properties of electrical circuits. }
}