文献类型：期刊文献

中文题名：Aspect-Oriented Design Method for Embedded Systems Based on Timed Statecharts

英文题名：基于时间Statecharts的面向方面嵌人式系统设计方法(英文)

作者：文欣秀[1,2];虞慧群[1];郑红[1,2]

机构：[1]Department of Computer Science and Engineering,East China University of Science and Technology;[2]Shanghai Key Laboratory of Computer Software Evaluating and Testing

年份：2013

卷号：10

期号：9

起止页码：33

中文期刊名：China Communications

外文期刊名：中国通信（英文版）

收录：CSTPCD;;Scopus;CSCD:【CSCD2013_2014】；

基金：supported by the National Natural Science Foundation of China under GrantsNo.61173048,No.61103115

语种：中文

中文关键词：embedded systems; model check-ing; timed statecharts; computation tree logic

外文关键词：嵌入式系统;状态图;定时;设计方法;面向方面软件开发;形式化建模;嵌入式应用;分离系统

摘要：The formal modelling and verification method has become an effective way of improving the reliability and correctness of complex,safety-critical embedded systems.Statecharts are widely used to formally model embedded applications,but they do not realise the reasonable separation of system concerns,which would result in code scattering and tangling.Aspect-Oriented Software Development(AOSD)technology could separate crosscutting concerns from core concerns and identify potential problems in the early phase of the software development life cycle.Therefore,the paper proposes aspect-oriented timed statecharts(extended timed statecharts with AOSD)to separately model base functional requirements and other requirements(e.g.,scheduling,error handling),thereby improving the modularity and development efficiency of embedded systems.Furthermore,the dynamic behaviours of embedded systems are simulated and analysed to determine whether the model satisfies certain properties(e.g.,liveness,safety)described by computation tree logic formulae.Finally,a given case demonstrates some desired properties processed with respect to the aspect-oriented timed statecharts model.
The formal modelling and verifica- tion method has become an effective way of improving the reliability and correctness of complex, safety-critical embedded systems. Statecharts are widely used to formally model embedded applications, but they do not realise the reasonable separation of system concerns, which would result in code scattering and tan- gling. Aspect-Oriented Software Development （AOSD） technology could separate crosscut- ting concerns from core concerns and identify potential problems in the early phase of the software development life cycle. Therefore, the paper proposes aspect-oriented timed statech- arts （extended timed statecharts with AOSD） to separately model base functional require- ments and other requirements （e.g., scheduling, error handling）, thereby improving the modu- larity and development efficiency of embed- ded systems. Furthermore, the dynamic be- haviours of embedded systems are simulated and analysed to determine whether the model satisfies certain properties （e.g., liveness, safety） described by computation tree logic formulae. Finally, a given case demonstrates some desired properties processed with re- spect to the aspect-oriented timed statecharts model.