Formal models of UML statechart diagrams based on Petri nets
-
摘要: 提出一种可以准确描述UML状态图动态特征的形式化模型SC_Net.首先给出了UML状态图的形式化语法定义,其中用状态集合、转移集合、事件集合、条件集合、活动集合、对象集合和变量集合,定义了一系列辅助函数描述UML状态图特征,用确定目标状态和受限源状态表示层次关系,用开放事件和封闭事件表示对象之间的消息.基于C_Net定义了描述UML状态图动态语义的Petri网模型SC_Net,既能描述状态图中的控制部分,又能描述状态图中的数据处理部分,并给出了从UML状态图到SC_Net的转换步骤,便于实现自动转换过程.最后以柔性制造系统的一个实例说明SC_Net能用于分析UML状态图的性质.Abstract: A formal model named SC_Net which can precisely describe the dynamic features of UML statechart diagrams was presented. Firstly a formal syntactic of UML statechart diagrams was given and a series of auxiliary functions to describe the structure features of UML statechart diagrams were presented in which target determinator and source restriction were used to describe the inter-level transitions and open events and close events were used to describe the communication among UML statechart diagrams. Then, based on C_Net an extended Petri net model named SC_Net was defined which can be used for the semantic models of UML statechart diagrams. Besides the control parts, SC_Net also included the data process parts which was lacked in the research area of formal semantics of UML statechart diagrams. The translation process from UML statechart diagrams to SC_Net was defined. At last, an example in flexible manufacture systems was given. Results show that SC_Net can be used to verify the properties of the UML statecharts.
-
Key words:
- UML statecharts /
- Petri nets /
- formal semantics
-
[1] Harel D. Statecharts:a visual formalism for complex systems[J]. Science of Computer Programming, 1987,8(3):231-274 [2] OMG unified modelling language version 1.5 . Object Management Group, 2003, http://www.omg.org/uml/ [3] Wieringa R, Broersen J. A minimal transition system semantics for lightweight class and behavior diagrams Broy M, Coleman D, Maibaum T, et al. Proceedings of the ICSE98 Workshop on Precise Semantics for Software Modeling techniques. Munich:Technical University Munich,1998:129-151 [4] Latella D, Majzik I, Massink M. Towards a formal operational semantics of UML statechart diagrams Ciancarini P, Fantechi A, Gorrieri R. Proceedings of the 3rd International Conference on Formal Methods for Open Object-Oriented Distributed Systems. Boston:Kluwer Academic Publishers, 1999:15-18 [5] Lilius J, Paltor P I. The semantics of UML state machines . TUCS Technical Report No 273, 1999 [6] Baresi L, Pezzè M. On formalizing UML with high-level Petri nets Cindio F De, Agha G. Concurrent Object-oriented Programming and Petri Nets:Advances in Petri Nets. New york:Springer-Verlag, 2001:276-304 [7] Saldhana J A, Shatz S M, Hu Zh X. Formalization of object behavior and interactions from UML models[J]. International Journal of Software Engineering and Knowledge Engineering, 2001,11(6):643-673 [8] Eshuis R, Wieringa R. Requirements-level semantics for UML statecharts Smith S F, Talcott C L. Processings of Fourth International Conference on Formal methods for open object-based distributed systems. Boston:Kluwer Academic Publishers, 2000:121-140 [9] 袁崇义. Petri网原理与应用[M].北京:电子工业出版社, 2005:213-225 Yuan Chongyi. The theory and application of Petri nets[M]. Beijing:Publishing House of Electronics Industry, 2005:213-225(in Chinese) [10] Busi N. Analysis issues in Petri nets with inhibitor arcs[J]. Theoretical Computer Science, 2002, 275(1/2):127-177 [11] Strrle H. Models of software architecture . Munich:Institute for Information, Ludwig Maximilians University, 2000 -
点击查看大图
计量
- 文章访问数: 3087
- HTML全文浏览量: 238
- PDF下载量: 1569
- 被引次数: 0
下载:
