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.