论文部分内容阅读
以Web应用为代表的网络软件安全性受到业界的广泛关注，对具有复杂交互行为的Web戍用安全性建模和验证是一个挑战．该文提出一种威胁驱动的、veb应用On-the-Fly导航模型验证方法，采用威胁驱动方法从规格说明中设计和抽取用于性质检验的安全性质，利用模型检测工具NuSMV对建立的模型进行验证．实验结果表明该方法可以减少搜索空间并在一定程度上避免状态空间爆炸．