Paper presented at ASE 2021
The team at SESAME partner University of York have presented a technical paper at the 36th IEEE/ACM International Conference on Automated Software Engineering (ASE 2021) highlighting some of their work in the SESAME project. The paper titled: Evolutionary-Guided Synthesis of Verified Pareto-Optimal MDP Policies presents a new approach for synthesising Pareto-optimal Markov decision process (MDP) policies that satisfy complex combinations of quality-of-service (QoS) software requirements. These policies correspond to optimal designs or configurations of software systems, and are obtained by translating MDP models of these systems into parametric Markov chains, and using multi-objective genetic algorithms to synthesise Pareto-optimal parameter values that define the required MDP policies. Use case studies from the service-based systems and robotic control software domains to show that our MDP policy synthesis approach can handle a wide range of QoS requirement combinations unsupported by current probabilistic model checkers. For requirement combinations supported by these model checkers, the approach was shown to generate better Pareto-optimal policy sets according to established quality metrics.