Equivalence Classes in Performance Evaluation Programming

In recent work we have introduced performance evaluation programming - a programming paradigm supporting performance analysis and formal verification of concurrent programs. For software verification the ranges of variables must be bounded, and programs are translated into finite-state continuous-time Markov chains verified formally by using probabilistic model checking techniques. Our present aim is to increase the size of the state space of programs that can be verified formally. The solution investigated in this paper is inspired by equivalence partitioning - a well-known software testing technique. We provide experimental results showing that, by partitioning the state space of concurrent programs into behavioral equivalence classes, the performance evaluation programming paradigm can be used to design and verify formally concurrent programs with large state spaces.