计算机工程与科学
計算機工程與科學
계산궤공정여과학
COMPUTER ENGINEERING & SCIENCE
2015年
8期
1498-1509
,共12页
刘雪%胡军%黄志球%马金晶%程桢%石娇洁
劉雪%鬍軍%黃誌毬%馬金晶%程楨%石嬌潔
류설%호군%황지구%마금정%정정%석교길
系统安全性分析%模型驱动工程%SysML/MARTE%状态机模型%嵌入式系统
繫統安全性分析%模型驅動工程%SysML/MARTE%狀態機模型%嵌入式繫統
계통안전성분석%모형구동공정%SysML/MARTE%상태궤모형%감입식계통
system safety analysis%model-driven engineering%SysML/MARTE%state machine model%embedded system
基于模型的嵌入式系统安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点.提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性验证方法,具体包括:构建了具备SysML/MARTE扩展语义的状态机元模型,以及安全性建模与分析语言AltaRica的语义模型GTS的元模型;然后建立了从SysML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则,并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证的框架.最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析.
基于模型的嵌入式繫統安全性分析與驗證方法是近年來在安全攸關繫統工程領域中齣現的一箇重要研究熱點.提齣一種基于模型驅動架構的麵嚮SysML/MARTE狀態機的繫統安全性驗證方法,具體包括:構建瞭具備SysML/MARTE擴展語義的狀態機元模型,以及安全性建模與分析語言AltaRica的語義模型GTS的元模型;然後建立瞭從SysML/MARTE狀態機模型分彆到時間自動機模型以及AltaRica模型的語義映射模型轉換規則,併基于AMMA平檯和時間自動機驗證工具UPPAAL設計實現瞭對SysML/MARTE狀態機的模型轉換與繫統安全性形式化驗證的框架.最後給齣瞭一箇飛機著陸控製繫統設計模型的安全性驗證實例分析.
기우모형적감입식계통안전성분석여험증방법시근년래재안전유관계통공정영역중출현적일개중요연구열점.제출일충기우모형구동가구적면향SysML/MARTE상태궤적계통안전성험증방법,구체포괄:구건료구비SysML/MARTE확전어의적상태궤원모형,이급안전성건모여분석어언AltaRica적어의모형GTS적원모형;연후건립료종SysML/MARTE상태궤모형분별도시간자동궤모형이급AltaRica모형적어의영사모형전환규칙,병기우AMMA평태화시간자동궤험증공구UPPAAL설계실현료대SysML/MARTE상태궤적모형전환여계통안전성형식화험증적광가.최후급출료일개비궤착륙공제계통설계모형적안전성험증실례분석.
