Nuno Macedo

Nuno Macedo, Hugo Pacheco

Many properties related to security or concurrency must be encoded as so-called hyperproperties, temporal properties that allow reasoning about multiple traces of a system. However, despite recent advances on model checking hyperproperties, there is still a lack of higher-level specification languages that can effectively support software engineering practitioners in verifying properties of this class at early stages of system design. Alloy is a lightweight formal method with a high-level specification language that is supported by automated analysis procedures, making it particularly well-suited for the verification of design models at early development stages. It does not natively support, however, the verification of hyperproperties. This work proposes HyperPardinus, a new model finding procedure that extends Pardinus -- the temporal logic backend of the Alloy language -- to automatically verify hyperproperties over relational models by relying on existing low-level model checkers for hyperproperties. It then conservatively extends Alloy to support the specification and automatic verification of hyperproperties over design models, as well as the visualization of (counter-)examples at a higher-level of abstraction. Evaluation shows that our approach enables modeling and finding (counter-)examples for complex hyperproperties with alternating quantifiers, making it feasible to address relevant scenarios from the state of the art.

André Santos, Alcino Cunha, Nuno Macedo

This tool paper presents the High-Assurance ROS (HAROS) framework. HAROS is a framework for the analysis and quality improvement of robotics software developed using the popular Robot Operating System (ROS). It builds on a static analysis foundation to automatically extract models from the source code. Such models are later used to enable other sorts of analyses, such as Model Checking, Runtime Verification, and Property-based Testing. It has been applied to multiple real-world examples, helping developers find and correct various issues.

Julien Brunel, David Chemouil, Alcino Cunha et al.

Most model checkers provide a useful simulation mode, that allows users to explore the set of possible behaviours by interactively picking at each state which event to execute next. Traditionally this simulation mode cannot take into consideration additional temporal logic constraints, such as arbitrary fairness restrictions, substantially reducing its usability for debugging the modelled system behaviour. Similarly, when a specification is false, even if all its counter-examples combined also form a set of behaviours, most model checkers only present one of them to the user, providing little or no mechanism to explore alternatives. In this paper, we present a simple on-the-fly verification technique to allow the user to explore the behaviours that satisfy an arbitrary temporal logic specification, with an interactive process akin to simulation. This technique enables a unified interface for simulating the modelled system and exploring its counter-examples. The technique is formalised in the framework of state/event linear temporal logic and a proof of concept was implemented in an event-based variant of the Electrum framework.

Hugo Pacheco, Nuno Macedo

Robotics is incredibly fun and is long recognized as a great way to teach programming, while drawing inspiring connections to other branches of engineering and science such as maths, physics or electronics. Although this symbiotic relationship between robotics and programming is perceived as largely beneficial, educational approaches often feel the need to hide the underlying complexity of the robotic system, but as a result fail to transmit the reactive essence of robot programming to the roboticists and programmers of the future. This paper presents ROSY, a novel language for teaching novice programmers through robotics. Its functional style is both familiar with a high-school algebra background and a materialization of the inherent reactive nature of robotic programming. Working at a higher-level of abstraction also teaches valuable design principles of decomposition of robotics software into collections of interacting controllers. Despite its simplicity, ROSY is completely valid Haskell code compatible with the ROS ecosystem. We make a convincing case for our language by demonstrating how non-trivial applications can be expressed with ease and clarity, exposing its sound functional programming foundations, and developing a web-enabled robot programming environment.

Nuno Macedo, Alcino Cunha, José Pereira et al.

We present Alloy4Fun, a web application that enables online editing and sharing of Alloy models and instances, to be used mainly in an educational context. By introducing the notion of secret paragraphs and commands in the models, it also allows the distribution and automatic evaluation of simple specification challenges, a useful mechanism that enables students to learn relational logic at their own pace. Alloy4Fun stores all versions of shared and analyzed models, as well as derivation trees that depict how those models evolved over time: this wealth of information can be mined by researchers or tutors to identify, for example, learning breakdowns in the class or typical mistakes made by students and other Alloy users. A beta version of Alloy4Fun was already used in two formal methods courses, and we present some results of this preliminary evaluation.

Rui Couto, José C. Campos, Nuno Macedo et al.

Alloy is a lightweight formal specification language, supported by an IDE, which has proven well-suited for reasoning about software design in early development stages. The IDE provides a visualizer that produces graphical representations of analysis results, which is essential for the proper validation of the model. Alloy is a rich language but inherently static, so behavior needs to be explicitly encoded and reasoned about. Even though this is a common scenario, the visualizer presents limitations when dealing with such models. The main contribution of this paper is a principled approach to generate instance visualizations, which improves the current Alloy Visualizer, focusing on the representation of behavior.

Nuno Macedo, Alcino Cunha

Alloy and TLA+ are two formal specification languages that are increasingly popular due to their simplicity and flexibility, as well as the effectiveness of their companion model checkers, the Alloy Analyzer and TLC, respectively. Nonetheless, while TLA+ focuses on temporal properties, Alloy is better suited to handle structural properties, requiring ad hoc mechanisms to reason about temporal properties. Thus, both have limitations in the specification and analysis of systems rich in both static and dynamic properties. This paper explores the pros and cons of these two frameworks when handling this class of systems through the step-by-step modeling, specification and verification of an example.

Nuno Macedo, Tiago Jorge, Alcino Cunha

Consistency management, the ability to detect, diagnose and handle inconsistencies, is crucial during the development process in Model-driven Engineering (MDE). As the popularity and application scenarios of MDE expanded, a variety of different techniques were proposed to address these tasks in specific contexts. Of the various stages of consistency management, this work focuses on inconsistency fixing in MDE, where such task is embodied by model repair techniques. This paper proposes a feature-based classification system for model repair techniques, based on an systematic review of previously proposed approaches. We expect this work to assist both the developers of novel techniques and the MDE practitioners looking for suitable solutions.