The final day of this year's Real Time Linux
Workshop (RTLWS) had talks from a number of different researchers and others
from the realtime Linux community. It also featured a talk from outside of
that community, but on a topic—as might be guessed—that may be
important to users and developers of realtime systems: modeling system
behavior for better reliability. Eunsuk Kang from MIT gave an introduction to
the Alloy language, which has
been used to model and find bugs in systems ranging from network protocols
RTLWS organizer Nicholas Mc Guire prefaced the talk by noting that "Z" is used
modeling and design verification, but that there is no free Z support.
Alloy, on the other hand, is similar to Z, but is free software. The
availability of a free alternative will make this kind of analysis more
Kang is part of a group at MIT that focuses on how to build more reliable
software, which is the motivation behind Alloy. Software design often
starts with sketches, then moves into creating design documents in various
formats. "Is this the best way to design software?" is one question to
ask, he said.
Sketches are good because they are lightweight and informal. That allows
people to brainstorm and to quickly prototype ideas. Documents are much
more heavyweight and are geared toward completeness. But those documents
can't be used to answer questions about the design, nor to determine
whether the system design is consistent.
So, they set out to create a new language that is "simple" and
would be easy to learn, so it would impose a low burden on its users. It
could be used in a step between sketches and design documents. The language
would be "precise and analyzable", so that one could ask questions
about the system described. The language and tools would provide instant
feedback in support of rapid prototyping. That new language is Alloy.
As a demonstration of Alloy and its development environment, Kang created a
model of a filesystem in the language. The model consisted of several
different kinds of objects, such as files, paths, and filesystems, as
well as operations for things like adding and deleting files. The model
describe the implementation of the filesystem, just the relationships between
the objects—and how they change based on the operations.
The model can then be "run" in the GUI. There is a built-in visualization
component, which shows solutions that satisfy the constraints set out in
the model. One can add assertions to the model, which can either be
confirmed to a certain search depth or a counterexample can be found.
Alloy is, in many ways, a descendant of languages like Prolog and
automated theorem proving systems.
In the demo, Kang's seemingly reasonable model was missing a key
constraint. Alloy was able to find a counterexample to an
assertion because the model did not preclude multiple file objects having
the same path. Once the add-file operation was changed to eliminate that
possibility, no counterexample to the assertion (which essentially stated
that the delete operation undoes the add operation) could be found.
Alloy has a small number of constructs, purposely. It is a declarative
language that describes the system, but, importantly, not the
implementation, in "pure first-order logic". Alloy allows for two different
kinds of analysis, Kang said, simulation or assertion. The models get
translated into a "constraint solving engine" that can find problems that
Standard software testing tries to cover as many different behaviors of the system as
possible, but one of its weaknesses is that it can't show the absence of
bugs. The analyzer in Alloy is exhaustive, and can be used to "verify very
deep properties" about the model, he said. The analyzer allows the
designer to "reason about the behavior" of systems.
That kind of reasoning has been done using Alloy, Kang said, both by his
group and other researchers and universities. One of his examples was not
computer-related, instead concerning the beam-scheduling policies for
radiation therapy at Massachusetts General Hospital. There are multiple
treatment rooms, where several different kinds of requests for radiation
from a single cyclotron can be made. There are multiple doctors and nurses
making the requests, which get funneled to a master control room that
enforces various safety requirements. By modeling the system, several race
conditions and other problems were found that had the potential to silently
In addition, Stanford and Berkeley have applied Alloy to web security
protocols and found previously unknown vulnerabilities in HTML 5 and
WebAuth. In fact, researchers using Alloy have found problems in protocols
that had previously been "proved" correct. Pamela Zave analyzed the Chord
peer-to-peer distributed hash table protocol, which had proofs of its
correctness in one of the most cited papers in computer science, Kang
said. But Zave found that it is not correct according to its
specification, and that six properties believed to be true were not.
There are lots of other examples, he said, including smart card security,
the flash filesystem for a Mars rover, and Java virtual machine security.
What his group has found is that by using Alloy one will often "find very
results". There is ongoing work to generate test cases for the actual
implementation from the models to help ensure that the code matches the
There are also efforts to generate code from the models, but it is a
Going the other way, from existing code to models, is even more difficult.
It is far more efficient to start modeling at the design stage,
Kang said. The key observation from the team is that spending the time to
model a system (or a portion of a larger system) is worth it because it
will uncover "a lot of surprises". Those surprises are typically bugs, of
course, so finding them—early or late—can only lead to better
[ I would like to thank the RTLWS and OSADL for travel assistance to attend
the conference. ]
to post comments)