Complete formal verification of the PSTM transaction Scheduler

State of the art formal verification is based on formal methods and its goal
 is proving given correctness properties. For example, a PSTM scheduler was
 modeled in CSP in order to prove deadlock-freeness and starvation-freeness.
 However, as this paper shows, using solely formal methods is not sufficient.
 Therefore, in this paper we propose a complete formal verification of
 trustworthy software, which jointly uses formal verification and formal
 model testing. As an example, we first test the previous CSP model of PSTM
 transaction scheduler by comparing the model checker PAT results with the
 manually derived expected results, for the given test workloads. Next,
 according to the results of this testing, we correct and extend the CSP
 model. Finally, using PAT results for the new CSP model, we analyze the
 performance of the PSTM online transaction scheduling algorithms from the
 perspective of the relative speedup.