search

ModelInference / synoptic

Inferring models of systems from observations of their behavior
Other
81 stars 25 forks source link

Adding SPIN model checker support to CSight #375

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
We are enhancing CSight by utilizing SPIN as a model checker. As a model 
checker, SPIN is also used to verify models. However, SPIN allows us to set a 
maximum length of the communication channels. With this limit, SPIN can avoid 
running without termination. However, this tradeoff prevents us from 
guaranteeing that the model is valid for any channel length greater than the 
limit specified. The user will still be able to use McScM as the model checker 
if they choose to.

This requires that Issue 374 be in a working state so the Promela can be used 
here.

Original issue reported on code.google.com by Kenneth....@gmail.com on 5 Jun 2014 at 11:48

GoogleCodeExporter commented 9 years ago 
Most of the functionality ended up in Issue 374. 

This is now a duplicate and closed.

Original comment by Kenneth....@gmail.com on 3 Jul 2014 at 5:19