ISEP - DM - Engenharia de Sistemas Computacionais Críticos
Permanent URI for this collection
Browse
Browsing ISEP - DM - Engenharia de Sistemas Computacionais Críticos by advisor "Pereira, David Miguel Ramalho"
Now showing 1 - 2 of 2
Results Per Page
Sort Options
- Abordagem à especificação e verificação de requisitos: Caso de estudo em Updates via Over the AirPublication . CARVALHO, ANAISA CRISTINA PEREIRA; Pereira, David Miguel Ramalho; Pinho, Luís Miguel Rosário da SilvaModern vehicles rely on increasingly complex embedded software to deliver advanced features in performance, safety, and connectivity. In automotive software development, a precise requirement specification is essential to manage complexity and ensure reliability throughout the life cycle. Although natural language has been standard for documenting requirements, it often introduces ambiguity and misinterpretation. This thesis focuses on investigating the advantages of adopting formal requirements engineering over natural language approaches within the automotive field, using the Formal Requirements Elicitation Tool (FRET) tool and taking as use case a representative set of requirements of an Over-the-Air (OTA) updates project derived from the automotive industry. This analysis highlights how FRET improves clarity when eliciting, managing, analysis, and verifying requirements, thus serving as a strong asset for reducing errors in later development phases, which is specially important in critical projects. This work also provides evidence of the tangible benefits of formal techniques for the specification, analysis, and verification of vehicle software requirements, but also highlights that tools such as FRET still require formal logic training and, given the niche nature of the tool, that users maintain regular interaction with the developers in order to be aware of features that are fundamental for better usage of the tool, however that still remain undocumented in the literature.
- Formal analysis of an authority transfer protocol for UAVsPublication . Rodrigues, Ricardo Alexandre Almeida; Pereira, David Miguel RamalhoThe use of Unmanned Aerial Vehicles (UAVs) in a variety of applications has resulted in a growing demand for Beyond Visual Line of Sight (BVLOS) operations to cover long distances. This thesis focuses on an initial analysis of a UAV communication protocol designed for transferring control authority between ground controls within a common range, addressing challenges and evaluating its efficacy across different operational phases. The research encompasses start-up, mission execution, and handover phases, assessing the protocol’s interactions with ground-based systems for reliability, efficiency, and adaptability. A comprehensive overview of model checking is provided, emphasizing transition systems, formalisms, and tools for system correctness verification. The research employs model checking to formally specify and model the UAV communication protocol, establishing evaluation criteria through the use of LTL and CTL properties. The derived requirements serve as a foundational framework for future iterations, ensuring the protocol’s robustness and addressing security strategies in the event of connection loss. The holistic approach contributes to a comprehensive understanding of the protocol’s functionality, aiming to enhance the security authorization handover procedure and promote public and regulatory acceptance of BVLOS operations with UAVs.