Runtime monitoring library for the FreeRTOS

Abstract

Runtime Verification (RV) é uma técnica leve e dinâmica que verifica a execução atual do sistema por meio de estruturas chamadas monitores e produz um veredicto sobre se essa execução satisfaz ou não uma propriedade específica de correção do sistema. Atualmente, há alguns trabalhos que fornecem bibliotecas para suporte à RV. No entanto, uma característica comum é o suporte apenas a sistemas POSIX, e muitos Real-Time Operating Systems (RTOS) não possuem suporte a POSIX, como, por exemplo, o FreeRTOS. Neste trabalho, foi desenvolvida uma biblioteca de suporte ao RunTime Monitoring (RM), que são os monitores para suporte a RunTime Verification com suporte a sistemas não-POSIX. Um dos requisitos era o desenvolvimento de uma biblioteca altamente desacoplada da arquitetura do Real-Time Operating System (RTOS), com suporte ao monitoramento dos Deadlines e Execution Time das Tasks e suporte às Tasks Periódicas e Não Periódicas. O trabalho também possui dois modos de operação: um modo de operação online e um modo de operação offline. O modo de operação offline é mais simples e leve, buscando impactar menos o sistema sendo monitorado, enquanto o modo de operação online faz todas as verificações dos monitores no sistema em execução e também possui suporte a alguns recursos adicionais.Foi desenvolvida uma aplicação exemplo para demonstrar o funcionamento da biblioteca, a partir de um modelo proveniente do Projeto ProVANT. A biblioteca deu suporte ao monitoramento e validação do modelo proveniente do ProVANT e também demonstrou como utilizar a biblioteca e todos os recursos que ela suporta.

Abstract: RunTime Verification (RV) is a lightweight and dynamic technique that checks the current running of the system through structures called monitors and produces a verdict on whether or not this run satisfies a specific property of system correctness. Currently there are some works that provide libraries to support RV, however a common feature is the support only for POSIX systems like Linux, and many Real Time Operating Systems (RTOS) do not support POSIX, such as FreeRTOS. In this work, a support library for RunTime Monitoring is developed, which are the monitors to support RunTime Verification with support for FreeRTOS. One of the requirements was the development of a library highly decoupled from the RTOS architecture, with support for monitoring Deadlines and Execution Time of Tasks and support for Periodic and Non-Periodic Tasks. There are also two operation modes, an online operation mode and an offline operation mode, the offline operation mode is simpler and lighter, seeking to impact less the system being monitored, the online operation mode does all the checks of the monitors on the running system and also supports some additional features. An example application was developed to demonstrate how the library works, based on a model from the ProVANT Project. The library supported the monitoring and validation of the model from ProVANT and also demonstrated how to use the library and all the features it supports.