72 citations · 97 across the 10 of their papers we have counts for
7 papers · 1 filter
Model checking of hyperproperties for high-level relational models
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…
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…
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…
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…