Visiting lecture - "An Introduction to FORMULA" with Ethan Jackson, Microsoft Research

04/23/2009 12:00 pm
04/23/2009 1:00 pm


Thursday at noon, Ethan Jackson from Microsoft Research will give a lecture on his continuing work on model-based design and formal methods in the Large Conference Room.



Model-based development (MBD) is a methodology for designing complex software systems. Central to this approach are domain-specific abstractions and model transformations. Domain-specific abstractions are used to specify and decompose functional and non-functional requirements. Model transformations translate models from one abstraction layer to another. Together, these tools allow heterogeneous systems to be formally modeled, composed, and refined.

The success of MBD rests on general techniques for rapidly specifying and reusing both domain-specific abstractions and model-transformations. For example, domain-specific abstractions can be viewed as special-purpose specification languages, called domain-specific modeling languages (DSMLs). Similarly, model transformations can be viewed as compilers from one language syntax to another. This perspective exposes the challenge in more familiar terms: Provide tools for rapidly engineering new formal specification languages and reusing compilers between them.

In this presentation I will talk about a language called FORMULA, which has been developed to support the formal specification, reuse, and composition of DSMLs and model transformations. FORMULA is unique in a number of ways: First, it uses logic programming as formal framework for integrating domain invariants and model transformations. Second, it provides correct-by-construction operators that make semantic guarantees on DSML compositions. Third, it is designed to give the modeler access to many mathematical theories in the sense of the Nelson-Oppen technique for combining decision procedures. During this presentation I will introduce its concepts and briefly discuss two interesting results: A technique for separately specifying and composing non-functional requirements, and a technique for automatically lifting model transformations.