| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 9.9 MB | Adobe PDF |
Authors
Abstract(s)
Cyber-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.
Os 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.
Os 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.
Description
Keywords
Cyber-Physical Systems Formal verification method Model checking Call ordering MicroPython Sistemas Ciber-Físicos Métodos de verificação formal Verificação de modelo Ordem de chamadas