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 "Pinho, Luís Miguel Rosário da Silva"
Now showing 1 - 3 of 3
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.
- Application of model checking in the formal verification of requirements for a speed control system in railwayPublication . COELHO, CRISTIANO MANUEL GARCÊS; Pinho, Luís Miguel Rosário da SilvaRailway speed control systems are essential for the safety and efficiency of railway transportation systems, as they ensure compliance with regulations and prevent accidents. As the demand for rail transport grows, rigorous verification of these systems is becomes increasingly critical. In such projects, errors are sometimes only detected during the testing phase, leading to costs that could have been avoided if these errors were identified in the early stages of the project. This thesis focuses on the topic of the formal verification of speed control system, specifically using model checking, to ensure that these systems meet safety requirements as well as performance standards. As the basis for the work presented in this thesis, we will adopt the EBICAB 700 architecture, and for which a small, yet representative, set of safety, operational, or regulatory requirements will be rigorously specified using well-known temporal logic languages, and verified against the system models using the model checking tools NuSMV and UPPAAL. This thesis work aims at contributing to the effort of demonstrating the feasibility and benefits of applying formal verification to railway systems, not only in terms of safety assurance but also as a strategy for reducing late-stage development risks and increased costs. It highlights the value of incorporating formal methods into the requirements and design phases of critical system engineering.
- Rumo a uma estrutura de verificação e validação baseada em arquiteturas de microserviçosPublication . HERNÁNDEZ, LIDIA GLORIA WILSON; Pinho, Luís Miguel Rosário da SilvaIn recent years, microservices architectures have become a popular approach in software development to address the challenges of scalability, maintainability, and agility of complex systems. This thesis focuses on the intersection of microservices architectures with formal verification techniques, especially in the context of safety-critical applications such as Assisted and/or Automated Driving solutions. The lack of research in this area requires a comprehensive investigation of how microservices architectures and formal verification techniques can interact effectively. The primary challenge is to seamlessly integrate microservices architectures with formal verification processes to ensure the safety properties typical of Cyber-Physical Systems, with a particular focus on autonomous driving applications. The importance of this work lies in the development of a robust framework that reconciles the decentralised nature of microservices with the requirements of formal verification. Research objectives include analysing the benefits and limitations of microservices, identifying suitable formal verification tools and microservices frameworks, designing microservices APIs, and conducting experiments for validation. Successful implementations and a comprehensive overview of formal verification methods in safety-critical systems form the basis for this research. As a proof of concept, this thesis presents the implementation of VVFramework, a microservicesbased hybrid verification and validation framework that integrates NuSMV, Z3, and an automatic Python-SMV translation pipeline and demonstrates its applicability for small case studies in safety-critical domains.