|
Systems Modeling Language (SysML) is the latest international standard modelinglanguage in the field of systems engineering which is an extension and expansion of the UnifiedModeling Language (UML).SysML provides visualization and graphical system modelingsupport on the system design and modeling features in the field of systems engineering, and havegained the support of many companies, which is widely used in modeling complex systems.However, in order to maintain legible described, in giveing semantic description SysML usessemi-formal description which uses natural language to describe constraints and detailedsemantic, and strives to achieve the balance between a form of strict and easyly tounderstand.This means that SysML itself lacks a means of analysis and validation. Sequencediagram, activity diagram and state machine diagram as a behavioral modeling in SysML model,there is no such problem equally. In this paper, we study on the problem and complete thefollowing work:Firstly, this paper proposes a method for conversing sequence diagrams into the coloredPetri nets, defining an equivalent conversion rules for converting sequence diagrams of thecommon operations into a colored Petri net, mainly focusing on mapping sequence diagram‘scommon structure such as optional structures, alternate structures, parallel structure and loopstructure into colored Petri nets, which not only contains structure elements, such asplace,transition, input and output arcs, but also contains the logic elements, such as the globaldeclaration of the color sets and variables, color sets and places, and the initial marking, arcexpression. Using these transformation rules, sequence diagrams can be transformed into coloredPetri nets, and thus its formation and analysis. Besides of this, it can verify the characters of themodel, such as absence-deadlocks, boundness, liveness, etc.At the same time, this method hasexcellent characteristics of scalable and can handel the message with the conditions and thecorresponding changes with time interval. Finally, the examples of digital certificates updatedanalysis the semantic of the model before and after mapping, verifying the correctness of themapping.Secondly, the paper proposes a method for conversing the SysML activity diagram into thePetri net, mainly defines six transformation rules for converting SysML activity diagram to aPetri net executable model. Using these transformation rules, SysML activity can be transformedinto Petri net, and thus its simplication, analysis and verification. Besides of this, it can detectconcurrency-related code of conduct nature, such as deadlocks, boundness, etc. And theconsistency of the model is verified by the list method and simulates method. Finally, an example is used verified the feasibility of the method.Thirdly, the paper proposes a method for conversing SysML state machine diagrams intogeneralized Stochastic Petri Nets, mainly defines some transformation rules for convertingSysML state machine diagram to a generalized Stochastic Petri net executable model. Usingthese transformation rules, SysML state machine diagram can be transformed into generalizedStochastic Petri net, and thus its analysis and verification. Besides of this, it can detectconcurrency-related code of conduct nature, such as deadlocks, boundness, etc. At the same time,the method can handel state transition with a time delay and the probability ofinformation.Finally, an example of digital certificates systems is used verified the feasibility ofthe method.
|