|Thesis abstract: |
The aim of my research is to develop novel methods for verifying the correct functioning of a hybrid system (i.e., a dynamical system with interacting continuous and discrete state components) and for imposing to the system some desired reachability properties related to its evolution by appropriately designing its input.
In standard verification problems, the typical goal is to evaluate if the system executions associated with a set of initial conditions satisfy a certain specification - possibly depending on both the continuous and discrete state components evolution - for some given input. In this research project, we shall address verification problems where the input is not a-priori given but has to be designed so as to determine an appropriate excitation of some internal variables of the system. These variables represent test-points that are not directly accessible but that can be affected by the external input to the system.
The developed techniques will be applied to the testing of the autopilot of an avionic system. Currently, the input design phase is done manually and takes a large fraction of the whole amount of time needed for the verification procedure. The availability of suitable automatic methods for input design is expected to produce a significant impact on the overall process.