M3C: Modal Meta Model Checking

M3C is a method and tool supporting meta-level product lining and evolution that comprises both context free system structure and modal refinement. The underlying Context-Free Modal Transition Systems can be regarded as loose specifications of meta models, and modal refinement as a way to increase the specificity of allowed DSLs by constraining the range of allowed syntax specifications. Model checking with M3C allows one to verify properties specified in a branching-time logic for all DSLs of a given level of specificity in one go, which is illustrated by looking at variations of an elementary programming language. Technically, M3C is based on second-order model checking which determines how procedure calls affect the validity of the properties of interest. The inherent compositionality of the second-order approach leads to a runtime complexity linear in the size of the procedural system representation, whose corresponding transition systems typically have infinitely many states. In fact, second-order model checking can be regarded as a means to tame state explosion via 'procedural abstraction', a technique which may well be beneficial also for regular (recursion-free) systems.