https://www.mdu.se/

Autonomous systems are supposed to automatically plan their actions and execute the plan without human intervention. In this paper, we propose a model-based two-layer frame-work for policy synthesis and test-case generation for autonomous systems. At the high-level layer of the framework, we have two kinds of methods for synthesising policies whose correctness is guaranteed by model checking. The autonomous system's controller executes synthesised policies at the low-level layer. As the kinematics of autonomous systems is often nonlinear and the environment may influence the results of their actions, formally verifying the controllers is extremely difficult. We propose a novel method for generating test cases for the controllers at the low-level layer. The method employs reinforcement learning for test-case generation and model checking to ensure that the test cases faithfully realise the execution of the policy. The framework is designed in Uppaal Stratego, which integrates model checkers and algorithms for policy synthesis. Therefore, the framework separates concerns and seamlessly interchanges the information between two layers.