The Formal Semantics of UML State Machine
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    More and more large systems are taking UML as requirements description language for system analysis and design, especially in those safety-critical systems. One of the most important dynamic behaviorspecifying mechanism of UML---the UML state machine, is widely used for specification of communicationprotocols and control units. Unfortunately, UML has no strictly defined formal dynamic semantics. It is difficult to do formal verification and proof on the requirements. In this paper, a formal semantics of UML state machine is built. The UML state is firstly represented by inductive state term from some kind of term algebra. Secondly, a labeled transition system (LTS) is introduced, in which an LTS-state is a UML state term, an LTS-transition is a micro step of UML state machine. In the end, a set of Plotkin-style structural operational semantics (SOS) rules inductively defines a compositional formal semantics for UML state machine. This method not only synthesizes those formal methods for classical Statecharts, but also makes innovation addrerssed to UML state machine. At any tiem, the configuration of the machine can be inferred from the state term. The simplified LTS-lable and structuralized operational semantics ruls will play a fundamental fole in formal verification.

    Reference
    Related
    Cited by
Get Citation

蒋慧,林东,谢希仁. UML状态机的形式语义.软件学报,2002,13(12):2244-2250

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:April 17,2001
  • Revised:November 02,2001
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063