从活性顺序图到时态逻辑的转化方法  

Transfer method from live sequence charts to temporal logic

作　　者：付明慧[1] 周清雷[1] 张兵[1] 

机构地区：[1]郑州大学信息工程学院,河南郑州450001

出　　处：《计算机工程与设计》2012年第9期3437-3441,共5页Computer Engineering and Design

基　　金：国家863高技术研究发展计划基金项目(2007AA010408)

摘　　要：为了将活性顺序图用于模型检测,方便描述系统的场景需求,提出了一种将活性顺序图转换成时态逻辑的转化方法。分析活性顺序图语言并且定义一种基于路径的语义,用活性顺序图表述系统的场景需求。根据提出的语义,给出了一个将场景需求显式转化为时态逻辑的一般方法,针对并发消息较多的系统扩展和优化此方法,以得到更简短的时态逻辑公式。通过实例说明活性顺序图到线性时态逻辑的转化过程。In order to use LSC in model checking and describe scenario-based requirements of system conveniently,a method of converting LSC into the corresponding temporal logic is presented.First,the LSC language is analyzed and a trace-based semantics is defined.Then,LSC charts are used to capture the scenario-based requirements of system.According to the semantics proposed,a method of transforming the scenario-based requirements to temporal logic is given and by extending and optimizing this method for system that have lots of concurrent messages,a more succinct temporal logic formulas is obtained.In the end,an example is given to show the transformation process of LSC to temporal logic

关 键 词：活性顺序图 时态逻辑 路径语义 场景需求 模型检测 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]