北京大学学报（自然科学版）
北京大學學報（自然科學版）
북경대학학보（자연과학판）
ACTA SCIENTIARUM NATURALIUM UNIVERSITATIS PEKINENSIS
2005年
3期
344-357
,共14页
孙猛%张乃孝%Bernhard K Aichernig
孫猛%張迺孝%Bernhard K Aichernig
손맹%장내효%Bernhard K Aichernig
UML%状态机%RAISE%形式化
UML%狀態機%RAISE%形式化
UML%상태궤%RAISE%형식화
UML%statechart%RAISE%formalization
使用RAISE规范语言RSL给出了UML状态机视图的形式描述.通过这一形式化提出了一种对图形化的UML状态机视图模型的形式化和RSL规范进行集成的框架,这一工作是对UML类图在RSL中形式化的继续,使得人们可以对UML的非形式化模型给出一种精确、无二义性的语义解释,同时也提高了RSL规范的抽象层次,增强了其可读性、简明性.最后通过一个应用实例,说明这一框架如何用于从UML模型创建对应的形式化规范,并对模型的性质进行了分析.
使用RAISE規範語言RSL給齣瞭UML狀態機視圖的形式描述.通過這一形式化提齣瞭一種對圖形化的UML狀態機視圖模型的形式化和RSL規範進行集成的框架,這一工作是對UML類圖在RSL中形式化的繼續,使得人們可以對UML的非形式化模型給齣一種精確、無二義性的語義解釋,同時也提高瞭RSL規範的抽象層次,增彊瞭其可讀性、簡明性.最後通過一箇應用實例,說明這一框架如何用于從UML模型創建對應的形式化規範,併對模型的性質進行瞭分析.
사용RAISE규범어언RSL급출료UML상태궤시도적형식묘술.통과저일형식화제출료일충대도형화적UML상태궤시도모형적형식화화RSL규범진행집성적광가,저일공작시대UML류도재RSL중형식화적계속,사득인문가이대UML적비형식화모형급출일충정학、무이의성적어의해석,동시야제고료RSL규범적추상층차,증강료기가독성、간명성.최후통과일개응용실례,설명저일광가여하용우종UML모형창건대응적형식화규범,병대모형적성질진행료분석.
It is presented that a formalization for UML statechart diagrams in the RAISE specification language RSL.By such a formalization, a general framework is proposed for integration of graphical UML statechart diagrams and formal RSL specifications,which forms the continuation of the previous work on formalization ofUML class diagrams in RSL.This allows the definition of UML semantic interpretations that are precise and unambiguous,and also enhancing the readability,conciseness and Abstraction of the resulting RSL specification.A case study illustrates how the framework can be used to create formal specification for UMLmodels and analyze the properties of the models.
