An Introduction to Modelling Notations in Model Based Software Engineering: Alloy & Statecharts

In this post, I’m going to briefly describe two notations for models that are popular in model based software engineering. The first, Alloy, is a relatively new language while the second, statecharts, are much older.

Alloy was developed by Daniel Jackson at MIT, who published the first paper on the language in 2001, titled “Alloy: a lightweight object modelling notation.” Jackson created the language as a tool for lightweight formal methods: reduced cost formal methods with the benefits of “traditional” formal methods. Heavily inspired by Z, Alloy is a small expressive, declarative, language that can express useful structural properties of models. That means Alloy is designed for models that model what affects are achieved, rather than models that model how such affects are achieved. Primarily a model-finder (rather than a model-checker), Alloy, through the use of the Alloy Analyzer, finds and displays state snapshots of models. Such snapshots can be considered pre- and post-states, allowing Alloy to describe the behaviour of models. A user can constrain the outputs to instances that satisfy predicates.

The Alloy Analyzer is a tool used to find instances of the system modeled (typically constrained by predicates), as well as find counter-examples to assertions regarding the model. Asserts are written in the model and the Analyzer will check exhaustively for instances that satisfy the model constraints and violate the assertion. This is done through restricting the scope of the instances to be checked. The Analyzer will exhaustively search every possible instance where there is at most scope number of elements in each set of objects. Jackson’s motivation for this is his small scope hypothesis: most errors do not require many instances of objects, and can be found by considering relations on only a few objects. Thus a scope of 3 or 4 will often reveal flaws in models, and since the Analyzer is complete and sound, all such errors with at most 3 (or 4) objects of each type will be reported and the Analyzer won’t report any false negative. On a typical computer, such a search is quick (a few milliseconds for small models) but with larger models and slower machines this can vary. Interestingly, the Analyzer works by translating the model and constraints to a long SAT formula, which is then fed to an off-the shelf SAT solver, capitalizing on the research advances in solving SAT problems. This means performance gains are possible by switching the underlying SAT solver. The Analyzer also supports the generation of metamodels and themes, to customize how model instances (and metamodels) are displayed.

The language itself has both a graphical and textual syntax, though the use of the Analyzer requires textual input. Alloy has no explicit types, and is built on sets and relations. It should be noted that the (textual) syntax of the language has changed greatly since Jackson’s first paper. A tutorial for Alloy can be found here.

In contrast to Alloy, Statecharts are older and much more familiar (provided the reader has any background in modelling or more generally, software engineering). Statecharts were introduced in 1987 by David Harel. A primarily graphical system of modelling systems, statecharts look similar (though often more complicated than) finite state machines. Harel’s goal in designing statecharts was to have a system that could represent concurrency, allow grouping of common actions, and present different levels of abstraction while ensuring all properties were formally defined. Though statecharts look similar to finite state machines, they often have many new features that Harel introduced: superstates, that allow for state composition and a state to have a substate; (deep) history to allow the system to remember what substate it is in when the superstate exits; conditional and selectional connectives to control the flow of the machine entering a state with substates; actions and activities: processes run by the system which are instantaneous and long-lived, respectively; timeouts and more. By using superstates, the level of abstraction can vary: the contents of the superstate may not be required for someone looking at the big picture, while particular developers can expose and inspect the superstate’s internals.

The full paper on statecharts, though dated, is an excellent introduction. Statecharts do have pitfalls though, and the paper mentions at least two. They are not particularly suited for simultaneous events (though concurrent events are supported, and thus many simultaneous events are modeled quite well, however, not all simultaneous event are suited for statecharts), and there are occasionally possibilities of non-determinism that are cause for concern. More current research may have formalized resolutions for these problems, but I don’t have any references to confirm this, and I suspect that often modelers simply agree on a behaviour if an inconsistency might arise.


References

Jackson, D., Alloy: a lightweight object modelling notation. In ACM Transacitons on Software Engineering and Methodology, 11(2): 256-290 (Apr. 2002).
Jackon, D. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006.
Harel, D., Statecharts: A visual formalism for complex systems, In Science of Computer Programming 8(3):231-274, (June 1987).

Tags: ,

Leave a Reply