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

ECS-9709796库马尔这个项目的动机是对用于飞机系统自动控制的操作嵌入式航空电子软件系统进行全面和正式的研究。这样的自动控制系统是混合的，既有连续状态，也有离散状态。将开发一种摩尔机类型的航空电子软件操作程序的正式表示法，并将用于检查软件的一致性和完整性。还将进行必要的扩展，以包括该系统的混合特点。混杂系统的性质验证通过系统和规格说明的混杂自动机表示来完成。提出了一种模块化递阶混杂自动机的复杂混杂系统建模框架。其次，通过扩展离散事件系统的优先同步理论，发展了这类混合系统的相互作用理论。然后，这一理论将被用于设计多个交互混合系统之间所需的接口逻辑。最后，将在所提出的框架中开发用于混合系统的验证和综合的工具和算法，具体地说，我们建议开发一种逐级递阶验证和综合的方法。

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.