Cyber-physical systems (CPS):
CPS feature discrete dynamics (e.g., autopilots in airplanes, controllers in self-driving cars) as well as continuous dynamics (e.g., motion of airplanes or cars) and are increasingly used in safety-critical areas. Models of such CPS (i.e., hybrid system models, e.g., hybrid automata, hybrid programs) are used to capture properties of these CPS as a basis to analyze their behavior.
Formal verification of CPS:
The hybrid dynamics of computation and physics in safety-critical CPS are almost impossible to get right without proper formal analysis. However, as the complexity of these systems increases, monolithic models and analysis techniques become unnecessarily challenging.
Component-based modeling approaches split large models into partial models, i.e., co-existing or interacting components (e.g., multiple airplanes in a collision avoidance maneuver). Even though this can lead to component-based models with improved structure and reduced modeling complexity, component verification results do not always transfer to composite systems without appropriate care.