Add support for a model checker that supports checking of CFSMs with bounded queues.

chubbymaggie / synoptic

Automatically exported from code.google.com/p/synoptic

0 stars 0 forks source link

Add support for a model checker that supports checking of CFSMs with bounded queues. #278

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago

McScM does not support bounded queues checking. For performance, and in some 
cases for tractability, it is necessary to be able to check a CFSM with a bound 
on the length of the queue. The SPIN model checker can do this, as well as Cadp 
and UPPAAL. We have to evaluate which one of these suits Dynoptic best.

Original issue reported on code.google.com by bestchai on 11 Nov 2012 at 8:26