Automatic generation of model checking properties and constraints from production based specification

We propose a technique for automatic generation of environment constraints and component properties used in the constrained model checking (CMC). Beginning from a production based specification of the interface of two components, the tool generates a set of constraints for the interface signals. Industrial model checkers, like formal check can consequently use these constraints and properties to model check the components at each side of the interface separately. In this way, the methodology allows a compositional verification.