摘要
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.
基金
supported by the National Natural Science Foundation of China under GrantsNo.61173048,No.61103115
