Time-accurate Middleware for the Virtualization of Communication Protocols

Abstract

Esse trabalho foi realizado dentro do grupo VERTICS do LAAS-CNRS, Laboratório de Análise e Arquiteturas de Sistemas, localizado em Toulouse (França), em parceria com a empresa francesa Scalian. VERTICS possui foco no uso de métodos formais para estudar sistemas críticos com características temporais restritas. É também o local de desenvolvimento da ferramenta de model checking Tina, da linguagem de especificação Fiacre e do motor de execução Hippo; ferramentas que são utilizadas nesse projeto. O parceiro industrial Scalian é especialista em sistemas críticos e embarcados, testabilidade, simulação e sistemas digitais.

A complexidade de sistemas aviônicos só tem aumentado com o passar do tempo. Co- municação entre os dispositivos de uma rede aviônica deve ser previsível, deterministica

e confiável. Para auxiliar o cumprimento desses requisitos, protocolos de comunicação como ARINC 429 e AFDX foram especificados para padronizar as arquiteturas de rede e o modo no qual os dispositivos devem comunicar-se entre si. Entretanto, mesmo que o comportamento de cada componente da rede seja bem definido, ainda é necessário testar extensivamente cada aplicação durante o desenvolvimento e implementação. Normalmente testes em sistemas com essas características são realizados através do uso de hardware equivalente ou semelhante ao utilizado em aplicações reais. Sistemas físicos de teste necessários no desenvolvimento de sistemas aviônicos são complexos e com custo inicial e de manutenção elevados. Sendo assim, fabricantes têm utilizado cada vez mais da simulação e da virtualização para a realização de testes quando possível. Nesse contexto, virtualização propõe muitas vantagens. Primeiramente, ela elimina a necessidade de implementar sistemas físicos (switches, cabos, etc), cortando os custos necessários para a implantação, manutenção e alimentação desses elementos. Virtualização também torna o desenvolvimento e a testabilidade mais rápidos e fáceis—benefícios esses também sobre a simulação, a qual tem um comportamento geralmente muito mais lento que o hardware. Além do mais, muitas vezes é possível integrar facilmente uma rede virtualizada com componentes físicos, como software e hardware utilizados em aplicações reais. Nessa monografia é proposto um protótipo de um middleware tempo real para virtualização de protocolos de comunicação—mais especificamente o protocolo AFDX. Tempo real nesse contexto significa que as características temporais observadas durante a virtualização devem estar o mais próximo possível do comportamento real. Durante o estágio foi desenvolvido um novo framework de virtualização utilizando o emulador de redes Mininet, capaz de virtualizar uma rede AFDX em um computador padrão com Linux. O framework fornece um ambiente para testar diferentes configurações de redes, de fácil instalação, onde a escalabilidade depende principalmente da plataforma física. Embora ainda não tenha garantias suficientes para respeitar todos os requisitos temporais

rigorosamente, resultados experimentais evidenciam a capacidade da virtualização de simular a rede mais rápido que sistemas físicos reais. Entretanto, ainda é necessária a continuação do desenvolvimento do protótipo e uma melhor análise da performance— através do uso de ferramentas de benchmarking também desenvolvidas durante o estágio— antes que se possa concluir sobre a vialibidade de virtualizar redes AFDX industriais mantendo as características tempo-real. Paralelamente, outra contribuição deste trabalho é o desenvolvimento de três modelos formais de redes AFDX utilizando a linguagem de especificação Fiacre—linguagem formal baseada na teoria de Redes de Petri— levando em conta as restrições temporais do protocolo. Os modelos têm diferentes níveis de aproximação em relação ao sistema real, aumentando o nível de precisão com o qual dados são transportados através da rede. Também foi desenvolvido um modelo formal do mecanismo de policiamento de tráfego—o algoritmo Token Bucket—responsável por limitar a banda passante e enforçar o cumprimento das garantias de serviço da rede. Esses modelos formais são então utilizados como pontos de referência para a criação de monitores, afim de garantir as características temporais da virtualização durante a execução. Os monitores são executados através do motor de execução Hippo, o qual é capaz de executar Redes de Petri com suporte a chamada de funções externas e gerenciamento de eventos. Entretanto, Hippo ainda está em fase inicial de desenvolvimento e durante a implementação dos monitores foi descoberta uma falha fundamental na sua implementação, impedindo que os monitores sejam executados com o comportamento correto. Mesmo assim, a tradução dos modelos formais de Fiacre para Hippo se mostrou possível e acessível.

Communication between devices in avionics systems must be predictable and deterministic, and data must be delivered reliably. To help the system architects comply with these requirements, network protocol standards like ARINC 429 and AFDX were created. Even though the behaviour of each component in a network is well defined, it is still necessary to test extensively every applications before deployment. But physical test benches used in the aircraft development process are complex and expensive platforms. In order to limit the need for physical tests, we propose a time-accurate middleware for virtualizing communication protocols that can be used to replace physical tests with simulations. During my internship I specified three formal models of AFDX networks that take into account temporal constraints with different levels of precision. I also developed a prototype for a network virtualization middleware based on the AFDX protocol specification that provides an easy-to-setup environment for testing network configurations. Finally, I have used formal models together with virtualization in order to define runtime monitors for checking whether the behavior of the middleware is time-accurate with respect to a real system.