文献类型：期刊文献

中文题名：基于时间Statecharts的面向方面嵌入式系统设计方法

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

作者：文欣秀;虞慧群;郑红

机构：[1]E China Univ Sci & Technol, Dept Comp Sci & Engn, Shanghai 200237, Peoples R China;[2]Shanghai Key Lab Comp Software Evaluating & Testi, Shanghai 201112, Peoples R China

年份：2013

卷号：10

期号：9

起止页码：33

中文期刊名：中国通信

外文期刊名：China Communications

收录：CSTPCD;;Scopus;WOS:【SCI-EXPANDED(收录号:WOS:000324552800005)】；CSCD:【CSCD2013_2014】；

基金：The authors would like to express their appreciation to the anonymous referees for their valuable suggestions and comments. This work was partially supported by the National Natural Science Foundation of China under Grants No. 61173048, No. 61103115.

语种：中文

中文关键词：embedded systems;model checking;timed statecharts;computation tree logic

外文关键词：embedded systems;model checking;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.