基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究_黄传林.docVIP

基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究_黄传林 小型微型计算机系统JournalofChineseComputerSystems2015年3月第3期Vol．36No．32015 基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究 11 黄志球，胡黄传林， 12 1，211 军，徐丙凤，曲长亮 （南京航空航天大学计算机科学与技术学院，南京210016）（南京大学计算机软件新技术国家重点实验室，南京210093） E-mail：huangchuanlin@nuaa．edu．cn 要：能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一；本文提出一种 结合MAＲTE语义信息的扩展SysML活动图模型，用于描述安全关键应用中的嵌入式系统动态行为的设计，并对此扩展模型展摘 开基于模型转换的系统设计安全性特征的形式化分析与验证方法的研究；包括：构建了SysML活动图与MAＲTE中非功能性质建模语义相结合的元模型，以及验证工具UPPAAL的时间自动机元模型，并且给出了二者之间的语义映射规则；建立了从时间自动机模型描述到UPPAAL工具输入格式之间的语法转换方法；设计了一个基于AMMA平台的面向扩展SysML活动图的模型转换与验证框架；最后，给出了一个高铁控制系统设计模型的安全性验证的实例分析．关键词：嵌入式系统安全性分析；SysML活动图；MAＲTE；模型转换；形式化方法 1220（2015）03-0408-10中图分类号：TP311文献标识码：A文章编号：1000- ＲesearchonSafetyVerificationofExtendedSysMLActivityDiagramforEmbeddedSystem Design 2 HUANGChuan-lin1，HUANGZhi-qiu1，HUJun1，，XUBing-feng1，QUChang-liang112 （CollegeofComputerScienceandTechnology，NanjingUniversityofAeronauticsandAstronautics，Nanjing210016，China）（StateKeyLaboratoryforNovelSoftwareTechnology，NanjingUniversity，Nanjing210093，China） Abstract：Intheareasofenergy，transportationandothers，thesafetyverificationandanalysisofcomplexembeddedsystemdesignhasbecomeoneoftheimportantresearch；thispaperpresentsanextendedSysMLactivitydiagrammodelcombinedwithMAＲTEsemanticin-formation，whichusedtodescribethedesignofdynamicembeddedsystembehaviorinsafety-criticalapplications，andhasaresearchoftheformalsafetyanalysisandverificationforthesystemdesignhavingsafetyfeaturesbasedonmodeltransformation，whichisasfollow：constructsthemeta-modelofSysMLactivitydiagramcombinedwithnon-functionalmodelingsemanticofMAＲTEandtimedautomatausedintheUPPAALoneofmodelcheckertools，then，givesthesemanticmappingrulesbetweenthetwo；constructsthesyntaxtransfor-mationbetweenthedescriptionoftimedautomatamodelandtheinputformatofUPPAAL；designsthemodeltransformationandverifica-tionframeworkfortheextendedSysMLactivitydiagrambasedontheAMMAplatform；finally，hasasafetyverificationofadesignmo