Automated Formalisation for Verification of Diagrammatic Models

Software engineering uses models to design and analyse systems. The current state-of-the-art, various forms of model-driven development, uses diagrams with defined abstract syntax but relatively-lose translational approaches to semantics, which makes it difficult to perform rigorous analysis and verification of models. Here, we present work-in-progress on tool support for formal verification of diagrammatic models. The work builds on Amálio's rigorous template-based approach to formalisation, which formally expresses the intended semantics of both the diagram notation and modelled system, along with standard correctness conjectures and, in many cases, proof of these conjectures.