The main goal of this project is to develop a methodology for trustworthy software design that is both formal, unified, and lightweight. By "formal" we mean a methodology that is based on a specification language with a precise semantics and supported by rigorous V&V techniques. By "unified" we mean a methodology that covers many key aspects of software design with a single unifying formalism and an integrated toolset. And by "lightweight" we mean a methodology that is (a) easy to grasp by software engineers, allowing them to quickly capture the essence of the system under design, (b) flexible to adapt to their prefered styles of specification and (c) supported by automated V&V, the all-important ingredient in any trustworthy design. In short, we want to develop a methodology that has some of the key features that industry seeks when choosing a design language and methodology: be able to "handle very large, complex or subtle problems", "minimize cognitive burden", and have "high return on investment".

Many design methodologies and languages have been proposed in the past, but we believe none of them achieved the right blend of the three characteristics stressed above. Either they are too informal, or they focus on a very specific aspect of design, or they are not lightweight, namely not supported by automated V&V tools. A particular formal specification language that excels in two of these characteristics, namely, being both formal and lightweight, is Alloy. Alloy is a formal modeling language based on relational logic, a variant of first-order logic where predicates can be combined using relational operators, further extended with transitive closure to allow the specification of reachability properties. This so-called relational logic is quite easy to grasp, and allows a very simple specification style, quite often resembling natural language. Alloy is also supported by an Analyzer that enables model validation and automatic (bounded) verification by translation to off-the-shelf SAT solvers. The tool finds examples and counterexamples that are depicted visually, greatly simplifying the design validation process. Due to this powerful combination of formality and lightweightness, Alloy has become increasingly popular in recent years.

Unfortunately, while great for conceptual design, namely to specify and reason about structural properties, Alloy still has some shortcomings that difficult its application to other aspects of software design. Thus, to achieve the above stated goal, we plan to extend Alloy and its Analyzer with several new features, such as, temporal logic to allow the specification of dynamic properties, support for variability modeling, support for the specification and verification of software architectures, a more efficient verification engine, or better support for scenario exploration.




  1. Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, and Denis Kuperberg: Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. To appear in FSE'16.
  2. Denis Kuperberg, Julien Brunel, David Chemouil: On Finite Domains in First-Order Linear Temporal Logic. To appear in ATVA'16.