An Operational Semantics for UML State Machines in Model Checking Context

ZHOU Ying; ZHENG Guo-liang; LI Xuan-dong

您当前的位置：

首页 >

文章列表页 >

An Operational Semantics for UML State Machines in Model Checking Context

更新时间：2025-07-16

- An Operational Semantics for UML State Machines in Model Checking Context
- Acta Electronica Sinica Vol. 31, Issue S1, Pages: 2091-2095(2003)
- 作者机构：
  
  1. 南京大学计算机软件新技术国家重点实验室,江苏,南京,210093
  2. 南京大学计算机科学技术系,江苏,南京,210093
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP311
- Published Online：25 December 2003，
  
  Published：2003
- 稿件说明：
移动端阅览
ZHOU Ying, ZHENG Guo-liang, LI Xuan-dong. An Operational Semantics for UML State Machines in Model Checking Context[J]. Acta Electronica Sinica, 2003, 31(S1): 2091-2095.
DOI：

ZHOU Ying, ZHENG Guo-liang, LI Xuan-dong. An Operational Semantics for UML State Machines in Model Checking Context[J]. Acta Electronica Sinica, 2003, 31(S1): 2091-2095. DOI：

摘要

UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图.它丰富的表示符号提供了强大的描述机制

但也降低了其结构的模块性

提高了对其分析验证的难度.模型检验是自动检验有限状态并发系统的技术.通过模型检验SM描述的不同系统元素的行为是否满足某些性质

能尽早发现设计中的错误.为了将模型检验技术应用于SM的验证

本文用kripke结构定义SM的操作语义.与已有的SM语义定义不同

本文考虑到了SM中包含的不确定因素

用kripke结构描述系统所有可能的演化轨迹.通过检验从SM翻译得到的kripke结构达到模型检验SM的目的.

Abstract

The state machine formalism in UML is used for modeling discrete behavior of various system elements.Its rich notation provides a powerful description mechanism which meanwhile decreases modality of its structure and increases verifying complexity.Model checking is a technique for automatically verifying finite-state concurrent systems.By model checking the behavior of various system elements described by SM

we can find design errors as soon as possible.This paper defines an operational semantics for SM using Kripke structure in order to model checking SM.Different from existing SM semantics definitions

this paper takes undetermined factors in SM into consideration.SM is translated into kripke structure that describes all possible evolving traces on which model checker checks.

关键词

Keywords

references

Views

1461

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Test Program Generation for Microprocessor Verification Using Local Modeling Strategy

Property Generation Method for Model Checking on Clock Domain Crossing Design

Model Checking on Clock Domain Crossing Design of System-on-Chip

Monte Carlo Simulation of THz-Pulse Generation from Semiconductor Surface

Development of Software Modeling Tools Based on UML

Related Author

WANG Ke-yi

CHENG Xu

TONG Dong

YI Jiang-fang

ZHANG Liang

XU Jing-wei

FENG Yi

YI Jiang-fang

Related Institution

Microprocessor Research and Development Center of Peking University

ShenZhen Graduate School,Peking University

Micro-Processor Research and Development Center,Peking University

Department of Electronics and Communication Engineering,the State Key Laboratory of Optoelectronic Materials and Technologies,Zhongshan University

Department of Computer Science and Technology, Peking University

⁰