Verifying Aspect-oriented Programs using Open Temporal Logic
The behavior model of traditional temporal logic is closed and symmetrical, while the behavior model of aspect-oriented programs is open and asymmetrical. When the programmer designs the base-code, he is not sure what aspects will be woven to it. It is indirect and difficult to specify and verify the behavior of aspect-oriented programs by using traditional temporal logic. In this paper, we propose a new temporal logic named open temporal logic, which introduced some new path operators and one new temporal operator. Since paths are divided into two kinds: internal parts and external parts, the behavioral model of open temporal logic is open and asymmetrical. Base on open temporal logic and the proof system of traditional rely-guarantee method, a new proof system is given to verify the behavior of aspect-oriented programs.
temporal logic formal specification formal verification aspect-oriented language program proof reliability
Jia Lv Jing Ying Minghui Wu Tao Jiang Fanwei Zhu
College of Computer Science and Technology, Zhejiang University,Hangzhou, China College of Computer Science and Technology, Zhejiang University, Hangzhou, China
国际会议
上海
英文
85-92
2009-07-08（万方平台首次上网日期，不代表论文的发表时间）