论文部分内容阅读
在基于场景的软件工程中，时态逻辑被广泛地用来推理并发系统的正确性．模型检验技术允许自动检验系统模型和给定的属性之间的一致性，这些属性常用线性时态逻辑公式来表示．不幸的是，由于这些公式具有复杂的结构使得模型检验技术很难应用在工业实践中．属性序列图可以用来解决这种问题，它是一种基于场景的可视化的语言，容易理解并且具有较强的表达能力，能够克服当前工业中常用的符号中存在的诸多表达缺陷．为了能够完全清晰地描述和理解属性序列图，使其能够广泛地应用，给出其形式语法和基于Büchi自动机的形式语义，并进行了实例