Safety Verification Technologies based on Behavioral Specifications

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

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.