Project Tuva Enhanced Video Player

Formal Modeling with Formula

	FORMULA (Formal Modeling Using Logic Analysis) analyzes domain-specific modeling languages (DSMLs) and model transformations that are expressed in logico-algebraic framework. For example, the "domain" of a DSML is characterized by a term algebra and a set of invariants over sets of terms. Similarly, model transformations can be expressed as axioms that map set of terms from one domain to sets of terms of another domain. FORMULA uses these descriptions to calculate models that satisfy (or do not satisfy) these axioms. This basic capability can be used to determine properties of DSMLs/transformations such as domain equivalence, domain emptiness, and structure preserving maps.

FORMULA (Formal Modeling Using Logic Analysis) analyzes domain-specific modeling languages (DSMLs) and model transformations that are expressed in logico-algebraic framework. For example, the "domain" of a DSML is characterized by a term algebra and a set of invariants over sets of terms. Similarly, model transformations can be expressed as axioms that map set of terms from one domain to sets of terms of another domain. FORMULA uses these descriptions to calculate models that satisfy (or do not satisfy) these axioms. This basic capability can be used to determine properties of DSMLs/transformations such as domain equivalence, domain emptiness, and structure preserving maps.

Examples of Formula Features

Formula is a language for formally capturing modeling abstractions and model transforations through structured logic programming. In Formula an abstraction layer is called a "domain". A domain contains a set of data types (typed free-constructors) for capturing the concepts of an abstraction layer. Encapsulated within a domain are also logical statements (horn clauses) that explain how the modeling concepts are related to each other. Please see this paper for a more detail description of BAM concepts.

Formula also provides a mechanism to specify the relationships between abstraction layers using "model transformations". A model transformation is rewriting procedure that converts the data structures from one domain into the data structures of another domain. These transformations are also expressed using horn clauses to specify the rewriting procedures. This approach permits formal analysis of the model transformations taking into account the properties of the abstraction layers.

New User Interface

FORMULA is primarily an analysis tool; the new UI helps to better manage the results of analysis. The figure below shows a screenshot of the new UI: The left-hand side of the window shows the domains, transformations, and models that make up a project. Objects can extend other objects, and this is also shown in the tree-view. The bottom panel is a simple message window that contains important notifications. Finally, the main part of the UI is an embedded browser. Whenever objects are added to the project or proof tasks are executed, a website is dynamically generated that represents the new data. These dynamic websites are viewable through the embedded browser, and can access functionality in FORMULA. Additionally, the generated website can be posted to the web for documentation purposes without any additional libraries or components.