A Runtime Model Checker for Dynamic Software Based on Aspect-Oriented Programming

Increasingly, more and more software systems must make dynamic reconfiguration of their architectures at runtime to adapt to the changing conditions. The runtime verification of architecture evolution is necessary to guarantee the conformance to the specification. In this paper, we propose a runtime model checker that supports dynamic reconfiguration of software architectures taking advantage of linear temporal logic and aspect-oriented programming. The runtime model checker is a concurrent thread with the execution thread of the dynamic software, and is an automaton which can accept exactly the set of executions that satisfy the given specification defined by LTL. So the proposed runtime model checker can monitor and verify the architecture evolution of a dynamic software system continuously at runtime.