Fluent model checking for event-based systems
Fluent model checking for event-based systems
复制标题
DOI：
10.1145/940071.940106
复制
发表时间：
2003-09
期刊：
影响因子：
--
通讯作者：
D. Giannakopoulou;J. Magee
中科院分区：
文献类型：
--
作者：
D. Giannakopoulou;J. Magee
模型检查是一种自动化技术，用于验证系统是否满足一组必需的属性。这些属性通常表示为时态逻辑公式，其中原子命题是系统状态变量的谓词。在基于事件的系统描述中，状态不是由状态变量来表征的，而是由在这些状态中产生的行为来表征的。在这种情况下，时间公式很自然地由原子命题构建，这些原子命题是动作发生的谓词。本文确定了这种方法的局限性，并介绍了“流畅”的命题，允许公式自然地表达属性，联合收割机的状态和行动。流畅是世界的一种属性，它在由一个动作启动后保持，并在被另一个动作终止时停止保持。本文描述了一种基于流的线性时态逻辑性质模型检测方法，并在LTSA工具中实现和应用。
Model checking is an automated technique for verifying that a system satisfies a set of required properties. Such properties are typically expressed as temporal logic formulas, in which atomic propositions are predicates over state variables of the system. In event-based system descriptions, states are not characterized by state variables, but rather by the behavior that originates in these states in terms of actions. In this context, it is natural for temporal formulas to be built from atomic propositions that are predicates on the occurrence of actions. The paper identifies limitations in this approach and introduces "fluent" propositions that permit formulas to naturally express properties that combine state and action. A fluent is a property of the world that holds after it is initiated by an action and ceases to hold when terminated by another action. The paper describes an approach to model checking fluent-based linear-temporal logic properties, with its implementation and application in the LTSA tool.