Repository logo
 
Publication

Safe and resource-aware verification for programming Cyber-Physical Systems

2025-02-06Doctoral thesis Open access
Simple item page
datacite.subject.fosCiências Naturais::Ciências da Computação e da Informaçãopt_PT
dc.contributor.advisorMartins, Francisco Cipriano da Cunha
dc.contributor.advisorCosta, António Casimiro Ferreira da
dc.contributor.authorMão De Ferro, Carlos
dc.date.accessioned2025-05-14T15:39:07Z
dc.date.available2025-05-14T15:39:07Z
dc.date.issued2025-02-06
dc.date.submitted2024-04-21
dc.description.abstractCyber-physical systems (CPS) integrate computation with physical processes and are expected to influence nearly 30 billion devices globally by 2030. Developing software for these systems presents unique challenges, especially in critical and resource-constrained scenarios. A predominant issue is the integration of multiple stateful systems, where the incorrect sequence of function calls compromises the overall system functionality. Formal verification increases safety, but its application is often confined to experts. This thesis presents Shelley, a novel model checking framework that streamlines the verification of function call order when integrating stateful systems. Shelley uniquely allows developers to specify temporal requirements closely aligned with the source code and automates the verification process. The framework’s ability to generate behavior diagrams and show intuitive counterexamples further assists developers in analyzing the program behavior, ensuring that the software is safe and adheres to its specified requirements. An evaluation is provided, which includes rigorous case studies such as NASA’s PHALANX experiment and an industrial setting, demonstrating the framework’s broad applicability and effectiveness in identifying invalid behaviors. Our contributions through the Shelley framework include the formalization of the process of extracting models from MicroPython code, as well as a new specification language tailored for verifying call order. In addition, we establish the decidability of checking system usage via automata theory and we introduce an automated process for checking requirements that utilizes temporal logic over finite traces. Together, these advancements simplify the incorporation of formal verification into high-level programming contexts, ensuring that more programmers can deliver safer software.pt_PT
dc.description.abstractOs sistemas ciberfísicos integram computação com processos físicos prevendose cerca de 30 mil milhões de dispositivos globalmente até 2030. Um problema predominante é a integração de sistemas com estado, onde uma incorreta sequência de chamadas pode comprometer a funcionalidade do sistema no seu todo. A verificação formal contribui para garantir a segurança operacional, mas a sua aplicação está frequentemente confinada a programadores especialistas. A Shelley é uma ferramenta de verificação de modelo que simplifica a verificação da ordem de chamadas em sistemas com estado. A Shelley permite de forma única que os programadores especifiquem requisitos temporais estreitamente alinhados com o código-fonte e automatiza o processo de verificação. Adicionalmente, a sua capacidade de gerar diagramas de comportamento e de mostrar contraexemplos intuitivos é uma ajuda fundamental na análise do comportamento do programa, garantindo que o software é seguro e que cumpre os requisitos especificados. A avaliação desta ferramenta é feita através de dois estudos de caso rigorosos, a experiência PHALANX da NASA e a aplicação industrial Aquamote®, demonstrando a ampla aplicabilidade da ferramenta e a sua eficácia na identificação de comportamentos inválidos. As contribuições desta tese incluem a formalização do processo de extração de modelos a partir de código MicroPython, bem como a introdução de uma nova linguagem de especificação feita à medida. Adicionalmente, mostramos que é decidível verificar a utilização de um sistema fazendo uso da teoria de autómatos e introduzimos um processo automatizado para verificar requisitos que utiliza lógica temporal sobre traços finitos. Estes avanços simplificam a incorporação de verificação formal em linguagens de alto nível, garantindo aos programadores não especialistas a possibilidade de escrever software mais seguro.pt_PT
dc.identifier.tid101548923pt_PT
dc.identifier.urihttp://hdl.handle.net/10400.5/100695
dc.language.isoengpt_PT
dc.relationSafe resource-aware virtual machines for IoT devices
dc.relationLASIGE - Extreme Computing
dc.relationLASIGE - Extreme Computing
dc.subjectCyber-Physical Systemspt_PT
dc.subjectFormal verification methodpt_PT
dc.subjectModel checkingpt_PT
dc.subjectCall orderingpt_PT
dc.subjectMicroPythonpt_PT
dc.subjectSistemas Ciber-Físicospt_PT
dc.subjectMétodos de verificação formalpt_PT
dc.subjectVerificação de modelopt_PT
dc.subjectOrdem de chamadaspt_PT
dc.titleSafe and resource-aware verification for programming Cyber-Physical Systemspt_PT
dc.typedoctoral thesis
dspace.entity.typePublication
oaire.awardTitleSafe resource-aware virtual machines for IoT devices
oaire.awardTitleLASIGE - Extreme Computing
oaire.awardTitleLASIGE - Extreme Computing
oaire.awardURIinfo:eu-repo/grantAgreement/FCT/OE/SFRH%2FBD%2F131418%2F2017/PT
oaire.awardURIinfo:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F00408%2F2020/PT
oaire.awardURIinfo:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDP%2F00408%2F2020/PT
oaire.fundingStreamOE
oaire.fundingStream6817 - DCRRNI ID
oaire.fundingStream6817 - DCRRNI ID
person.familyNameMão de Ferro
person.givenNameCarlos
person.identifier920392
person.identifier.ciencia-id4D1F-DDA3-3150
person.identifier.orcid0000-0001-6835-3097
person.identifier.ridU-5247-2018
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.nameFundação para a Ciência e a Tecnologia
project.funder.nameFundação para a Ciência e a Tecnologia
project.funder.nameFundação para a Ciência e a Tecnologia
rcaap.rightsopenAccesspt_PT
rcaap.typedoctoralThesispt_PT
relation.isAuthorOfPublication02469c6c-ecd9-4828-9948-d85413b314fa
relation.isAuthorOfPublication.latestForDiscovery02469c6c-ecd9-4828-9948-d85413b314fa
relation.isProjectOfPublication137b0e44-be4c-4f20-9c3e-98322310730a
relation.isProjectOfPublicationb429b8f0-500f-4a0b-8e91-33e0a200ad1c
relation.isProjectOfPublication1047b7c0-692c-4e8a-9fb0-ef819e9248a3
relation.isProjectOfPublication.latestForDiscovery1047b7c0-692c-4e8a-9fb0-ef819e9248a3
thesis.degree.nameTese de doutoramento, Informática, Universidade de Lisboa, Faculdade de Ciências, 2025pt_PT

Files

Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
scnd_td_Carlos_Ferro.pdf
Size:
9.9 MB
Format:
Adobe Portable Document Format
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.2 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

FC - Teses de Doutoramento