On the specification and verification of safety properties in data-driven critical systems

Abstract

Os dados estão no cerne do design de sistemas críticos de segurança modernos. Os dados não são mais apenas sensoriados e processados no contexto dos loops de controle de tais sistemas. Eles também são protegidos, armazenados e transmitidos para o bem dos processos de tomada de decisão necessários para níveis mais altos de autonomia. As estratégias centradas em tarefas, tradicionalmente usadas para projetar sistemas críticos, oferecem suporte consistente à análise de escalonamento e verificação dos tempos de execução de tarefas, desde que os períodos, prazos e estimativas de tempo de execução sejam conhecidos, mas geralmente ignoram o fluxo de dados entre os vários componentes do sistema, e assumem que o tempo de geração de dados é constante e pode ser totalmente encapsulado no tempo de execução das tarefas. Essas suposições, no entanto, não estão alinhadas com o design de sistemas autônomos modernos, como fábricas inteligentes e veículos autônomos, exemplos de sistemas que enfrentam restrições de criticidade e estão avançando rapidamente em direção à autonomia. Uma abordagem orientada a dados para o design de tais sistemas pode acomodar mais prontamente requisitos como atualização de dados, fontes de dados redundantes, e segurança operacional. Neste trabalho, um Framework para apoiar a especificação e verificação das propriedades de segurança de sistemas críticos projetados com métodos orientados a dados. Extraímos as propriedades considerando os requisitos temporais e a dependência de dados, que são verificados em tempo de execução por meio de uma Unidade de Aplicação de Segurança (Safety Enforcement Unit - SEU). A SEU é um componente isolado do sistema que monitora constantemente o sistema e verifica as propriedades de segurança, emitindo contramedidas conforme necessário para manter a segurança do sistema. Demonstramos e avaliamos a solução proposta modelando um Veículo Autônomo, com uma implementação de prova de conceito que considera um simulador de veículo autônomo integrado a um sistema hardware-in-the-loop. Demonstramos que o sistema pode ser formalmente verificado em tempo de execução, onde a implementação da SEU consumiu menos de 2% da capacidade computacional da Unidade de Controle Eletrônico (Electronic Control Unit - ECU) utilizada para avaliação.

Abstract: Data is at the core of the design of modern Safety-Critical Systems. Data is no longer only sensed and processed in the context of the control loops of such systems. It is also secured, stored, and transmitted for the sake of the decision-making processes required for higher levels of autonomy. The task-centered strategies traditionally used to design critical systems consistently support scheduling analysis and verification of tasks execution times as long as periods, deadlines, and execution time estimates are known, but mostly ignore the flow of data across the various components in the system and often assume that data generation time is constant and can be fully encapsulated in the execution time of tasks. These assumptions, however, are not in phase with the design of modern autonomous systems such as smart factories and autonomous vehicles, examples of systems that address critical constraints, that are quickly advancing towards autonomy. A Data-driven approach to the design of such systems can more promptly accommodate requirements such as data freshness, redundant data sources, and operational safety. In this work, we propose a Framework to support the specification and verification of safety properties of safety-critical systems that are designed using data-driven methods. We extract the properties considering the timing and data dependency, which are verified at run-time via a Safety Enforcement Unit (SEU). The SEU is an isolated component of the system that constantly monitors the data generated by the system and verifies the safety properties, issuing counter-measures as needed to maintain system safety. We demonstrate and evaluate the proposed solution with the modeling of an Autonomous Vehicle, with a proof of concept implementation considering an autonomous vehicle simulator integrated with hardware-in-the-loop. We demonstrate that the system can be formally verified at runtime, where the SEU implementation consumed less than 2% of the computational power of the Electronic Control Unit (ECU) used for evaluation.