Comet: A configuration management tool for formal modeling

In this paper, we report on our experience in designing Comet, a tool to support verification goals that require exploration of multiple model configurations and options. Comet helps us track the various runs we have made using Spin: it provides us with various visualizations and the ability to easily schedule a new run with point-and-click parameters. Our work on Comet is motivated by the observation that verification through model-checking is a complex process even after a model is built and properties are defined, where an analyst typically must navigate a difficult parameter space that involves both model configurations and tool options. Comet supports an analyst in this run, analyze, choose-next-run cycle.