Modeling, Interface Design, and Verification of Hybrid and Discrete Event Systems

点击翻译按钮获取中文摘要

ECS-9709796 Kumar This project is motivated from a comprehensive and formal study of operationally embedded avionics software systems that are used in automated control of aircraft systems. Such automated control systems are hybrid-possessing both continuous and discrete states. A Moore machine type formal representation of the operational procedures of the avionics software will be developed and it will be used to check consistency and completeness of the software. Requisite extensions will be also made to include hybrid characteristics of the system. Verification of properties of hybrid systems is accomplished by hybrid automaton representation of the system and the specification. We propose to develop a modular and hierarchical hybrid automata modeling framework of complex hybrid systems. Next a theory of interaction of such hybrid systems will be developed by extending the theory of prioritized synchronization of discrete event systems. This theory will then be used to design the required interface logic between multiple interacting hybrid systems. Finally, tools and algorithms for the verification and synthesis of hybrid systems will be developed in the proposed framework, specifically we propose to develop a method of successive hierarchical verification and synthesis.