Alcino Cunha and Nuno Macedo, INESC TEC researchers, contributed to the development of Alloy 6, the latest version of one of the most used specification and analysis platforms for the formal analysis of designs in the early stages of software development.
This new version of the language presents new primitives that allow specifying, validating, and verifying behavioural models in a native way. The Alloy’s analysis techniques have also been extended to support this type of analysis, as well as the viewer that presents instances during validation.
Alloy, initially developed by MIT, can be used to model and analyse all types of systems, but is mainly useful in systems with complex structural properties, such as distributed protocols or systems with highly configurable architectures. Being based on a simple, expressive logic, focused on the notion of relationships, and being supported by automatic formal analyses, Alloy is quite useful for quickly exploring different design options, as well as verifying that the expected behaviour is guaranteed.
The advantage of Alloy 6 is that it allows combining structural and behavioural analyses – which, until now, needed to be coded manually. This extension also preserves Alloy’s simplicity and flexibility, making it the ideal platform for analysing the design of systems with significant structural and behavioural properties.
High-Assurance Software Laboratory (HASLab) researchers, together with a team of researchers from ONERA (French Aerospace Laboratory), developed this extension to Alloy as an independent tool, Electrum, within the scope of the TRUST research project. Moreover, and after the acknowledgement of the scientific community, this extension was integrated into the official distribution of Alloy.
The INESC TEC researchers mentioned in this news piece are associated with UMinho and UP-FEUP.
News, current topics, curiosities and so much more about INESC TEC and its community!
