Safety Verification Technologies based on Behavioral Specifications

(1)未知病毒检测技术：基于行为规范的逻辑，提出了一种对程序的行为S进行建模并自动检测其安全性的技术。基于行为规范的安全验证技术：通过对需求和/或规范在行为层面上的形式化描述，开发了一种验证技术，能够在对用户或应用逻辑更诚实的级别上验证系统的安全属性。该技术已在铁路信号系统、软件构件、并发分布式系统、安全协议等方面得到应用，并被证明是有效的。基于行为规范的模型检测技术：基于行为规范，提出了一种适用于无限状态软件的模型检测技术。

The following results have been gotten by doing research for developing the verification technology which is highly applicable and flexible, and is amenable for automation.(1)Inspection Technology for Unknown Viruses : Based on the logics of behavioral specifications, a technology for modeling behavior s of programs and automatically inspecting their safety is developed. A virus inspection program is developed for Windows OS, and the effectiveness of developed technology has been proved.(2) Safety Verification Technology based on Behavior Specification : By formalizing requirements and/or specifications in behavior level, a verification technology is developed which can verify the safety properties of systems in the level which is more honest to users or application logics. The technology has been applied to railway signal systems, software components, concurrent and distributed systems, and secure protocols, and is proved to be effective. In particular, verifications of several practical e-commerce protocols have been done using the technology.(3) Model Checking Technology based on Behavioral Specification : Based on behavioral specifications, a model checking technology which is effective for software with infinite states is developed.