HASLab - Indexed Articles in Conferences

Permanent URI for this collection

http://localhost:4000/handle/123456789/176

Browse

Browsing HASLab - Indexed Articles in Conferences by Author "5612"
  • Item
    Adding Records to Alloy
    ( 2023) Nuno Moreira Macedo ; Alcino Cunha ; 5625 ; 5612
    Records are a composite data type available in most programming and specification languages, but they are not natively supported by Alloy. As a consequence, users often find themselves having to simulate records in ad hoc ways, a strategy that is error prone and often encumbers the analysis procedures. This paper proposes a conservative extension to the Alloy language to support record signatures. Uniqueness and completeness is imposed on the atoms of such signatures, while still supporting Alloy’s flexible signature hierarchy. The Analyzer has been extended to internally expand such record signatures as partial knowledge for the solving procedure. Evaluation shows that the proposed approach is more efficient than commonly used idioms. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
  • Item
    Experiences on Teaching Alloy with an Automated Assessment Platform
    ( 2020) Alcino Cunha ; Carvalho,R ; Pereira,J ; Macedo,N ; Silva,DC ; Ramalho,MS ; Paiva,ACR ; Silva,R ; 5612
  • Item
    An Experimental Evaluation of Tools for Grading Concurrent Programming Exercises
    ( 2023) José Orlando Pereira ; Paulo Sérgio Almeida ; Alcino Cunha ; 5602 ; 5607 ; 5612
  • Item
    The High-Assurance ROS Framework
    ( 2021) Santos,A ; Alcino Cunha ; Nuno Moreira Macedo ; 5625 ; 5612
  • Item
    Improving the Visualization of Alloy Instances
    ( 2018) José Creissac Campos ; Rui Miguel Couto ; Alcino Cunha ; Nuno Moreira Macedo ; 5625 ; 5599 ; 5612 ; 6000
    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. c R. Couto, J. C. Campos, N. Macedo & A. Cunha This work is licensed under the Creative Commons Attribution License.
  • Item
    Merging Cloned Alloy Models with Colorful Refactorings
    ( 2020) Alcino Cunha ; Liu,C ; Nuno Moreira Macedo ; 5612 ; 5625
  • Item
    Property-based testing for the robot operating system
    ( 2018) André Filipe Santos ; Alcino Cunha ; Nuno Moreira Macedo ; 5625 ; 6414 ; 5612
  • Item
    Schema-guided Testing of Message-oriented Systems
    ( 2022) Santos,A ; Alcino Cunha ; Nuno Moreira Macedo ; 5625 ; 5612
    Effective testing of message-oriented software requires describing the expected behaviour of the system and the causality relations between messages. This is often achieved with formal specifications based on temporal logics that require both first-order and metric temporal constructs - to specify constraints over data and real time. This paper proposes a technique to automatically generate tests for metric first-order temporal specifications that match well-understood specification patterns. Our approach takes in properties in a high-level specification language and identifies test schemas (strategies) that are likely to falsify the property. Schemas correspond to abstract classes of execution traces, that can be refined by introducing assumptions about the system. At the low level, concrete traces are successively produced for each schema using property-based testing principles. We instantiate this approach for a popular robotic middleware, ROS, and evaluate it on two systems, showing that schema-based test generation is effective for message-oriented software.
  • Item
    Simplifying the Analysis of Software Design Variants with a Colorful Alloy
    ( 2019) Chong Liu ; Alcino Cunha ; Nuno Moreira Macedo ; 5625 ; 5612 ; 6934
    Formal modeling and automatic analysis are essential to achieve a trustworthy software design prior to its implementation. Alloy and its Analyzer are a popular language and tool for this task. Frequently, rather than a single software artifact, the goal is to develop a full software product line (SPL) with many variants supporting different features. Ideally, software design languages and tools should provide support for analyzing all such variants (e.g., by helping pinpoint combinations of features that could break a property), but that is not currently the case. Even when developing a single artifact, support for multi-variant analysis is desirable to explore design alternatives. Several techniques have been proposed to simplify the implementation of SPLs. One such technique is to use background colors to identify the fragments of code associated with each feature. In this paper we propose to use that same technique for formal design, showing how to add support for features and background colors to Alloy and its Analyzer, thus easing the analysis of software design variants. Some illustrative examples and evaluation results are presented, showing the benefits and efficiency of the implemented technique. © Springer Nature Switzerland AG 2019.
  • Item
    Simulation under Arbitrary Temporal Logic Constraints
    ( 2019) Brunel,J ; Nuno Moreira Macedo ; Alcino Cunha ; Chemouil,D ; 5625 ; 5612
    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. © J. Brunel, D. Chemouil, A. Cunha, & N. Macedo.
  • Item
    Static-Time Extraction and Analysis of the ROS Computation Graph
    ( 2019) André Filipe Santos ; Alcino Cunha ; Nuno Moreira Macedo ; 6414 ; 5612 ; 5625
    The Robot Operating System (ROS) is one of the most popular open source robotic frameworks, and has contributed significantly to the fast development of robotics. Even though ROS provides many ready-made components, a robotic system is inherently complex, in particular regarding the architecture and orchestration of such components. Availability and analysis of a system's architecture at compile time is fundamental to ease comprehension and development of higher-quality software. However, ROS developers have to overcome this complexity relying mostly on testing and runtime visualisers. This work aims to enhance static-time support by proposing, firstly, a metamodel to describe the software architecture of ROS systems (the ROS Computation Graph) and, secondly, model extraction and visualisation tools for such architectural models. The provided tools allow users to specify custom-made queries over these models, enabling the static verification of relevant properties that had to be (manually) checked at runtime before. © 2019 IEEE.
  • Item
    Task Model Design and Analysis with Alloy
    ( 2023) Alcino Cunha ; Nuno Moreira Macedo ; 5612 ; 5625
    This paper describes a methodology for task model design and analysis using the Alloy Analyzer, a formal, declarative modeling tool. Our methodology leverages (1) a formalization of the HAMSTERS task modeling notation in Alloy and (2) a method for encoding a concrete task model and compose it with a model of the interactive system. The Analyzer then automatically verifies the overall model against desired properties, revealing counter-examples (if any) in terms of interaction scenarios between the operator and the system. In addition, we demonstrate how Alloy can be used to encode various types of operator errors (e.g., inserting or omitting an action) into the base HAMSTERS model and generate erroneous interaction scenarios. Our methodology is applied to a task model describing the interaction of a traffic air controller with a semi-autonomous Arrival MANager (AMAN) planning tool. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
  • Item
    Timely Specification Repair for Alloy 6
    ( 2022) Cerqueira,J ; Alcino Cunha ; Nuno Moreira Macedo ; 5625 ; 5612
  • Item
    Validating Multiple Variants of an Automotive Light System with Electrum
    ( 2020) Liu,C ; Alcino Cunha ; Macedo,N ; 5612
  • Item
    Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum
    ( 2018) Nuno Moreira Macedo ; Alcino Cunha ; 5625 ; 5612
  • Item
    Verification of railway network models with EVEREST
    ( 2022) Nuno Moreira Macedo ; Alcino Cunha ; José Creissac Campos ; José Nuno Oliveira ; Rafael Braga Costa ; 5625 ; 5612 ; 5599 ; 5601 ; 8206
    Models-at different levels of abstraction and pertaining to different engineering views-are central in the design of railway networks, in particular signalling systems. The design of such systems must follow numerous strict rules, which may vary from project to project and require information from different views. This renders manual verification of railway networks costly and error-prone. This paper presents EVEREST, a tool for automating the verification of railway network models that preserves the loosely coupled nature of the design process. To achieve this goal, EVEREST first combines two different views of a railway network model-the topology provided in signalling diagrams containing the functional infrastructure, and the precise coordinates of the elements provided in technical drawings (CAD)-in a unified model stored in the railML standard format. This railML model is then verified against a set of user-defined infrastructure rules, written in a custom modal logic that simplifies the specification of spatial constraints in the network. The violated rules can be visualized both in the signalling diagrams and technical drawings, where the element(s) responsible for the violation are highlighted. EVEREST is integrated in a long-term effort of EFACEC to implement industry-strong tools to automate and formally verify the design of railway solutions. © 2022 ACM.
  • Item
    Verification of railway network models with EVEREST
    ( 2022) Martins,J ; Fonseca,JM ; Costa,R ; José Creissac Campos ; Alcino Cunha ; Nuno Moreira Macedo ; Oliveira,JN ; 5612 ; 5625 ; 5599
    Models-at different levels of abstraction and pertaining to different engineering views-are central in the design of railway networks, in particular signalling systems. The design of such systems must follow numerous strict rules, which may vary from project to project and require information from different views. This renders manual verification of railway networks costly and error-prone. This paper presents EVEREST, a tool for automating the verification of railway network models that preserves the loosely coupled nature of the design process. To achieve this goal, EVEREST first combines two different views of a railway network model-the topology provided in signalling diagrams containing the functional infrastructure, and the precise coordinates of the elements provided in technical drawings (CAD)-in a unified model stored in the railML standard format. This railML model is then verified against a set of user-defined infrastructure rules, written in a custom modal logic that simplifies the specification of spatial constraints in the network. The violated rules can be visualized both in the signalling diagrams and technical drawings, where the element(s) responsible for the violation are highlighted. EVEREST is integrated in a long-term effort of EFACEC to implement industry-strong tools to automate and formally verify the design of railway solutions. © 2022 ACM.
  • Item
    Verification of system-wide safety properties of ROS applications
    ( 2020) Carvalho,R ; Santos,A ; Macedo,N ; Alcino Cunha ; 5612
  • Item
    Verifying Temporal Relational Models with Pardinus
    ( 2023) Alcino Cunha ; Nuno Moreira Macedo ; 5612 ; 5625
    This short paper summarizes an article published in the Journal of Automated Reasoning [7]. It presents, an extension of the popular [12] relational model finder with linear temporal logic (including past operators) to simplify the analysis of dynamic systems. includes a SAT-based bounded model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counterexamples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.