72 citations · 135 across the 12 of their papers we have counts for
13 papers
Synthesizing Test Cases for Narrowing Specification Candidates
Alcino Cunha, Nuno Macedo
This paper proposes a technique to help choose the best formal specification candidate among a set of alternatives. Given a set of specifications, our technique generates a suite o…
Validating Formal Specifications with LLM-generated Test Cases
Alcino Cunha, Nuno Macedo
Validation is a central activity when developing formal specifications. Similarly to coding, a possible validation technique is to define upfront test cases or scenarios that a fut…
The High-Assurance ROS Framework
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 Ro…
alurity, a toolbox for robot cybersecurity
Víctor Mayoral-Vilches, Irati Abad-Fernández, Martin Pinzger +8
The reuse of technologies and inherent complexity of most robotic systems is increasingly leading to robots with wide attack surfaces and a variety of potential vulnerabilities. Gi…
Simulation under Arbitrary Temporal Logic Constraints
Julien Brunel, David Chemouil, Alcino Cunha +1
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…
Sharing and Learning Alloy on the Web
Nuno Macedo, Alcino Cunha, José Pereira +5
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 notio…
Improving the Visualization of Alloy Instances
Rui Couto, José C. Campos, Nuno Macedo +1
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 pro…
Alloy meets TLA+: An exploratory study
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 c…
A Feature-based Classification of Model Repair Approaches
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 a…
A Generic Scheme and Properties of Bidirectional Transformations
Hugo Pacheco, Nuno Macedo, Alcino Cunha +1
The recent rise of interest in bidirectional transformations (BXs) has led to the development of many BX frameworks, originating in diverse computer science disciplines. From a use…
Automatic Unbounded Verification of Alloy Specifications with Prover9
Nuno Macedo, Alcino Cunha
Alloy is an increasingly popular lightweight specification language based on relational logic. Alloy models can be automatically verified within a bounded scope using off-the-shelf…
Bounded Model Checking of Temporal Formulas with Alloy
Alcino Cunha
Alloy is formal modeling language based on first-order relational logic, with no specific support for specifying reactive systems. We propose the usage of temporal logic to specify…
Fast Distributed Computation of Distances in Networks
Paulo Sérgio Almeida, Carlos Baquero, Alcino Cunha
This paper presents a distributed algorithm to simultaneously compute the diameter, radius and node eccentricity in all nodes of a synchronous network. Such topological information…