请问openEuler在验证多线程等问题时用什么做model checking?

请问openEuler在验证多线程等问题时用什么做model checking?