属性序列图:形式语法和语义  

Property Sequence Chart:Formal Syntax and Semantic

作　　者：张鹏程[1] 周宇[1] 李必信[1] 徐宝文[1] 

机构地区：[1]东南大学计算机科学与工程学院,南京210096

出　　处：《计算机研究与发展》2008年第2期318-328,共11页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60473065;60773105);江苏省自然科学基金项目(BK2007513);国家"八六三"高技术研究发展计划基金项目(2007AA01Z141);国家杰出青年科学基金项目(60425206)

摘　　要：在基于场景的软件工程中,时态逻辑被广泛地用来推理并发系统的正确性.模型检验技术允许自动检验系统模型和给定的属性之间的一致性,这些属性常用线性时态逻辑公式来表示.不幸的是,由于这些公式具有复杂的结构使得模型检验技术很难应用在工业实践中.属性序列图可以用来解决这种问题,它是一种基于场景的可视化的语言,容易理解并且具有较强的表达能力,能够克服当前工业中常用的符号中存在的诸多表达缺陷.为了能够完全清晰地描述和理解属性序列图,使其能够广泛地应用,给出其形式语法和基于Bchi自动机的形式语义,并进行了实例研究,讨论了其应用前景.Temporal logics are extensively used to reason about correctness of concurrent system in scenario-based software engineering. Formal verification techniques such as model checking can automatically check the consistence between the system and the properties. These properties are usually represented by linear temporal logics. Unfortunately, the inherent complication of linear temporal logic formulas makes model checking difficult to apply widely in industry practice. Property sequence chart is a scenarios-based visual language, which can solve this problem; it not only has the ability of powerful expression and simplicity, but also can tackle the defaults of currently used notations in industry such as UML 2.0 sequence diagrams and message sequence charts and, in academy, such as live sequence chart. In order to describe PSC clearly and make it used widely, this paper gives the formal syntax and formal semantic. The basic semantic of basic property sequence chart based on Btichi automaton is first given and then the semantic of how to get more complex property sequence chart with Par, Loop, Simulat operators is put forward. Semantic of how to compose two property sequence charts into a more complex one is also given. Finally, some examples are studied and its future applications in model checking are discussed.

关 键 词：时态逻辑 场景 属性序列图 Büchi 自动机 模型检验 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]