Aspect-Oriented Design Method for Embedded Systems Based on Timed Statecharts  

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

作　　者：文欣秀 虞慧群 郑红 

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

出　　处：《China Communications》2013年第9期33-42,共10页中国通信（英文版）

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

摘　　要：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.

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

分 类 号：TP368.1[自动化与计算机技术—计算机系统结构]