Jasmine: A Tool for Model-Driven Runtime Verification with UML Behavioral Models
This paper describes the Jasmine tool to detect inconsistencies between the modelled behavior depicted in UML behavior models and monitored runtime behavior of Java programs by runtime verification. Jasmine takes Java programs under verification and corresponding UML models including sequence diagrams, activity diagrams and state machine diagrams. Jasmine imports and parses UML models created by any UML modelling tools. Jasmine instruments the code directed by the UML models,so as to relate the monitored runtime behavior to the UML models. Jasmine drives the instrumented program by existing test suites to collect the program execution traces. Jasmine checks the consistencies between the collected program execution traces and the UML models. It is implemented in Eclipse framework,working as a stand-alone Java application as well as a plug-in in Eclipse platform. It is highly automated and has been evaluated on several case studies.
Zhou Zhou Linzhang Wang Zhanqi Cui Xin Chen Xin Chen Jianhua Zhao Jianhua Zhao
State Key Laboratory of Novel Software Technology, Nanjing University, Nanjing, P.R.China 210093 Department of Computer Science and Technology, Nanjing University, Nanjing, P.R.China 210093
国际会议
11th IEEE High Assurance Systems Engineering Symposium(HASE 2008)(第十一届IEEE高可信系统工程国际研讨会)
南京
英文
487-490
2008-12-03（万方平台首次上网日期，不代表论文的发表时间）