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

上海大学学报(自然科学版) ›› 2012, Vol. 18 ›› Issue (2): 156-162.

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

戴雨婷，缪淮扣，梅佳，高洪皓

(1.上海大学计算机工程与科学学院，上海 200072; 2.上海市计算机软件评测重点实验室，上海 201114)

出版日期:2012-04-30 发布日期:2012-04-30

Property Extraction Based on LSC Model Checking

(1. School of Computer Engineering and Science, Shanghai University, Shanghai 200072, China；
2. Shanghai Key Laboratory of Computer Software Evaluating and Testing, Shanghai 201114, China)

Online:2012-04-30 Published:2012-04-30

摘要/Abstract

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

关键词: LSC, 模型验证, 性质抽取, 一致性

Abstract: This paper uses live sequence chart (LSC) to describe scenariobased requirement specifications. According to the principle that design model must be consistent with the specification of requirement model, and aiming at extraction of safety, reachability and liveness, the paper proposes three criteria for generating and extracting properties from LSC specification automatically. The extracted result can be used for automatic verification, providing protection for consistency of requirement model with the design model.

Key words: consistency, extracting properties, live sequence chart (LSC), model checking

中图分类号:

TP 311.51

戴雨婷，缪淮扣，梅佳，高洪皓. 基于LSC模型检验的性质抽取[J]. 上海大学学报(自然科学版), 2012, 18(2): 156-162.