Validation and Verification of an UML/OCL Model with USE and B: Case Study and Lessons Learnt

Runtime adaptations of applications generate new risks of bugs and unpredicted interactions that may lead the application execution to an unsafe state. Although execution supports are enough mature to implement such adaptation mechanisms, there is still a lack of formal foundations to support such a process. Our work consists in adopting a Model Driven Engineering approach to express adaptation safety independently of execution supports. In this paper we present our experiments in using traditional validation and verification techniques to ensure the correctness of an adaptation safety model in a practical and rigorous way.