Companion Web site for our paper in FACS 2012:
The SMV code used to encode the running example (the client's credential disclosure preferences) as a Kripke structure is contained in the following file:
cinet-facs12.smv (plain text, approx. 5K)
To test our method, we randomly generated CI-nets with between 5 and 20 variables and either 5 or 10 statements, then used the Consistency Checker component of our tool to determine which of the randomly-generated CI-nets were consistent. Once 20 consistent CI-nets were identified, we used the Rank Order Generator component of our tool. For each consistent CI-net, we identified the first-best through 25th-best sets of credentials to disclose (with respect to the client's disclosure preferences as modeled by the CI-net). Time and memory usage data were collected each time the underlying model checker, Cadence SMV, was called.
For more information about our tool, please see Section 5 of our paper.
To run the tool on a computer with a current Java Runtime Environment installed:
Note that this tool is primarily meant to explore the feasibility of our proposed approach; we can't guarantee that the software will behave exactly as expected, although it has worked well in our experience. If you do find a bug or if you have any questions about the tool, please let us know via email; we'll do our best to respond.
Each of our charts has versions for CI-nets with 5 statements and 10 statements. We have placed both versions side-by-side for your convenience.
Each line represents the mean value computed over all 20 trials for each combination of variables and statements.
If you have any problems viewing these graphs, please email the site's maintainer, Zach Oster (firstname.lastname@example.org).