Good software design is key to achieve high-quality systems, that satisfy the expected requirements, even when subject to tight operating constraints. Design is particularly important when dealing with safety-critical software, e.g. controlling aircraft or medical devices, where failure to fulfill the expected goals may have catastrophic consequences. In these cases, a clear specification and validation of the underlying concepts and requirements is essential to establish a trustworthy design, prior to its realization in actual code. This constitutes “the most basic form of ‘what’ before ‘how’” [RJ13], a fundamental principle behind good decision making.

Software design usually relies on a modeling language to specify and reason about concepts and requirements. When dealing with critical software, the usage of formal specification languages, supported by rigorous validation and verification (V&V) techniques, is highly recommended. For the past 30 years, the formal methods community have actively researched and developed such languages. Among these, the Alloy language [Jac12] has recently become quite popular due to its so-called “lightweight” approach to formal methods: first, it is based on relational logic, an easy to grasp variant of first-order logic embracing the simple mathematical notion of relation; second, it is supported by a fully automatic SAT based Analyzer, that brings the power of formal V&V to the average software engineer.

While useful for conceptual design, namely to reason about structural properties, Alloy has some shortcomings that prevent its application to the overall process of software design. For example, concerning low-level component design, it provides limited support for direct V&V of temporal properties [Zav12], which was one of the reasons that recently prevented it being the formal language of choice at Amazon [New14]. Also, it does not handle the specificities of high-level software design, in particular it lacks V&V support to reason about software architectures. The overall goal of this project is to tackle these shortcomings and extend Alloy and its Analyzer so that they can be used effectively for fully-fledged, trustworthy software design.

First of all, we intend to tackle Alloy’s shortcomings concerning low-level design. In particular, we intend to combine Alloy’s relational logic with the Temporal Logic of Actions [Lam02], thus achieving a specification language that enables direct reasoning about temporal properties, while retaining the flexibility (so popular among Alloy users) in accommodating various idioms for behavioral specification. Besides defining model-checking procedures for such a combined logic, we will also improve the Alloy’s scenario exploration capabilities, by providing mechanisms that allow the users to quickly target the most revealing scenarios. We also intend to survey existing techniques for unbounded verification of Alloy specifications, and, based on this survey, propose a verification technique that can be used to perform verification in highly critical applications, where the bounded analysis of the Alloy Analyzer is not sufficient.

Concerning high-level design, we intend to focus on three complementary aspects. In several domains it is necessary to design not just one, but a whole family of related software products. To deal with this scenario we intend to extend Alloy to allow variability modeling, and perform V&V over families of related models, namely reason about properties of the whole family at once, or repair a user-sketched or legacy model to fit the specification of the family. It is well-known that several catastrophic failures of software systems were caused by poorly designed interfaces [BBS12]. As such, we intend to propose an Alloy based methodology for this very same purpose, and also develop mechanisms for rapid interface prototyping, relying on symbolic model execution, to allow a complementary empirical validation of the interface design in the presence of real end users. Finally we will also address the fundamental aspect of architectural design, by proposing techniques to orchestrate components and reason about their interaction, namely in presence of probabilistic or continuous behavior. This will allow designers not only to ensure if a requirement is realized by the proposed architecture but also by “how much” it does so.

Rather than deploying all these extensions as separate prototypes, we intend to fully integrate them in a new version of the Alloy Analyzer for trustworthy software design, to be called “Titanium Alloy”, since we expect it to share the excellent properties of such alloys: “high tensile strength and toughness”, but still “light in weight” [Wikipedia]. Summing up, Titanium Alloy will retain the flexible and lightweight approach that made Alloy such a popular language, but strengthen it to tackle other key aspects of software design.