A Federated Tooling Framework for Formal Analysis of Simulation Models

This paper presents an integrated tooling framework for the formal analysis of simulation models based on the DEVS-Driven Modeling Language (DDML). DDML, a graphical modeling language inspired by Discrete EVent System Specification (DEVS), defines models at three levels of abstractions and the operational semantics adopts the DEVS simulation protocol. To increase the quality of DDML models, a formal semantics is given by multiple levels of denotational translations to different formal methods (each corresponding to the different levels of abstractions). In these semantic domains, we can take advantage of already existing tools to perform analysis for verification, validation, and accreditation. We present the formal framework of DDML and the methodology for tools integration to automate formal analysis of simulation models. The federation methodology is based on model-driven techniques.