基于LSC模型检验的性质抽取

采用LSC(live sequence chart)描述基于场景的需求规格说明,根据设计模型必须满足需求规格说明的一致性原理,针对安全性、可达性、活性等性质,设计3种用于自动生成和抽取性质的覆盖准则,并根据准则从LSC需求规格说明中抽取与设计模型相关的性质.抽取的结果可用于自动化验证,为验证需求模型与设计模型的一致性提供保障.     

威胁驱动的Web应用On-The-Fly导航模型验证方法

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