Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
FORMULA - Formal Modeling Using Logic Programming and Analysis
Download FORMULA, or click the online button to try a limited version online (does not require installation). FORMULA is supported for 32-bit/64-bit Windows 7 machines and requires Visual Studio 2010. The current version of FORMULA requires Visual Studio 2010 (at least the Professional Edition), or the Visual Studio 2010 Isolated Shell.

Note: By installing, copying, or otherwise using this software, you agree to be bound by the terms of its license. Read the license.

For questions/comments please send email to formula@microsoft.com, or join our user-discussion mailing list: join-formula@list.research.microsoft.com.

Release date: 9/26/2011
Release notes: Click to download notes
Release summary: Optimizations, improved cardinality inference, support for VS isolated shell, and bug fixes. Please see the release notes for feature summary and limitations.
All versions:
FORMULA Version 1.3.15450.0 (9/26/2011)
Optimizations, improved cardinality inference, support for VS isolated shell, and bug fixes. Please see the release notes for feature summary and limitations.
FORMULA Version 1.2.11228.0 (6/16/2011)
Optimizations, improvements in VS integration, and bug fixes. Please see the release notes for feature summary and limitations.
FORMULA Version 1.1.6700.0 (4/8/2011)
First public release version of FORMULA. Please see the release notes for feature summary and limitations.

Release date: 8/31/2011
Documentation summary: Slides presented for ICTAC 2011 School.
Full description:
These slides where presented at the ICTAC 2011 school in Johannesburg, South Africa. The are three parts to this tutorial:
Part I - Introduction: Introduces FORMULA and its approach to automated formal methods for formal modeling.
Part II - Domains and Models: Explains how to specify abstractions and build models using these abstractions. Shows how to synthesize models for design space exploration and test-case generation.
Part III - Composing and Transforming: Explains how to formally compose abstractions and to build model transformations across domains. Shows how to prove correctness properties on transformations.

Use the links belows to explore examples of FORMULA specifications. Click the "online" button to try the example online (when available). The first couple of examples encode interesting problems arising in graph theory. From the perspective of model-based development, constraints on model construction can often contain these subproblems.
Release date: 4/8/2011
Example summary: Encodes a map coloring problem.
Full description:
Encodes a map coloring problem for several countries in Western Europe. Demonstrates constructors, enumeration types, model conformance, and partial models.
Release date: 4/8/2011
Example summary: Encodes arbitrary graph coloring problems.
Full description:
Graph coloring is an abstract version of map coloring. Unlike the previous map coloring example, which was specific to Western Europe, this example encodes the coloring problem once and for all (for a fixed set of colors). Then partial models encode various problem instances.
Release date: 4/8/2011
Example summary: Finds Eulerian walks in a graph.
Full description:
This example finds a walk W, which is a sequence of edges in graph (W = (v0, v1), (v1, v2), (v2, v3), ...). such that every edge in the graph appears in the walk exactly once. This example uses LP rules to keep track of edges that have been used in a solution. It also uses arithmetic to label the edges in the sequence.
The next set of examples use arithmetic constraints in deeper way than the previous graph-theoretic examples. These demonstrate some classic CSP problems.
Release date: 4/8/2011
Example summary: Assign digits to the variables m, o, r, e, n, y such that send + more = money.
Full description:
This is a classic constraint problem originating from cryptography: Given the variables m, o, r, e, n, y, assign each variable a value in the interval [0,9] such that send + more = money. This is subject to the additional constraints that s and m should be non-zero and that every variable should have a distinct value. In this example we utilize the order-sorted type system of Formula to encode the digits [0,9] and positive digits [1,9] as two sets. These type constraints are enough to ensure that variables take values in the desired range.
Release date: 4/8/2011
Example summary: Place N queens on an NxN chess board so that no queen can take another.
Full description:
Place N queens on an NxN chess board so that no queen can take another. Arithmetic constraints are used to explain when queens can attack along a diagonal. This version of N queens allows the size of the board to be specified using the constructor Size(). Thus, problem instances of arbitrary size can be encoded. Finally, the usual optimization that only the row positions need to be solved is obtained by specifying are partial model where the column values are fixed.
Release date: 4/8/2011
Example summary: Schedule sets of tasks across machines.
Full description:
The job shop scheduling problem: There are "jobs" and each job owns a set of "tasks". Tasks within a job are totally ordered and each task takes some amount of time to execute. Also, there are "machines" and each machine can only execute one task a time. The problem is to find a schedule assigning a start time and machine to each task such that all tasks run in order and no machine runs two tasks at the same time.
These examples encode small platform-mapping problems found in MBD. Even though these are relatively simple, they may contain difficult constraint problems similar to the above examples. They also make deeper use of the FORMULA module system to compose specifications.
Release date: 4/8/2011
Example summary: Map a tree of communicating components onto a set of nodes.
Full description:
Often embedded architectures are modeled as a tree of components that can be wired together. To make the example more interesting there is a special type "System" used for root of the tree. Union types are used to express rules that are agnostic to this distinction. The mapping problem is to place components onto a network of nodes that can support the communication requirements of components. This requires computing the transitive closure of node connectivity.
Release date: 4/8/2011
Example summary: Deploy a set of tasks on a balanced network of nodes.
Full description:
The software architecture is modeled as a set of tasks that are in conflict. Two tasks in conflict cannot be placed on the same node. These constraints form a graph coloring problem. Furthermore, nodes are connected by directional channels with fixed communication capacities. Anytime a node has both incoming and outgoing channels, then the in and out capacities must be balanced. Finally, no node can support more than two incoming and two outgoing channels.
These are some examples of model-checking problems. We are in the process of building direct model checking facilities into FORMULA, but it isn't released yet. In the meantime, many model-checking problems can be rephrased as modeling finding problems on domains. Requires the latest version of FORMULA.
Release date: 6/16/2011
Example summary: A farmer has a conundrum.
Full description:
This is the problem:
(1) There is a chicken, a fox, a bag of grain, a farmer, and a boat.
(2) Initially all these things are on the left side of a river bank.
(3) The farmer wants to take everything to right side of a river bank,
(4) But the farmer can only fit one additional object in the boat at a time,
(5) And if the chicken is left alone with grain it eats all the grain,
(6) And if the fox is left along with the chicken it eats the chicken.
How does the farmer move everything with anything being eaten?
Metamodeling frameworks allow the specification of DSL sytnax via metamodels. This example specifies a small metamodeling framework based on typed graphs. It uses model finding to prove properties about the framework.
Release date: 6/16/2011
Example summary: A farmer has a conundrum.
Full description:
This is the problem:
(1) There is a chicken, a fox, a bag of grain, a farmer, and a boat.
(2) Initially all these things are on the left side of a river bank.
(3) The farmer wants to take everything to right side of a river bank,
(4) But the farmer can only fit one additional object in the boat at a time,
(5) And if the chicken is left alone with grain it eats all the grain,
(6) And if the fox is left along with the chicken it eats the chicken.
How does the farmer move everything with anything being eaten?
 > Projects  > Formal Modeling with FORMULA  > Explore FORMULA