FORMULA - Modeling Foundations
FORMULA (Formal Modeling Using Logic Programming and Analysis) is a modern formal specification language targeting model-based development (MBD). It is based on algebraic data types (ADTs) and strongly-typed constraint logic programming (CLP), which support concise specifications of abstractions and model transformations. Around this core is a set of composition operators for composing specifications in the style of MBD.
A major advantage of FORMULA is it model finding and design space exploration facility. FORMULA can be used to construct system models satisfying complex domain constraints. The user inputs a partially specified model and FORMULA searches the space of completed models until it finds a globally satisfactory design. This process may be repeated to find many globally consistent designs. Variations on this procedure can be used to prove properties on model transformations and to perform bounded-symbolic model checking.
A major advantage of FORMULA is it model finding and design space exploration facility. FORMULA can be used to construct system models satisfying complex domain constraints. The user inputs a partially specified model and FORMULA searches the space of completed models until it finds a globally satisfactory design. This process may be repeated to find many globally consistent designs. Variations on this procedure can be used to prove properties on model transformations and to perform bounded-symbolic model checking.
People
Publications
- Ethan Jackson, Tihamer Levendovszky, and Daniel Balasubramanian, Reasoning about Metamodeling with Formal Specifications and Automatic Proofs, in MODELS 2011, 2011
- ethan jackson, nikolaj bjorner, and wolfram schulte, Canonical Regular Types, in ICLP (Technical Communications), 2011
- Ethan K. Jackson, Wolfram Schulte, Daniel Balasubramanian, and Gabor Karsai, Reusing Model Transformations While Preserving Properties, in Fundamental Approaches to Software Engineering, 13th International Conference, FASE 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, Springer Verlag, 2010
- Ethan K. Jackson, Eunsuk Kang, Markus Dahlweid, Dirk Seifert, and Thomas Santen, Components, platforms and possibilities: towards generic automation for MDA, in EMSOFT, ACM, 2010
- Ethan K. Jackson and Daniel Balasubramanian, Lost in Translation: Forgetful Semantic Anchoring, in Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering, 16 November 2009
- Ethan K. Jackson and Eunsuk Kang, Generalizing Design Space Exploration, in Under Review, 2009
- Ethan K. Jackson, Wolfram Schulte, Daniel Balasubramanian, and Gabor Karsai, Reusing Model Transformations While Preserving Properties, in Under Review, 2009
- Ethan K. Jackson, Dirk Seifert, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte, and Markus Dahlweid, Specifying and Composing Non-functional Requirements in Model-Based Development, in Proceedings of the 8th International Conference on Software Composition, Springer Verlag, 2009
- Ethan K. Jackson, Wolfram Schulte, and Janos Sztipanovits, The Power of Rich Syntax for Model-based Development, Microsoft Research, 2008
- Ethan K. Jackson and Wolfram Schulte, Compositional Modeling for Data-Centric Business Applications, in Software Composition, Springer, 2008
- Ethan K. Jackson and Wolfram Schulte, Model Generation for Horn Logic with Stratified Negation, in Formal Techniques for Networked and Distributed Systems – FORTE 2008, Springer Verlag, 2008
