基于LSC的模型检验研究  

MODEL CHECKING OF LSC SPECIFICATIONS

作　　者：吴宏[1] 齐治昌[1] 

机构地区：[1]国防科大计算机学院,湖南长沙410073

出　　处：《计算机应用与软件》2006年第7期5-7,20,共4页Computer Applications and Software

基　　金：国家自然基金(编号:90104007和60233020)资助

摘　　要：LSC是一种表达能力很强的顺序图建模语言,模型检验技术是验证软件模型正确性的重要方法,提出了一个对LSC模型进行模型检验的方法,并实现了相关支持工具。首先分析了LSC语言,然后基于其语义提出了生成LSC等价状态模型的方法,进而对生成的状态模型进行模型检验;最后进行了实例研究,利用给出的实现工具检验了用CTL描述的验证性质。LSC is an expressive model specification language that can model the system behaviour with the messages between system objects and environment. Model checking is an important method to ensure the correctness of the specifications acquired during model design process. This paper presents a LSC specification based model checking method. The paper first discussed the LSC language. Based on the LSC automaton semantics a method is gived that generates the state models from LSC models, and then we can do model checking on the state models. Finally, a railway control case is studied. The properties described by CTL are verified with the supporting tool that we have developed.

关 键 词：LSC 顺序图 模型检验 CTL 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论] U284.3[自动化与计算机技术—计算机科学与技术]