Clarifications on ComFoRT and MAGIC

MAGIC and ComFoRT are the result of collaboration between Carnegie Mellon’s School of Computer Science (SCS) and the Software Engineering Institute (SEI). Both tools have benefited from this collaboration, with the result that both borrow extensively from each other. However, such borrowing can cause confusion about what “belongs” to ComFoRT and what to MAGIC. Before we can disentangle one from the other, we have to first define what they are:

• [MAGIC] is a software model checker& for concurrent programs written in C.  It is publicly available as MAGIC V1.0. 
• [ComFoRT] is a reasoning framework that combines the Copper model checker (which is based on MAGIC V1.0), with additional superstructure to enable its effective use in component-based software development.

What is not highlighted in this description, however, is that key features of MAGIC V1.0 were developed jointly by the SCS and SEI with the express purpose of supporting ComFoRT.  Confusingly, the results of this collaboration have been presented in the contexts of both tools.  To make matters more confusing, one SEI report referred to the anonymous “ComFoRT model checker,” rather than Copper or MAGIC, because we wanted to emphasize the reasoning framework as whole, not particular pieces of it.

To see the evolution of MAGIC and ComFoRT and how they are related, refer to the figure below. This figure also situates Copper, the model checker being developed at the SEI for use in ComFoRT. Copper is based on the MAGIC V1.0 baseline, but is evolving to satisfy the needs of ComFoRT.  The question of whether or how future versions of Copper and MAGIC will coevolve remains unresolved.