The same CFSM model can be model checked against multiple invariants
simultaneously to speed-up CSight.
The same CFSM can be augmented with different invariants to run multiple McScM
instances. A total of N model checking processes can be ran at once. When one
of the processes return safe, start another process to maintain the
parallelization factor. When one of the processes return unsafe, stop all model
checking processes and refine the model.
Original issue reported on code.google.com by bobyan...@gmail.com on 18 Jul 2014 at 5:24
Original issue reported on code.google.com by
bobyan...@gmail.com
on 18 Jul 2014 at 5:24