Implementação de monitores para verificação de padrões de cenários de operação
de sistemas embarcados baseado em rastreamento temporizado
Aluna: Janize Monteiro de Castilho
Orientadora: Alice M Tokarnia
27 de Junho 2014
Resumo
O comportamento funcional e temporal de um sistema embarcado tem que ser repetidamente
verificado durante o projeto e a operação de campo. Os requisitos dos sistemas, cada vez mais
complexos, que fazem parte de aplicações médicas, automotivas de segurança crítica e de transporte
podem ser descritos por milhares de cenários. Para estes sistemas, verificação de modelo e técnicas de
teste em laboratório devem ser complementadas em tempo de execução para obter garantias de
comportamento a longo prazo em condições reais. Este projeto de pesquisa tem como objetivo
introduzir uma definição de cenário, um conjunto de padrões de restrição de tempo, e um monitor para
ajudar os designers com a especificação e teste de sistemas embarcados. Um cenario pode estar
associado a um dos subsistemas de um sistema e descrever um comportamento incluindo entrada, saída
e alterações nas variável de estado ao longo de vários intervalos de tempo. O monitor verifica traços de
time-stamped das variáveis para o cumprimento do cenário. Pode ser usado tanto para verificação em
laboratório quanto em tempo de execução. Devido ao uso de padrões temporais de restrição, para um
conjunto de cenários, é possível estimar um limite superior sobre o seu tempo de execução. Os
resultados experimentais incluem os cenários para as descrições de requisitos de um sistema embarcado
que ainda está sendo definido e a avaliação de monitor de tempo de processamento em cima.
Introdução e Justificativa
O comportamento funcional e temporal de um sistema embarcado tem que ser repetidamente
verificado durante o projeto e a operação de campo. Os requisitos dos sistemas, cada vez mais
complexos, que fazem parte de aplicações médicas, automotivas de segurança crítica e de transporte
podem ser descritos por milhares de cenários[1] . Para estes sistemas, verificação de modelo e técnicas
de teste em laboratório devem ser complementadas em tempo de execução para obter garantias de
comportamento a longo prazo em condições reais[3] .
O problema com uma simples implementação de um monitor é que isso implicaria sintetizar um
autômato para cada cenário em verificação[9] . Assim, quando um novo cenário é introduzido ou um já
existente é modificado, software de verificação adicional tem que ser desenvolvido. Isso pode exigir
significativo esforço de projeto adicional e contribuir de uma forma imprevisível para monitorar
despesas gerais.
A proposta deste projeto, é apresentar uma definição formal de cenário, um conjunto de padrões
de restrição de tempo, e um monitor para enfrentar os desafios da especificação de sistemas
embarcados e testes. O uso cenários formais e padrões de restrição de tempo permitem a descrição de
uma grande variedade de cenários e simplifica o código do monitor. A verificação de um novo cenário
exige apenas que sua descrição seja inserido no monitor. É possível estimar o tempo de execução do
monitor com base nos cenário e propriedades traçadas.
Conceitos e Trabalhos Relacionados
Esta seção comenta brevemente sobre obras na descrição do cenário, padrões de cenários e
monitores.
Hsia et al. [8] reconheceu a importância de cenários para a descrição do requisito de software.
Eles propuseram um método para análise, geração e validação de cenários e aplicou suas idéias para o
projeto de um simples Sistema PBX. Somé et al. [13] apresentaram um algoritmo incremental para
sintetizar autômato temporizado de cenários correspondentes às necessidades dos utilizadores. Eles
definiram um cenário como a descrição de um interacção entre o sistema e o seu ambiente, numa
situação restrita, isto é, com as condições que devem manter para execução de cenario. Gajski et al. [4]
introduziu o programa modelo de máquina de estado que unifica os conceitos de máquinas hierárquicas
simultâneos de estados finitos, grafos de fluxo de dados, e imperativo linguagens de programação. No
programa máquinas de estado, o Estado determina as respostas do sistema à sua ambiente. Com base
nesses conceitos, o modelo, proposto no trabalho, deverá incluir modos de operação, definidos por
condições em variáveis de estado. Estes modos de operação podem ser associados às relações de
entrada/saída.
Os cenários são baseados em requisitos de sistema e trabalhos de pesquisa dedicados a evitar
ambigüidade têm desempenhado um papel importante na verificação do sistema. Denger et al. [6]
apresentam padrões de linguagem natural, que visam tornar a formulação de requisito funcional menos
ambígua, mais completo e preciso. Os elementos de linguagem em suas descrições são mapeados para
os elementos de um meta-modelo. Moebius et al. [11] utilizado UML com extensão de linguagem de
modelo para descrever protocolos de criptografia e desenvolveu um algoritmo que gera um
especificação e um código executável. Linguagens baseadas em UML para a especificação de sistemas
embarcados são sempre complementados com extensões que expressam contexto, tempo e
concordância.
Padrão de cenário, como proposto por diversos trabalhos, constituiu um passo importante em
direção à geração automática de software de verificação. Konrad e Cheng [10] estenderam os padrões
de especificação propostos por Dwyer et ai. [7] para permitir a descrição de comportamentos do
sistema em tempo real envolvendo duração, período e ordem. Seus padrões, expressos com três lógicas
temporais em tempo real, foram a base para uma estruturada gramática Inglês descrevendo distâncias
temporais entre variável tempos de mudança. Tsai et al. [14, 15] considera a associação de padrões de
cenário para verificação padrões, como forma de simplificar o desenvolvimento de código de
verificação para testes do sistema. Em todos os cenários classificadas em um único padrão, um
engenheiro de teste pode usar o mesmo modelo de software para escrever a código de verificação. Um
cenário que não corresponde a nenhum padrão exigiria o desenvolvimento de software de verificação a
partir do zero. No seu trabalho, apenas 8 padrões de cenário foram capazes de cobrir 95% de os
cenários especificando um dispositivo médico implantável de segurança crítica.
A importância de automatizar a geração de código de verificação de descrição do cenário foi
apontado por vários dos trabalhos acima mencionados. Além disso, Peters e COEX [12]
enfatizou a importância de monitores para sistemas de testes de segurança ou de missão crítica,
apresentou um definição de monitor do sistema em tempo real, e identificou as condições necessárias
para utilidade e viabilidade do monitor. Uma descrição detalhada de geração do código de verificação
também pode ser encontrado em Chen et ai. [5]. Eles apresentaram algoritmos para gerar
automaticamente o código C++ de um verificador de traço diretamente de requisitos escritos usando a
lógica de restrições [2], uma linguagem quantitativa formal que expressa restrições temporárias.
Objetivos
Este projeto de pesquisa tem como objetivo introduzir uma definição de cenário, um conjunto
de padrões de restrição de tempo, e um monitor para ajudar os designers com a especificação e teste de
sistemas embarcados.
Plano de Trabalho e Cronograma
Os créditos das disciplinas serão cumpridos até julho de 2014.
Inicialmente, será feita a revisão bibliográfica a fim se aprofundar no tema escolhido.
Posteriormente, serão escolhidas e estudadas as aplicações que serão utilizadas no trabalho. Em
seguida, iniciar-se-a a descrição dos cenários, com os conjuntos de padrões de restrição de tempo e a
implementação do monitor. Testes estarão sendo realizados para validação dos trabalhos
implementados.
Após validação do monitor, testes serão realizados utilizando-o nas aplicações definidas.
A redação da qualificação será feita ao fim dos testes nas aplicações, seguida da defesa de
qualificação.
Após revisão bibliografica, implementação de cénarios e monitores, teste das aplicações e
defesa de qualificação, iniciar-se-a a fase de redação da dissertação, para posterior defesa.
CRONOGRAMA
Atividades
Mês/Ano
03/14 04/14 05/14 06/14 07/14 08/14 09/14 10/14 11/14 12/14 01/15
Revisão
Bibliográfica
X
X
Definição
Aplicações
X
X
Estudo das
Aplicações
X
X
Descrição
Cenários
Implementação
Monitor
X
X
X
X
X
X
X
X
Testes
X
X
Redação e
Defesa
X
X
02/15
Qualificação
Redação
Dissertação
X
Defesa
Dissertação
X
X
X
Material e Métodos
O desempenho do monitor é uma função do traço e do conjunto de cenários sob verificação. O
traço determina a número de cenários que são simultaneamente pré-ativo ou ativo, que são susceptíveis
de exigir o máximo de processamento tempo em uma linha traço. Portanto, o desempenho do monitor
pode ser avaliada offline ou em tempo de execução estimado com base no historico dos traços. Ao
atribuir uma prioridade de verificação para cada cenário e determinar os cenários a serem verificados
com base nesses prioridades, é possível controlar o tempo de sobrecarga de verificação por linha traço.
Se um traço é gerado com uma política desencadeada em tempo e um intervalo de amostragem, tal
como proposto por Bonakdarpour et al. [3], a taxa de geração de linha de traço seria constante. Neste
caso, usar o monitor proposto no trabalho, é particularmente interessante uma vez que a verificação
tempo de uma linha traço é previsível. Verificação teria então uma sobrecarga de tempo previsível.
A fim de avaliar a expressividade dos cenário e padrões, serão examinados os requisitos de uma
aplicação comercial que ainda não foi definida. O monitor será implementado, a priori, em C e deverá
ser compilado e executado em um microcontrolador. Uma vez que as rotinas do monitor serão fixas, o
tempo, em uma linha de traçado, para processar um determinado cenário será gasto comparando
amostras das variáveis com os valores especificados e verificando equações de tempo.
Forma de Análise dos Resultados
Em um experimento para avaliar o desempenho do monitor, serão utilizados alguns cenários,
com números variáveis de variáveis e equações por cenário. Será considerado que um cenário tem, pelo
menos, uma equação do tempo, correspondente ao seu prazo de verificação.
Os traços serão sintetizados pela combinação de conjuntos de linhas de traçado correspondentes
às execuções bem-sucedidas e fracassadas de cenários em seqüência ou em paralelo, se os cenários têm
conjuntos disjuntos de variáveis.
Referências
[1] W. Tsai, L. Yu, F. Zhu, and R. Paul, "Rapid Embedded System Testing Using Verification Patterns,"
IEEE Software, vol. 22, p. 68, July/Aug.
[2] F. Balarin, J. Burch, L. Lavagno, Y. Watanable, R. Passerone, A. Sangiovanni-Vincentelli,
“Constraints specification at a higher levels of abstraction,” Proc. of the Sixth IEEE International HighLevel Design Validation and Test Workshop, 2001.
[3] B. Bonakdarpour, S.Navabpour, S. Fischmeister, “Time-triggered runtime verification,” Form
Methods Syst Des, Springer, 2013.
[5] D. Gajski, F. Vahid, S. Narayan, and J. Gong, Specification and Design of Embedded Systems,
Prentice Hall, 1994.
[6] Chen, H. Hsieh, Y. Watanabe, and F. Balarin, "Automatic trace analysis for logic of constraints,"
Proc. of the 40th annual Design Automation Conference, p. 460, 2003.
[7] C. Denger, D. M. Berry, and E. Kamsties, "Higher Quality Requirements Specifications through
Natural Language Patterns," Proceedings of the IEEE International Conference on Software-Science,
Technology & Engineering, p. 80, 2003.
[8] M. B. Dwyer, G. S. Avrunin, J. C. Corbett, “Patterns in property specifications for finite-state
verification,” Proc. Of the 21st Int. Conf. on Software Engineering, pp. 441-420, IEEE Computer
Society Press, 1999.
[11] P. Hsia, J. Samuel, J. Gao, D. Kung, Y. Toyoshima, C. Chen, "Formal approach to scenario
analysis," IEEE Software, p. 33, 1994.
[12] O. Kupferman, M. Vardi, “Model checking of safety properties,” Computer aided verification
(CAV), pp 172–183, 1999.
[13] S. Konrad and B. H.C. Cheng, "Real-time specification patterns," Proc. of the 27th international
conference on Software engineering, p. 372, 2005.
[14] N. Moebius, K. Stenzel, W. Reif, “Generating formal specification for security-critical
applications: a model driven approach,” Proc. of the 2009 ICSE Workshop on Software Engineering for
Secure Systems, pp. 68-74, 2009.
[15] D. K. Peters, D. L. Parnas, “Requirements-based monitors for real-time systems,” IEEE Trans. on
Software Engineering, vol. 28, no. 2, pp. 146-157, Feb. 2002.
[16] S. Somé, R. Dssouli, and J. Vaucher, "From Scenarios to Timed Automata: Building Specifications
from Users Requirements," Second Asia-Pacific Software Engineering Conference, p. 48, 1995.
[18] W. Tsai, L. Yu, R. Paul, and X. Wei, "Rapid Pattern-Oriented Scenario-Based Testing for
Embedded Systems," Software Evolution with UML and XML, 2004.
[19] W. Tsai, L. Yu, F. Zhu, and R. Paul, "Rapid Embedded System Testing Using Verification
Patterns," IEEE Software, vol. 22, p. 68, July/Aug. 2005.