Using Abstraction in the Verification of Simulation Coercion

Simulation coercion concerns the adaptation of an existing simulation to meet new requirements. Interactions among course-of-action options available during coercion can become sufficiently complex that full verification of the simulation as it is adapted becomes cost-prohibitive. To address this issue we introduce two forms of abstraction, as employed in the model-checking community, to support verification of critical features of the simulation. We extend existing abstraction methods to facilitate our goals, and propose a useful abstraction method based on partial traces. As a case study, we apply our abstraction methods to the verification of a coercion of an existing simulation.