Safety Verification Technologies based on Behavioral Specifications

通过对开发适用性强、灵活性强、易于自动化的验证技术的研究，取得了以下成果：(1)未知病毒检测技术：基于行为规范的逻辑，开发了一种对程序进行行为建模并自动检测其安全性的技术。本文针对Windows操作系统开发了一个病毒检测程序，并验证了所开发技术的有效性。(2)基于行为规范的安全验证技术：通过在行为层形式化需求和/或规范，开发出一种验证技术，可以在对用户或应用逻辑更诚实的层次上验证系统的安全属性。该技术已应用于铁路信号系统、软件组件、并发和分布式系统以及安全协议中，并证明了其有效性。特别是，已经使用该技术对几个实际的电子商务协议进行了验证。(3)基于行为规范的模型检查技术：基于行为规范，开发了一种对具有无限状态的软件有效的模型检查技术。

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.