Upload
internet
View
103
Download
1
Embed Size (px)
Citation preview
1
PONTIFÍCIA UNIVERSIDADE CATÓLICA – PUCRS
FACULDADE DE INFORMÁTICA E FACULDADE DE ENGENHARIA
CURSO DE ENGENHARIA DE COMPUTAÇÃO
Porto Alegre, 11 de julho de 2008
VERIFICAÇÃO DA IMPLEMENTAÇÃO DO PROTOCOLO CCSDS do PUC#SAT usando PROMELA/SPIN
AutorAlexandre Gomes Madeira
OrientadorProf. Dr. Eduardo Bezerra
2
Introdução, Contexto, Objetivos
Metodologia Utilizada
Referencial Teórico
Modelagem e Codificação
Simulação e Verificação do Modelo
Conclusões e Resultados
Resumo
3
Introdução, Contexto, Objetivos
• “PUC#SAT – Interface de Telecomando e Telemetria CCSDS Visando Lógica
Reconfigurável”
- (PUC-RS, Agência Espacial Brasileira, INPE)
- Visa à implementação dos subsistemas de comunicação de bordo de veículos espaciais
utilizando lógica reconfigurável (FPGA’s)
• “Sistema de Telecomando CCSDS em FPGAs” [10]
- Modelagem e implementação do fluxo de Telecomando
segundo as recomendações do CCSDS¹
• Contexto do Trabalho
1 Consultative Committee for Space Data Systems
4
Introdução, Contexto, Objetivos
TelecommandSending-End
TelecommandReceiving-End
TelemetryReceiving-End
TelemetrySending-End
Ground Space
5
Introdução, Contexto, Objetivos
• Aprimorar os conhecimentos de modelagem e
verificação de sistemas
• Introdução de técnicas de verificação formal no
projeto PUC#SAT
• Validação da implementação do fluxo de Telecomando
• Procurar por possíveis erros de projeto ou desvios no
comportamento esperado do sistema
• Objetivos
6
Introdução, Contexto, Objetivos
Metodologia Utilizada
Referencial Teórico
Modelagem e Codificação
Simulação e Verificação do Modelo
Conclusões e Resultados
Resumo
7
Metodologia Utilizada
• Estudo do sistema implementado - fluxo de telecomando
(relatório de TC, código VHDL, máquinas de estado)
• Estudo da recomendação CCSDS para Telecomando
• Estudo da técnica de Model Checking
• Estudo da lógica LTL (Linear Temporal Logic)
• Geração de um Modelo do sistema
Abstração de detalhes
Codificação em PROMELA
8
Metodologia Utilizada
• Simulação e Verificação do modelo com
ferramenta de Model Checking
. Simulação randômica / guiada / interativa.
. Definição de propriedades a serem testadas.
. Representação das propriedades em LTL.
. Verificação das propriedades
• Análise dos resultados
9
Metodologia Utilizada
• Simulação VHDL x SPIN
10
Introdução, Contexto, Objetivos
Metodologia Utilizada
Referencial Teórico
Modelagem e Codificação
Simulação e Verificação do Modelo
Conclusões e Resultados
Resumo
11
Referencial Teórico
• CCSDS – Recomendações para Telecomando
Camadas definidas pelo CCSDS Camadas que foram implementadas
12
Referencial Teórico
• Model Checking
- Técnica de verificação automática de sistemas concorrentes finitos e
consiste das seguintes etapas:
- Modelagem. Consiste em representar o sistema estudado em um
determinado formalismo que permita a análise automática de sua
consistência lógica através de uma ferramenta.
- Especificação. Definição de algumas propriedades que o sistema deve
satisfazer em lógica temporal. CTL, LTL.
- Verificação. Verificação das propriedades especificadas de forma
automática.
13
Referencial Teórico
• Estrutura do verificador SPIN
- Trabalha com a linguagem de modelagem
PROMELA
- Verifica consistência lógica de modelos
- Detecção de erros em sistemas distribuídos
e protocolos de comunicação
- Mantido em constante desenvolvimento
- Gratuito, open source
- Grande base de usuários
- Documentação abundante
- Interface gráfica XSPIN. Facilita visualização
das simulações
- Contra-exemplos, Error Trace
14
Referencial Teórico
• Estrutura do verificador SPIN
- Modelo representado internamente como Autômato Finito.
- Realiza enumeração exaustiva de todos os estados alcançáveis do
modelo
- Técnicas Aumento do Desempenho:
• Partial Order Reduction (técnica de redução do espaço de estados, explora comutatividade de transições concorrentes);
• State Compression;
• Bitstate Hashing (utiliza apenas hashcode para armazenar estados);
• Weak Fairness enforcement;
15
Referencial Teórico
• PROMELA
(Process Meta Language). Linguagem não-determinística, utilizada para a construção de modelos de sistemas distribuídos. . Linguagem de descrição de sistemas, não de implementação. Ênfase na modelagem da sincronização e coordenação de processos e não na sua computação.
Características que diferenciam de uma linguagem comum:. Estruturas de controle não-determinísticas. Primitivas para criação de processos concorrentes. Primitivas de comunicação entre processos. Ausência de funções com retorno de valores. Ausência de ponteiros. Poucos tipos de dados. Não existe noção de tempo, ou Clock
16
Referencial Teórico
Baseia-se na utilização de 3 tipos de objetos. Processos (assíncronos, concorrentes). Objetos de Dados. Canais de Comunicação
• PROMELA
mtype = { SEQINI, SEQFIM, ACK, READY };
chan transf_ready = [1] of { mtype };
/* ...:: CAMADA DE SEGMENTAÇÃO ::... */
active proctype segm_test(){
codeblock buffer;mtype buff;
INICIO:printf("MSC: [INICIO]\n");again9: transf_ready?buff;if:: (buff == READY) -> goto VAI;:: else goto again9;fi;
.
.}
Exemplo de código
17
Referencial Teórico
• LTL (Linear Temporal Logic)
. Conjunto de proposições atômicas relacionadas por conectores
booleanos e operadores temporais.
. O tempo não é citado explicitamente, mas através de expressões
como: eventualmente, sempre, nunca, etc..
Proposições: p1, p2, q, r
Conectores lógicos: !, or, and, ->
Operadores temporais: X : next;
G : always (globally);
F : eventually (in the future);
U : until;
R : release.
Exemplo: G ( (p1 or p2) -> Fq )
Computation tree
18
Introdução, Contexto, Objetivos
Metodologia Utilizada
Referencial Teórico
Modelagem e Codificação
Simulação e Verificação do Modelo
Conclusões e Resultados
Resumo
19
Modelagem e Codificação
. Camadas modeladas como processos. Um processo por camada.
(FARM como processo separado devido à sua complexidade)
. Sinais de comunicação, barramentos, ports, modelados como canais
(canais bufferizados ou não bufferizados)
20
Modelagem e Codificação
• Camada de Codificação
active proctype coding() {/* layer2 states */#define L2_IDLE 0#define L2_RECEIVE_DATA 1.../* variaveis locais */mtype state = L2_IDLE;codeblock buffer1, buffer2;
/* transicoes */do:: if :: state == L2_IDLE -> printf("MSC: [_IDLE]\n"); again1: layer2_data_in?buffer1; if :: (buffer1.data == SEQINI) -> state = L2_RECEIVE_DATA; :: else -> goto again1; fi; :: state == L2_RECEIVE_DATA ->
21
Modelagem e Codificação
• Camada de CodificaçãoReceber um streaming de bits, identificar as sequências de início e fim e os codeblocks,
realizar a decodificação de cada codeblock a partir de suas informações de paridade, e
enviá-los a camada superior informando se há erro ou não.
Seqüência de Início
.
.
.Seqüência de Fim
22
Modelagem e Codificação
• Camada de Transferência
23
Modelagem e Codificação
• Camada de Transferência
24
Introdução, Contexto, Objetivos
Metodologia Utilizada
Referencial Teórico
Modelagem e Codificação
Simulação e Verificação do Modelo
Conclusões e Resultados
Resumo
25
Simulação e Verificação do Modelo
• Simulação das camadas
Simulação randômica: o código PROMELA é executado e sempre que houver mais de uma declaração válida para ser executada, uma delas é escolhida de forma não-determinística.
Simulação Guiada: é feita com base em um arquivo trail, que é um arquivo gerado automaticamente após a execução de uma verificação do SPIN, e contém um cenário que leva à alguma situação de erro encontrado durante a verificação, com o objetivo de facilitar a sua depuração.
Simulação interativa: cada vez em que a execução puder proceder em mais de um caminho diferente, será apresentado um menu para que o usuário escolha uma das opções possíveis.
A etapa de simulação permite ao projetista ganhar maior confiança no modelo gerado, bem como depurá-lo ou fazer ajustes de modo que este reflita o mais próximo possível o comportamento do sistema real.
26
Simulação e Verificação do Modelo
• Simulação das camadas- Processo é Iterativo: sucessivas simulações e ajustes no modelo
- Cada camada foi simulada individualmente com auxílio de processos simplificados para emular os sinais de comunicação.
27
Simulação e Verificação do Modelo
• Simulação do modelo Integrado
- Identificação de
comportamentos
inesperados do sistema
- Visualização da
dinâmica de troca de
mensagens entre os
processos
- Acompanhamento do
andamento da máquina
de estados
28
Simulação e Verificação do Modelo
• Verificação do modelo
O procedimento de verificação é executado como um processo iterativo em que o modelo tem o seu nível de detalhamento crescente. Durante a verificação serão checados violação de asserções, existência de estados não atingíveis e condições de corrida, entre outros.
29
Simulação e Verificação do Modelo
• Verificação de Propriedades
• Um frame recebido do tipo AD sempre implicará em uma ação de
descarte do FARM. (Falso)
[] (p -> <>q)
#define p (BLOCK2.header.frame_type == AD)
#define q (farm_action == farm_discard)
• Um frame recebido fora da janela de recebimento sempre deverá levar o
FARM ao estado de lockout. (Verdadeiro)
[] ( (p && q) -> r)
#define p (NS == 11)
#define q (FARM_VR == 3)
#define r (FARM_lockout_flag == 1)
- Convertidas em um autômato descrito em promela
- Código é inserido no modelo
30
Simulação e Verificação do Modelo
• Verificação de Propriedades
• Qualquer frame recebido do tipo BD sempre deverá ser aceito pelo FARM.
(Verdadeiro)
[](p - > <>q)
#define p (BLOCK2.header.frame_type == BD)
#define q (farm_action == farm_accept)
• Se o FARM se encontrar no estado de lockout, somente sairá deste estado
mediante o recebimento de um comando Unlock.
[]( p -> (p U q) )
#define p (FARM_lockout_flag == 1)
#define q (farm_event == E7)
31
Simulação e Verificação do Modelo
• Assertions
:: (state == FARM_RECEIVE) ->
printf("MSC: [RECEIVE]\n");
assert(f_valid_codeblock == 1);
transf_to_farm?buffer1;
:: state == L2_ERROR ->
printf("MSC: [_ERROR]\n");
assert(decBCH_status == 2);
again3: layer2_data_in?buffer1;
32
Simulação e Verificação do Modelo
• Invalid End States
end_again1: layer2_data_in?buffer1;
if
:: (buffer1.data == SEQINI) -> state = L2_RECEIVE_DATA;
:: else -> goto end_again1;
fi;
• Progress States
:: state == L2_IDLE ->
progress_l2_idle:
printf("MSC: [_IDLE]\n");
33
Introdução, Contexto, Objetivos
Metodologia Utilizada
Referencial Teórico
Modelagem e Codificação
Simulação e Verificação do Modelo
Conclusões e Resultados
Resumo
34
Conclusões e Resultados
• Trabalhos Futuros
. Definição e verificação de outros conjuntos de propriedades
(específicos a cada aplicação)
. Verificação do módulo de Telemetria e do sistema completo
(ainda não implementados)
• Resultados
. Estudo das técnicas de Model Checking
. Introdução da verificação formal no projeto PUC#SAT
. Validação de alguamas funcionalidades básicas
. Inesistência de erros graves