摘要
状态机作为一种描述实体间交互或者单个实体行为的建模图，它具有丰富的直观图形化的符号。在许多模型的设计阶段都采用它来建模。但是因为缺乏精确完整的语义定义，给它的形式化验证带来困难。本文给出一种形式化操作语义，并概述基于形式化规则的验证技术。
The state machine is a modeling chart describing the alternation of objects and the dynamic behavior of an object .Because of its variety of well-known and intuitive graphical notations,we use it for modeling in design phase.However, the unprecise and incomplete semantics definition bring difficulties to its formal verification.This article introduces an formal operational semantics and summarizes a verifiable technique based on formulas.
作者
林敬恩
滕忠坚
陈圣群
LIN Jing-en,TENG Zhong-jian,CHEN Sheng-qun （Key Laboratory of OptoElectromc Science and Technology,Ministry of Educadon,Fu]ian Normal Umversity,Fuzhou 350007,China）
出处
《电脑知识与技术》
2008年第5期720-722,共3页
Computer Knowledge and Technology
关键词
状态机
操作语义
建模
验证技术
State machine
operational semantics
modeling
verifiable technique
