Formal Modeling Using Logic Analysis
Introduction
FORMULA (Formal Modeling Using Logic Analysis) is a unified framework for specifying domain-specific languages (DSLs) and model transformations. FORMULA allows modeling artifacts to be specified using logic programming (LP) extended with structuring and composition operators. This approach provides a formal foundation for the structural semantics of DSLs, which are non-operational, and the operational semantics of graph-like rewriting procedures, which arise in model transformations. FORMULA provides formal analysis of these model artifacts by means of a model finding procedure implemented on top of the SMT solver Z3. The tool also generates code for executing model transformations and testing if a model conforms to the structural semantics of a DSL.
- 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, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner, and Wolfram Schulte, Specifying and Composing Non-functional Requirements in Model-Based Development, in Proceedings of the 8th International Conference on Software Composition, 2009
- Ethan K. Jackson, Wolfram Schulte, Daniel Balasubramanian, and Gabor Karsai, Reusing Model Transformations While Preserving Properties, in Under Review, 2009
- Ethan K. Jackson and Eunsuk Kang, Generalizing Design Space Exploration, in Under Review, 2009
- Ethan K. Jackson, Wolfram Schulte, and Janos Sztipanovits, The Power of Rich Syntax for Model-based Development, 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 FORTE, Springer, 2008
