CAJ | 학술논문

针对SysML序列图本身缺乏分析和验证手段的问题,提出了一种序列图到有色Petri网的转换方法:定义了将序列图的常用操作转换为等价有色Petri网的转换规则,重点是把序列图的常用结构如可选结构、条件结构、并行结构以及循环结构等映射为有色Petri网.这当中既包含结构元素,如库所、变迁、输入/输出弧,又包含逻辑元素,如全局声明中的颜色集和变量、颜色集与库所、弧表达式以及初始标志.应用这些规则可以将序列图转换为有色Petri网模型,进而对其进行仿真分析,并可通过有色Petri网工具验证模型的无死锁性、可达性、有界性和活性.最后通过数字证书更新的实例分析了映射前后两种模型的语义,验证了映射的正确性.
침대SysML서렬도본신결핍분석화험증수단적문제,제출료일충서렬도도유색Petri망적전환방법:정의료장서렬도적상용조작전환위등개유색Petri망적전환규칙,중점시파서렬도적상용결구여가선결구、조건결구、병행결구이급순배결구등영사위유색Petri망.저당중기포함결구원소,여고소、변천、수입/수출호,우포함라집원소,여전국성명중적안색집화변량、안색집여고소、호표체식이급초시표지.응용저사규칙가이장서렬도전환위유색Petri망모형,진이대기진행방진분석,병가통과유색Petri망공구험증모형적무사쇄성、가체성、유계성화활성.최후통과수자증서경신적실례분석료영사전후량충모형적어의,험증료영사적정학성.