可信网络软件的形式验证

项目名称： 可信网络软件的形式验证

项目编号： No.60970007

项目类型： 面上项目

立项/批准年度： 2010

项目学科： 自动化技术、计算机技术

项目作者： 缪淮扣

作者单位： 上海大学

项目金额： 32万元

中文摘要： 以网络软件为研究对象，针对软件可信性质中的正确性和安全性，研究确保软件行为一致性和安全性验证的理论和方法。主要包括：研究网络软件的形式化行为建模与安全建模方法和自动抽取模型的方法、从整体功能层面和交互行为层面对网络软件进行行为建模的方法、威胁驱动的网络软件的形式化安全建模方法、Web应用的on-the-fly导航建模方法；研究自动生成一致性和安全行性质的方法、组合式的抽象精化验证方法与技术；采用模型检验和定理证明结合的方法和技术验证网络软件的行为一致性和安全性；应用监控理论的可控制性原理对构件式系统进行安全性质的验证。研究符号模型检测、限界模型检测、偏序规约模型检测和组合模型检测的理论。开发支持工具。该项研究对于提高网络软件的可信性和质量有重大意义。研究成果可以广泛应用到网络软件的开发过程中。

中文关键词： 形式方法；网络软件建模；形式验证；模型检验；

英文摘要：

英文关键词： Formal methods；network software modeling；formal verification；model checking；