Product Line Verification via Modal Meta Model Checking

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 (CFMTSs) can be regarded as loose specifications of meta models, and modal refinement as a way to increase the specificity of allowed domain specific languages (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. The paper illustrates the impact of M3C in an industrial setting where well-formed documents serve as contracts between a provider and its customers in two steps: it establishes CFMTS as a formalism to specify product lines of document description types (DTDs – or related formalisms like JSON schema), and it shows how M3C-based product line verification can be used to guarantee that violations of essential well-formedness constraints of a corresponding user document are detected by standard DTD-checkers. The resulting hierarchical product line verification allows Creios GmbH, a service provider for E-commerce systems to provide a wide range of tailored shop applications whose essential business rules are checked by a standard DTD-checker.