Integration of Runtime Verification into Metamodeling

Modeling is a well-established practice in the development of big and complex software systems. Domain Specific Modeling Languages (DSMLs) are a technique used for specifying such systems in an abstract way. These languages define the structure, semantics and constraints for models related to the same application domain. The models created with DSMLs are then interconnected or related to one another. Among the reasons for tailoring a language to the problem space is their better understandability by domain experts, capacity for high-level abstraction, and user friendliness. However, the use of DSMLs (like the use of types in general) does not shield the produced software from bugs or man-made mistakes. Software failures may still occur on complex systems due to a variety of reasons such as design errors, hardware breakdown or network problems. Ruling out these failures requires that verification methods that guarantee correct execution even in corner cases are integrated into the development process. We previously presented our ideas for integrating specifications tighter with the model [4]. We improve on our realisation in the context of behavioural models for embedded systems [6], and now tackle modelling and specification of a distributed system. LEGO MindStorm R robots serve as the platform for a small case study.