Author Archives: Alcino Cunha

Model-checking graph properties using Alloy

While developing an algorithm for fast distributed computation of a graph diameter and radius, some of my colleagues had a conjecture about graph topology that, if true, would enable an aggressive optimization of the algorithm.

In order to understand the conjecture we must first recall some (more or less) standard graph theory definitions:

  • The distance between two nodes is the length of the shortest path between them;
  • The eccentricity of a node is the greatest distance between that node and all others;
  • The diameter of a graph is the maximum eccentricity found in the graph;
  • A node is peripheral if its eccentricity is equal to the diameter;
  • The antipode of a node is the set of nodes at distance equal to its eccentricity.

Given a non-directed connected graph the initial conjecture was:

For every node, all nodes in its antipode are peripheral.

They quickly found a counter-example to this conjecture and relaxed it to the following:

For every node, some node in its antipode is peripheral.

For a long time they were not able to prove or refute this conjecture. At some point I was involved in the discussion and decided to model-check it using Alloy before attempting any proof.

Continue reading

Translating Alloy Specifications to UML Class Diagrams Enriched with OCL

Just accepted to SEFM’11 🙂 Joint work with Ana Garis and Daniel Riesco.

Abstract: Model-Driven Engineering (MDE) is a Software Engineering approach based on model transformations at different abstraction levels. It prescribes the development of software by successively transforming
models from abstract (specifications) to more concrete ones (code).
Alloy is an increasingly popular lightweight formal specification
language that supports automatic verification. Unfortunately, its
widespread industrial adoption is hampered by the lack of an
ecosystem of MDE tools, namely code generators. This paper presents
a model transformation between Alloy and UML Class Diagrams enriched
with OCL. The proposed transformation enables current UML-based
tools to also be applied to Alloy specifications, thus unleashing
its potential for MDE.


Welcome to the HASlab blog.