Logo do repositório

ISEP - DM - Engenharia de Sistemas Computacionais Críticos

URI permanente para esta coleção:

http://hdl.handle.net/10400.22/23806

Navegar

Percorrer ISEP - DM - Engenharia de Sistemas Computacionais Críticos por autor "HERNÁNDEZ, LIDIA GLORIA WILSON"

A mostrar 1 - 1 de 1
  • Rumo a uma estrutura de verificação e validação baseada em arquiteturas de microserviços
    Publication . HERNÁNDEZ, LIDIA GLORIA WILSON; Pinho, Luís Miguel Rosário da Silva
    In 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.
    2025-10-09Dissertação de mestrado Acesso aberto Ver mais