Formal Analysis for Discrete Optimisation Problems Based on Model Checker SPIN

Model checking is to check whether a bounded state system meets their design specifications using state-space search approach automatically. Model checker to solve discrete optimisation problems can first be used to verify that the model of the problem is correct. Subsequently, the same model can be used to find an optimal solution for the problem. It is described how to use Promela primitives to build model and show how branch-and-bound approaches can be added to the LTL property. The LTL property is dynamically changed during the verification which can reduce the transition of model space and make the search more efficiently. The method above is elaborated correctly using the case study.