| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 4.64 MB | Adobe PDF |
Authors
Advisor(s)
Abstract(s)
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.
Nos últimos anos, as arquiteturas de microsserviços tornaram-se uma abordagem popular no desenvolvimento de software para enfrentar os desafios de escalabilidade, manutenção e agilidade de sistemas complexos. Esta tese enfoca a interseção das arquiteturas de microsserviços com técnicas de verificação formal, especialmente no contexto de aplicações críticas para a segurança, como soluções de condução assistida e/ou automatizada. A falta de investigação nesta área requer uma investigação abrangente sobre como as arquiteturas de microsserviços e as técnicas de verificação formal podem interagir de forma eficaz. O principal desafio é integrar perfeitamente as arquiteturas de microsserviços com os processos de verificação formal para garantir as propriedades de segurança típicas dos sistemas ciberfísicos, com um foco particular nas aplicações de condução autónoma. A importância deste trabalho reside no desenvolvimento de uma estrutura robusta que concilie a natureza descentralizada dos microsserviços com os requisitos da verificação formal. Os objetivos da investigação incluem analisar os benefícios e limitações dos microsserviços, identificar ferramentas de verificação formal e estruturas de microsserviços adequadas, projetar APIs de microsserviços e realizar experiências para validação. Implementações bemsucedidas e uma visão geral abrangente dos métodos de verificação formal em sistemas críticos para a segurança formam a base desta investigação. Como prova de conceito, esta tese apresenta a implementação do VVFramework, uma estrutura híbrida de verificação e validação baseada em microsserviços que integra NuSMV, Z3 e um pipeline de tradução automática Python-SMV e demonstra a sua aplicabilidade para pequenos estudos de caso em domínios críticos para a segurança.
Nos últimos anos, as arquiteturas de microsserviços tornaram-se uma abordagem popular no desenvolvimento de software para enfrentar os desafios de escalabilidade, manutenção e agilidade de sistemas complexos. Esta tese enfoca a interseção das arquiteturas de microsserviços com técnicas de verificação formal, especialmente no contexto de aplicações críticas para a segurança, como soluções de condução assistida e/ou automatizada. A falta de investigação nesta área requer uma investigação abrangente sobre como as arquiteturas de microsserviços e as técnicas de verificação formal podem interagir de forma eficaz. O principal desafio é integrar perfeitamente as arquiteturas de microsserviços com os processos de verificação formal para garantir as propriedades de segurança típicas dos sistemas ciberfísicos, com um foco particular nas aplicações de condução autónoma. A importância deste trabalho reside no desenvolvimento de uma estrutura robusta que concilie a natureza descentralizada dos microsserviços com os requisitos da verificação formal. Os objetivos da investigação incluem analisar os benefícios e limitações dos microsserviços, identificar ferramentas de verificação formal e estruturas de microsserviços adequadas, projetar APIs de microsserviços e realizar experiências para validação. Implementações bemsucedidas e uma visão geral abrangente dos métodos de verificação formal em sistemas críticos para a segurança formam a base desta investigação. Como prova de conceito, esta tese apresenta a implementação do VVFramework, uma estrutura híbrida de verificação e validação baseada em microsserviços que integra NuSMV, Z3 e um pipeline de tradução automática Python-SMV e demonstra a sua aplicabilidade para pequenos estudos de caso em domínios críticos para a segurança.
Description
Keywords
Microservices Architectures Formal Verification Verification Framework Software Frameworks Safety-critical Systems
Pedagogical Context
Citation
Publisher
CC License
Without CC licence