Using MDE to Generate Formal Models
- When?
- Thursday 9 December 2010, 14:30 to 15:30
- Where?
- 39BB02
- Open to:
- Staff, Students, Public
- Speaker:
- Mr James Sharp
Formal analysis is based on ensuring that a model preserves particular system properties. Defining the model and specifying the properties requires specialist expertise, the formal model and properties are typically written by hand, based on some informal definition. These definitions range from English written requirements, Unified Modelling Language (UML) models to Domain Specific Language (DSL) descriptions. Our work focuses on the investigation of whether the formal models can be automatically generated from their corresponding informal definition.
Many mappings from the informal definitions to the formal models have repeatable patterns. By identifying these patterns we show that it is possible to use Model Driven Engineering (MDE) techniques to support the automated transformation between the informal and formal.
One of the key aspects of MDE is model transformation. Model transformations can be from model-to-text or model-to-model, these transformations allow for an incremental development of the translation between two different languages to be defined. Using model transformations, it is possible to translate an informal or semi formal language to a formal model for rigorous analysis.
We discuss our work in exploring and evaluating different transformations languages and methodologies, focusing on translations from UML to CSP, and Event-B to CSP; highlighting some of the techniques and methodologies required when not only creating model transformations but also defining the mapping rules between the two languages.
The main contribution of our work lies in a mapping between VHDL and CSP, which is based on the initial work by Neil Evans on identifying a translation from VHDL to CSP||B. We identify our own repeatable patterns for a VHDL to CSP mapping and elaborate on the development of meta-models for both languages, that are required for generating an automated translation between VHDL and CSP using MDE.