Switched Bond Graphs as Front-End to Formal Verification of Hybrid Systems

. Formal verification of safety and timing properties of engineering systems is only meaningful if based on models which are systematically derived. In this paper we report on our experience using switched bond graphs for the modelling of hardware components in hybrid systems. We present the basic ideas underlying bond graphs in general and switched bond graphs in particular. Switched bond graphs are tailored for the modelling of physical systems undergoing abrupt structural changes. Such abrupt changes appear frequently in plants closed by discrete controllers. We illustrate our approach by means of an aircraft landing gear system and prove safety and timeliness properties using the proof system of extended duration calculus. Keywords: hybrid system, physical modelling, bond graph, verification, duration calculus 1 Introduction In this paper we report on our experience on using switched bond graphs as a front-end to hardware engineers in verifying complex hybrid systems involving bot..