%0 Journal Article %1 guo_07_formal %A Guo, F. %A Yao, S. %C School of Computer Science and Technology, Beijing University of Aeronautics and Astronautics, Beijing 100083, China %D 2007 %J Beijing Hangkong Hangtian Daxue Xuebao %K 2007 statecharts petrinets uml chinese _to_download %N 2 %P 248--252 %T Formal models of UML statechart diagrams based on Petri nets %U http://www.scopus.com/scopus/record/display.url?view=extended&origin=resultslist&eid=2-s2.0-34147212768 %V 33 %X 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 state-chart 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.

@article{guo_07_formal, 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 state-chart 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.}, added-at = {2009-02-11T20:51:04.000+0100}, address = {School of Computer Science and Technology, Beijing University of Aeronautics and Astronautics, Beijing 100083, China}, author = {Guo, F. and Yao, S.}, biburl = {https://www.bibsonomy.org/bibtex/2b965be625107df38a295aec173373927/leonardo}, citeulike-article-id = {1277840}, interhash = {62ca6fa70201bbe4ea4333b8bed23f63}, intrahash = {b965be625107df38a295aec173373927}, journal = {Beijing Hangkong Hangtian Daxue Xuebao}, keywords = {2007 statecharts petrinets uml chinese _to_download}, number = 2, pages = {248--252}, posted-at = {2007-05-04 19:48:24}, priority = {1}, timestamp = {2009-02-11T20:51:04.000+0100}, title = {Formal models of UML statechart diagrams based on Petri nets}, url = {http://www.scopus.com/scopus/record/display.url?view=extended&origin=resultslist&eid=2-s2.0-34147212768}, volume = 33, year = 2007 }