Verificação Automatizada de Sistemas de Tempo Real Críticos
-
Upload
joel-carvalho -
Category
Documents
-
view
228 -
download
0
Transcript of Verificação Automatizada de Sistemas de Tempo Real Críticos
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
1/133
Joel Silva Carvalho
Verificao Automatizada
de Sistemas de Tempo Real Crticos
Universidade da Beira Interior
Departamento de Informtica
Junho 2009
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
2/133
Joel Silva Carvalho
Verificao Automatizadade Sistemas de Tempo Real Crticos
Dissertao referente aos trabalhos de investigao conducentes
obteno do grau de Mestre em Engenharia Informtica,
Orientado pelo Professor Doutor Simo Melo de Sousa
Universidade da Beira Interior
Departamento de Informtica
Junho 2009
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
3/133
Agradecimentos
Agradeo ao meu orientador (Doutor Simo Melo de Sousa) a liberdade, apoio e
orientao nas escolhas que me levaram apresentao desta dissertao. Os ob-
jectivos foram definidos com o seu consentimento e felizmente cumpridos. Apesar
de a dissertao focar uma linguagem acadmica, com visibilidade menor do que
algumas solues industriais, devo admitir ter desde j atingido um momento de
realizao pessoal.
Agradeo ainda aos meus pais (Prazeres Barata da Silva Gouveia de Carvalho e
Jos Antnio Chaves de Carvalho) por terem possibilitado a realizao deste sonho.
Sem eles no teria tidoo financiamento e apoio necessrio para o percurso acadmico
realizado. Num pas onde se apoia e avalia de forma estranha a investigao e oensino, s alguns conseguem este privilgio.
Agradeo tambm aos meus colegas do Release, do Socia e do NMCG pelo
companheirismo e bom ambiente proporcionado nos diversos momentos do dia-a-
dia. Bem como aos professores que tive ao longo de todo meu percurso acadmico
e aos elementos do projecto RESCUE que contriburam para o enriquecimento dos
meus conhecimentos.
Por fim agradeo a todos os meus familiares e amigos pelo apoio.
iii
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
4/133
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
5/133
Contedo
Agradecimentos iii
Contedo v
Lista de Figuras xi
Acrnimos xiii
1 Introduo 1
1.1 Objectivo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Motivao e Contribuio . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Organizao do relatrio . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2 Verificao de Sistemas de Tempo Real 5
2.1 Sistemas de Tempo Real . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.1.1 Definies e Caractersticas . . . . . . . . . . . . . . . . . . . . 5
2.1.2 Classificao dos sistemas de tempo real . . . . . . . . . . . . 6
2.1.2.1 Quanto criticidade do sistema . . . . . . . . . . . . 7
2.1.2.2 Quanto criticidade das tarefas . . . . . . . . . . . . 7
2.1.2.3 Quanto natureza temporal . . . . . . . . . . . . . . 7
2.1.3 Tolerncia a Falhas . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.1.4 Linguagens de Programao . . . . . . . . . . . . . . . . . . . 9
2.1.5 Sistemas Operativos . . . . . . . . . . . . . . . . . . . . . . . . 10
2.1.6 Escalonamento de tempo real . . . . . . . . . . . . . . . . . . . 10
v
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
6/133
2.1.6.1 Earliest Deadline First . . . . . . . . . . . . . . . . . . 12
2.2 Mecanismos de Verificao . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.1 Verificao Esttica . . . . . . . . . . . . . . . . . . . . . . . . . 132.2.1.1 Perfil Ravenscar . . . . . . . . . . . . . . . . . . . . . 14
2.2.1.2 SPARK (industrial) . . . . . . . . . . . . . . . . . . . 15
2.2.1.3 Giotto (acadmico) . . . . . . . . . . . . . . . . . . . 17
2.2.1.4 Schedule Carrying Code (acadmico) . . . . . . . . . 19
2.2.1.5 xGiotto (acadmico) . . . . . . . . . . . . . . . . . . . 19
2.2.1.6 TDL e HTL . . . . . . . . . . . . . . . . . . . . . . . . 20
2.2.2 Verificao de Modelos . . . . . . . . . . . . . . . . . . . . . . . 212.3 Concluso . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3 UPPAAL 25
3.1 Sistemas de Autmatos . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.1.1 Autmato . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.1.2 Caminho . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.1.3 Execuo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 273.1.4 Extenses de Autmatos . . . . . . . . . . . . . . . . . . . . . . 27
3.1.5 Redes de Autmatos/Produto Sincronizado . . . . . . . . . . 28
3.1.6 Grafo de Acessibilidade . . . . . . . . . . . . . . . . . . . . . . 28
3.1.7 Sincronizaes . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2 Autmatos Temporizados . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2.1 Relgios e Transies . . . . . . . . . . . . . . . . . . . . . . . . 30
3.2.2 Configurao e Execuo . . . . . . . . . . . . . . . . . . . . . 30
3.2.3 Redes e Sincronizaes . . . . . . . . . . . . . . . . . . . . . . . 31
3.2.4 Invariantes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.2.5 Estados e Sincronizaes Urgentes . . . . . . . . . . . . . . . . 32
3.2.6 Autmato de teste . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.3 Lgica Temporal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.3.1 Full Computation Tree Logic . . . . . . . . . . . . . . . . . . . 33
vi
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
7/133
3.3.1.1 Sintaxe (formato Backus-Naur Form (BNF)) . . . . . 33
3.3.1.2 LTL vs CTL . . . . . . . . . . . . . . . . . . . . . . . . 33
3.3.1.3 Estruturas de Kripke . . . . . . . . . . . . . . . . . . 343.4 Timed Computation Tree Logic . . . . . . . . . . . . . . . . . . . . . . 35
3.4.1 Sintaxe (formato BNF) . . . . . . . . . . . . . . . . . . . . . . . 35
3.4.2 Exemplo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.5 A ferramenta . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.5.1 Modelao . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.5.2 Verificao . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.5.3 Ferramentas Derivadas . . . . . . . . . . . . . . . . . . . . . . 393.6 Concluso . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
4 Hierarchical Timing Language 41
4.1 Logical Execution Time . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.2 Sintaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.2.1 program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
4.2.2 communicator . . . . . . . . . . . . . . . . . . . . . . . . . . . . 444.2.3 module . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.2.4 port . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4.2.5 task . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4.2.6 mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
4.2.7 invoke . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
4.2.8 switch . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.3 Caractersticas Principais . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.3.1 Refinamento . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.3.2 Distribuio da Computao . . . . . . . . . . . . . . . . . . . 50
4.3.3 Comunicao Inter-Tarefas . . . . . . . . . . . . . . . . . . . . 51
4.3.4 Comunicao Directa de Tarefas . . . . . . . . . . . . . . . . . 52
4.3.5 Composio Sequencial . . . . . . . . . . . . . . . . . . . . . . 53
4.3.6 Composio Paralela . . . . . . . . . . . . . . . . . . . . . . . . 53
vii
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
8/133
4.4 Compilador HTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4.4.1 Well-Formedness . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.4.1.1 Restries nos Programas . . . . . . . . . . . . . . . . 554.4.1.2 Restries nos Comunicadores . . . . . . . . . . . . . 55
4.4.1.3 Restries nas Invocaes de Tarefas . . . . . . . . . 55
4.4.1.4 Restries nos Refinamentos . . . . . . . . . . . . . . 56
4.4.2 Well-Timedness . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
4.4.3 HTL-Simulink Tool Chain . . . . . . . . . . . . . . . . . . . . . 56
4.5 Concluso . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5 HTL2XTA, O Tradutor 59
5.1 Automatizao da Verificao . . . . . . . . . . . . . . . . . . . . . . . 60
5.1.1 Traduo do Modelo . . . . . . . . . . . . . . . . . . . . . . . . 61
5.1.2 Inferncia de Propriedades . . . . . . . . . . . . . . . . . . . . 63
5.2 Algoritmo de Traduo do Modelo . . . . . . . . . . . . . . . . . . . . 64
5.2.1 Consideraes Iniciais . . . . . . . . . . . . . . . . . . . . . . . 65
5.2.1.1 Mudana de Modo . . . . . . . . . . . . . . . . . . . 655.2.1.2 Tipos e Drivers de Inicializao . . . . . . . . . . . . 66
5.2.1.3 Declarao de Tarefas . . . . . . . . . . . . . . . . . . 66
5.2.1.4 Declarao de Comunicadores . . . . . . . . . . . . . 66
5.2.1.5 Declarao de Portos . . . . . . . . . . . . . . . . . . 67
5.2.2 Transposio do LET . . . . . . . . . . . . . . . . . . . . . . . . 67
5.2.2.1 Invocaes de tarefas . . . . . . . . . . . . . . . . . . 68
5.2.2.2 taskTA . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
5.2.2.3 taskTA_S . . . . . . . . . . . . . . . . . . . . . . . . . 69
5.2.2.4 taskTA_R . . . . . . . . . . . . . . . . . . . . . . . . . 70
5.2.2.5 taskTA_SR . . . . . . . . . . . . . . . . . . . . . . . . 71
5.2.2.6 Comunicao Directa . . . . . . . . . . . . . . . . . . 72
5.2.3 Mdulos e Modos . . . . . . . . . . . . . . . . . . . . . . . . . 72
5.2.3.1 Refinamentos . . . . . . . . . . . . . . . . . . . . . . . 74
viii
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
9/133
5.3 Algoritmo de Traduo das Propriedades . . . . . . . . . . . . . . . . 75
5.3.1 Ausncia de Bloqueio . . . . . . . . . . . . . . . . . . . . . . . 76
5.3.2 Perodo dos modos . . . . . . . . . . . . . . . . . . . . . . . . . 76
5.3.3 Invocaes de tarefas . . . . . . . . . . . . . . . . . . . . . . . . 76
5.3.4 LET das tarefas . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
5.3.5 Refinamentos . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
5.4 Concluso . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
6 Validao Experimental 79
6.1 Caso de Estudo - 3TS . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
6.1.1 3ts-simulink . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
6.1.2 Modelo Uppaal . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
6.1.3 Simulao Uppaal . . . . . . . . . . . . . . . . . . . . . . . . . 85
6.1.4 Verificao Uppaal . . . . . . . . . . . . . . . . . . . . . . . . . 86
6.2 Outros Resultados . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
6.3 Concluso . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
7 Concluso 917.1 Contributo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
7.2 Desafio . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
7.3 Trabalho Futuro . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
A rvore de Sintaxe Abstracta do HTL2XTA 95
B .HTL - 3TS Java Simulator 97
C .XTA - 3TS Java Simulator 99
D .Q - 3TS Java Simulator 105
E .VRF - 3TS Java Simulator 111
Referncias 115
ix
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
10/133
x
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
11/133
Lista de Figuras
4.1 Timeline de alguns mecanismos de verificao . . . . . . . . . . . . . 41
4.2 Logical Execution Time [17] . . . . . . . . . . . . . . . . . . . . . . . . 42
4.3 Comunicao por comunicadores [29] . . . . . . . . . . . . . . . . . . 51
4.4 Comunicao por Ports [29] . . . . . . . . . . . . . . . . . . . . . . . . 52
4.5 Esquema do Compilador HTL [29] . . . . . . . . . . . . . . . . . . . . 54
4.6 Esquema HTL-Simulink Tool-Chain [29] . . . . . . . . . . . . . . . . . 57
4.7 Modelo Temporal de um Programa HTL [29] . . . . . . . . . . . . . . 57
5.1 Esquema HTL2XTA Tool-Chain . . . . . . . . . . . . . . . . . . . . . . 60
5.2 Autmato taskTA esquerda e instanciao direita . . . . . . . . . . 685.3 Autmato taskTA_S esquerda e taskTA_R direita . . . . . . . . . . 70
5.4 Autmato taskTA_SR . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
5.5 Autmatos de mdulo, com um modo esquerda e dois modos
direita . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
6.1 Planta Real do 3TS [29] . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
6.2 Mdulo IO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
6.3 Mdulo T1 e Mdulo T2 . . . . . . . . . . . . . . . . . . . . . . . . . . 82
6.4 Mdulo T1_P_PI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
6.5 Mdulo T2_P_PI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
6.6 Simulao do 3TS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
6.7 Modelo Temporal [29] . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
6.8 Verificao do 3TS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
xi
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
12/133
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
13/133
Acrnimos
Release RELiablE And SEcure Computation Group
RESCUE REliable and Safe Code execUtion for Embedded systems
HTL Hierarchical Timing Language
TDL Timing Definition Language
CTL Computation Tree Logic
CTL* Full Computation Tree Logic
TCTL Timed Computation Tree Logic
LTL Linear Temporal Logic
LET Logical Execution Time
SCC Schedule Carrying Code
xGiotto eXtended Giotto
IRTAW International Real-Time Ada Workshop
PCC Proof Carrying Code
EDF Earliest Deadline First
EAL Evaluation Assurance Level
CC Common Criteria
E-Code Embedded Code
xiii
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
14/133
xiv ACRNIMOS
HE-Code Hierarchical Embedded Code
E-Machine Embedded Machine
HE-Machine Hierarchical Embedded Machine
S-Code Scheduling Code
WCET Worst-Case Execution Time
WCTT Worst-Case Transmission Time
3TS Tree Tank System
ECU Engine Control Unit
ABS Anti-lock Braking System
DBC Design By Contract
SCC Schedule Carrying Code
RAT Rede de Autmatos Temporizados
LPTA Linearly Priced Timed Automata
BNF Backus-Naur Form
AST Abstract Syntax Tree
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
15/133
Captulo 1
Introduo
A miniaturizao das componentes electrnicas permite que os sistemas computa-
cionais tenham uma proliferao acelerada. Estes sistemas esto integrados nos
mais diversos meios, por exemplo, no carto do cidado, nos telemveis, nos
automveis, nos avies, entre outros.
Novas exigncias surgem com a evoluo destes sistemas computacionais. De
facto, a capacidade de processamento, por si s, j no suficiente para o preenchi-
mento de todos os requisitos industriais. Nos sistemas crticos a segurana e afiabilidade so os aspectos fundamentais. Apesar de ser importante, no basta
reunir condies tcnicas para executar um dado conjunto de tarefas num sistema,
preciso que o sistema (como um todo) execute correctamente essas tarefas (cap. 2).
1.1 Objectivo
Esta dissertao foca-se no estudo da fiabilidade de um subconjunto de sistemas
computacionais, mais precisamente os Sistemas de Tempo Real Crticos (cap. 2).
Comparativamente com os sistemas tradicionais, os sistemas de tempo real acres-
centam, questo da fiabilidade, a necessidade intrnseca de algo ser executado
num intervalo de tempo bem definido. Para este tipo de sistemas, no se conseguir
finalizar uma tarefa, no tempo que devido, corresponde sumariamente a uma
falha do sistema.
1
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
16/133
2 CAPTULO 1. INTRODUO
Enquadrada no RELiablE And SEcure Computation Group (Release) e no pro-
jecto REliable and Safe Code execUtion for Embedded systems (RESCUE), esta
dissertao teve como ponto de partida um estudo sobre os sistemas de tempo
real e sobre os diversos mecanismos de verificao aplicados neles (cap. 2). Aps
terem sido identificadas as linguagens de interesse, foi definido como objectivo
principal da dissertao a implementao de um tradutor automatizado da lin-
guagem Hierarchical Timing Language (HTL) (cap. 4) para Uppaal (cap. 3). Este
tradutor enquadra-se numa Tool-Chain que estende a verificao de programas HTL
recorrendo a um mecanismo de verificao formal.
Sendoo HTL umalinguagem de coordenao, capaz de verificar o escalonamento
de programas, constatou-se que a mesma podia ser complementada com outro
mecanismo de verificao, nomeadamente o Model Checking (doravante verificao
de modelos). O tradutor apresentado nesta dissertao (cap. 5) constri, de forma
automatizada, modelos com base em programas HTL e especifica propriedades
sobre os modelos. Aps serem verificadas pelo Model Checker Uppaal (cap. 3),
as propriedades permitem estabelecer uma relao entre o que o programador
produziu e aquilo que se pretende do sistema. Esta relao no completa, umavez que s possvel verificar propriedades temporais sobre as tarefas, mas sempre
complementa a verificao de escalonamento feita pelo HTL. De notar ainda que,
a especificao automatizada de propriedades pode ser enriquecida manualmente
permitindo a verificao de requisitos temporais no inferidos pelo tradutor.
1.2 Motivao e Contribuio
Aps ter estudado computao ubqua, na realizao do projecto de final de curso,
a conscincia para a dependncia de todo o tipo de sistemas computacionais
aumentou. Neste sentido foi impossvel ficar indiferente aos desafios inerentes
ao desenvolvimento de aplicaes para sistemas embebidos. Para alm da vontade
de estudar sistemas embebidos e sistemas de tempo real, existiu sempre a esperana
e vontade de poder contribuir com algo na verificao deste tipo de sistemas.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
17/133
1.3. ORGANIZAO DO RELATRIO 3
A liberdade na escolha das linguagens permitiu abordar algo menos conven-
cional. No conjunto de mecanismos de verificao e linguagens estudadas era
evidente que, dado o contexto, seria mais arriscado mas mais interessante focar o
estudo numa linguagem acadmica como o HTL. Assim, para alm do estudo dosdiversos mecanismos de verificao aplicados nos sistemas de tempo real (cap. 2),
do estudo mais aprofundado do Uppaal (cap. 3) e do HTL (cap. 4) destaca-se a
implementao de um mecanismo de traduo automatizado (cap. 5) que contribui
na verificao dossistemasde tempo real desenvolvidos em HTL. O funcionamento
do tradutor foi confirmado com a execuo (simulao) e verificao dos casos de
estudo disponveis para o HTL no Uppaal, sendo que nesta dissertao apenas
apresentado detalhadamente o caso de estudo mais recorrente (cap. 6).
1.3 Organizao do relatrio
Este documento estrutura-se da seguinte forma.
Cap. 1 - Introduo Enquadramento do trabalho desenvolvido no mbito da
dissertao.
Cap. 2 - Verificao de Sistemas de Tempo Real Numa primeira fase deste
captulo so apresentados conceitos fundamentais aos sistemas de tempo real.
Numa segunda fase so apresentados os mecanismos de verificao estudados.
Cap. 3 - UPPAAL Introduo de alguns conceitos para uma melhor compreenso
das potencialidades da verificao de modelos, baseada em autmatos temporiza-
dos e lgica temporal, quer isolada como enquadrada com outros mecanismos de
verificao.
Cap. 4 - Hierachichal Timing Language Apresentao da sintaxe da linguagem
HTL, sntese das caractersticas principais da linguagem e descrio do funciona-
mento do compilador.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
18/133
4 CAPTULO 1. INTRODUO
Cap. 5 -HTL2XTA,OTradutor Descriodoalgoritmodetraduoeapresentao
das capacidades e fraquezas do tradutor.
Cap. 6 - Validao Experimental Apresentao de um caso de estudo em partic-
ular, bem como sntese dos resultados obtidos na verificao e execuo de outros
casos.
Cap. 7 - Concluso Apresentao de mais algumas consideraes sobre a disser-
tao.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
19/133
Captulo 2
Verificao de Sistemas de Tempo Real
Ao longo deste captulo so apresentados conceitos fundamentais aos sistemas de
tempo real e sua verificao. Numa primeira parte (referncia principal [36]),
os conceitos so apresentados de forma sucinta para uma familiarizao com o
vocabulrio e para reflexo sobre alguns cuidados necessrios no desenvolvimento
de sistemas de tempo real. Numa segunda parte, apresentado o estudo feito sobre
os mecanismos de verificao utilizados neste tipo de sistemas.
2.1 Sistemas de Tempo Real
2.1.1 Definies e Caractersticas
Um sistema embebido um sistema computacional dedicado realizao de tarefas
especficas. Este tipo de sistemas distingue-se dos sistemas de propsito geral
(desktop, laptop, netbook, etc.) pelas suas limitaes e enfoque nas tarefas. Essas
limitaes so as mais diversas, desde a necessidade de serem de dimensesreduzidas, passando por limitaes energticas e acabando na capacidade reduzida
de processamento e armazenamento. Bons exemplos de sistemas embebidos so, os
telemveis, os PDAs, os Smart Card, as mquina fotogrfica, os micro ondas, entre
outros.
Os sistemas de tempo real so geralmente sistemas embebidos porque controlam
um sistema genrico [32]. No entanto, um sistema de tempo real um sistema
5
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
20/133
6 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
em que a correco das tarefas depende do resultado lgico da computao e do
instante em que so executadas. Alguns exemplos de sistemas de tempo real so,
os Anti-lock Braking System (ABS) dos carros, as Engine Control Unit (ECU) (mais
tradicionalmente conhecidas por centralinas), os Pacemakers, entre outros.
Ao contrrio do que o nome pode sugerir, este tipo de sistemas no implica
que o tempo de resposta seja imediato. Implica sim, que o tempo resposta seja
adequado independentemente da unidade temporal (milissegundos, segundos,
etc.). O tempo de resposta no depende do tempo mdio de execuo das tarefas,
mas do Worst-Case Execution Time (WCET). Em mdia os requisitos temporais
podem ser cumpridos, mas se no pior caso no forem o sistema fica comprometido.
...e ento h um homem que se afogou ao atravessar uma corrente com
uma profundidade mdia de seis polegadas... Stankovic em [42]
Segundo Stankovic [41], o importante nos sistemas de tempo real a previsi-
bilidade e no a rapidez. Os requisitos temporais necessitam de ser conhecidos
partida e deve ser possvel identificar quais as tarefas que no cumprem com os
requisitos temporais. Como vai ser possvel perceber, este aspecto introduz muitas
limitaes na verificao dos sistemas de tempo real. Quanto mais determinista for
o sistema mais simples verificar propriedades sobre ele.
Outra caracterstica inerente aos sistemas de tempo real reside na concorrncia
das tarefas. Estes sistemas executam mltiplas tarefas de forma concorrente para
conseguir interagir com o ambiente envolvente.
2.1.2 Classificao dos sistemas de tempo real
Uma vez que os sistemas de tempo real se diferenciam pelas suas caractersticas
necessrio classifica-los. De seguida apresentam-se trs classificaes seleccionadas
de um conjunto maior. Dado que a dissertao aborda questes de periodicidade
de tarefas, e estando a verificao mais relacionada com sistemas crticos, estas
classificaes so imprescindveis.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
21/133
2.1. SISTEMAS DE TEMPO REAL 7
2.1.2.1 Quanto criticidade do sistema
Na classificao quanto criticidade do sistema, diz-se que um sistema de tempo
real crtico (Hard Real-Time Systems) implica o cumprimento de todos os requisitostemporais. O no cumprimento de um requisito pode implicar a falha do sistema,
situao que no desejada. Neste tipo de sistemas inclui-se, por exemplo, o sistema
de navegao de uma aeronave.
Por sua vez um sistemas de tempo real no crtico (Soft Real-Time Systems) no
implica o cumprimento de todos os requisitos temporais. O seu cumprimento
desejado mas, quando no verificado, no origina uma falha do sistema. Neste tipo
inserem-se, por exemplo, as consolas de jogos.
2.1.2.2 Quanto criticidade das tarefas
Na classificao quanto criticidade das tarefas diz-se que uma tarefa crtica
aquela em que o no cumprimento do requisito temporal associado implica uma
falha no sistema.
Uma tarefa firme aquela em que o resultado obtido deixa de ser til. Neste tipode tarefas as consequncias do incumprimento do requisito temporal tornam-se
irrelevantes.
Por fim, a tarefa no crtica, aquela em que o resultado obtido continua a ter um
valor decrescente, mas no qual o incumprimento do requisito temporal no implica
uma falha.
2.1.2.3 Quanto natureza temporal
Neste tipo de classificao, diz-se que as tarefas peridicas so aquelas que so
executadas com um perodo fixo (de x em x unidades de tempo). Este tipo de tarefas
bastante utilizado na leitura de dados de sensores ou na gesto de actuadores.
As tarefas no peridicas so aquelas cujo conhecimento prvio sobre o instante
da prxima execuo nulo.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
22/133
8 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
As tarefas aperidicas, so aquelas que no so crticas e simultaneamente no
so peridicas.
Por fim as tarefas espordicas, so aquelas que so crticas e no so peridicas.
2.1.3 Tolerncia a Falhas
Nos sistemas crticos, a possibilidade de existirem perdas de vidas humanas ou
perdas materiais relevantes, do ponto de vista financeiro, deve ser a mais reduzida
possvel. Para alm da utilizao de mtodos formais durante o desenvolvimento eda fase de testes no fim do desenvolvimento, muitas vezes necessrio acrescentar
a utilizao de mecanismos de tolerncia a falhas.
Este tipo de mecanismos permite que o sistemacontinue em funcionamento sobre
a presena de falhas [40]. No entanto os algoritmos de deteco e correco de
falhas introduzem um custo adicional de overhead. Assim eles devem ser previstos
e introduzidos desde cedo no processo de desenvolvimento, para que os requisitos
temporais contemplem a deteco e correco de falhas em tempo de execuo.
Estes mecanismos consistem muitas vezes na introduo de redundncia no
sistema, quer do ponto de vista espacial (replicao de componentes)comotemporal
(repetio da execuo de tarefas) [40]. No entanto isto pode ser prejudicial
previsibilidade do sistema, pelo que a redundncia tem que ser feita garantindo a
preservao da previsibilidade e fiabilidade do sistema.
Um dos resultados clssicos da engenharia de software refere que cerca de vintevezes mais complicado corrigir uma falha depois do sistema estar desenvolvido.
Deste modo, o interesse em evitar falhas durante o desenvolvimento continua a ser
predominante.
O uso de um processo slido de desenvolvimento um bom passo
na direco certa, mas outros podem ser dados, como por exemplo, a
utilizao de ferramentas automticas para maior parte do processo, ou
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
23/133
2.1. SISTEMAS DE TEMPO REAL 9
a utilizao de mtodos formais... Lus Miguel Pinho em [36]
2.1.4 Linguagens de ProgramaoExistem vrias linguagens de programao para sistemas de tempo real e todas elas
possuem as suas caractersticas, no entanto baseiam-se nalguns requisitos.
No que respeita segurana, as linguagens fortemente tipadas so preferveis
porque permitem forar o programador a evitar alguns erros de utilizao de var-
iveis. A utilizao de recursividade e apontadores deve ser cuidada, preferencial-
mente at evitada. Estas duas tcnicas reduzem significativamente a previsibilidade
do sistema.
Relativamente flexibilidade, a linguagem deve possuir mecanismos capazes
de evitar o uso de construes especficas ao hardware ou linguagem assembly, no
entanto nem sempre assim acontece. Os motivos so diversos, mas basta pensar
que por vezes os requisitos temporais so de tal forma complicados de atingir, que
necessrio optimizar o cdigo para utilizar caractersticas especificas do hardware
ou do sistema operativo.
Quantomaior foro uso destas tcnicas menos portvel vai sero cdigo. Mas como
os sistemas de tempo real baseiam-se na avaliao e cumprimento de requisitos
temporais, a eficincia fundamental. Aumentando a eficincia com as tcnicas re-
latadas reduz-se a portabilidade, e vice-versa. Por outro lado, as linguagens devem
ser suficientemente simples para permitir implementaes fiveis dos compiladores
e de outras ferramentas. Assim, a linguagem ou um subconjunto da mesma deve
ser suficiente para permitir algum tipo de verificao formal.
Facilmente se define aqui um ciclo vicioso, no existe nenhuma linguagem
perfeita mas sim linguagens que so mais adequadas para um determinado tipo
de sistemas e outras para outros. As linguagens de programao, para sistemas de
tempo real, devem suportar concorrncia, o que implica de alguma forma a capaci-
dade de construo de mdulos, a criao e gesto de tarefas, a comunicao entre
tarefas, a excluso no acesso a recursos, a utilizao de interrupes e dispositivos
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
24/133
10 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
de entrada e sada, o tratamento de excepes e a previsibilidade. Quando estas
caractersticas no so suportadas pela linguagem de programao ento devem
ser suportadas pelo sistema operativo.
2.1.5 Sistemas Operativos
Apesar de algumas linguagens permitirem criar aplicaes para sistemas de tempo
real sem a necessidade de utilizao de um sistema operativo, estes tornam a
programao mais abstracta. Tal como um sistema operativo tradicional, um
sistema operativo de tempo real precisa de mdulos para gesto de tarefas, gesto
de memria, comunicao e sincronizao entre tarefas e gesto de entradas/sadas.
Focando apenas o aspecto relevante para esta dissertao, identifica-se como
funo principal do mdulo de gesto de tarefas o escalonador. O mdulo de
gesto de tarefas responsvel pelo escalonamento bem como pelo despacho. O
despacho altera o contexto da tarefa que est a ser executada pelo da prxima
tarefa. Enquanto o escalonador responsvel por seleccionar qual a prxima tarefa
a executar atravs da implementao de algoritmos de escalonamento.
2.1.6 Escalonamento de tempo real
Nos sistemas de tempo real a especificao dos requisitos inclui informao tem-
poral na forma de prazos de execuo [9]. Estes prazos de execuo, so como j
foi referido, de importncia extrema. Para um correcto funcionamento do sistema
necessrio garantir que as tarefas so executadas respeitando os seus requisitos
temporais.
O processo de escalonamento consiste em distribuir eficientemente o acesso aos
recursos e providenciar tempo de processamento s tarefas para cumprirem os
seus requisitos temporais. O estudo do escalonamento nos sistemas de tempo real
difere dos sistemas tradicionais e como tal no deve ser confundido. Nos sistemas
tradicionais o escalonamento pretende apenas minimizar o tempo necessrio para
execuo de todas as tarefas. Nos sistemas de tempo real o escalonamento pretende
cumprir os requisitos temporais de cada tarefa.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
25/133
2.1. SISTEMAS DE TEMPO REAL 11
Os algoritmos de escalonamento de tempo real podem dividir-se em dois conjun-
tos diferentes, os algoritmos estticos e os algoritmos dinmicos. Estes diferem no
facto do sistema ter ou no conhecimento prvio sobre as caractersticas das tarefas.
Deste modo, os algoritmos estticos planeiam o escalonamento antes mesmo
da execuo das tarefas. Basta para isso que o algoritmo tenha conhecimento da
totalidade das tarefas e dos seus requisitos. Estes algoritmos podem-se dividir de
duas formas:
- Algoritmosbaseadosemtabelas-Nestesalgoritmosoescalonamentoplaneado
antes da execuo e concretizado na construo de tabelas que determinam
quandoumatarefadeveiniciarasuaexecuo. Estesalgoritmossoutilizados
quando as tarefas so peridicas ou podem ser transformadas em tal.
- Algoritmos baseados em prioridades - Nestes algoritmos o escalonamento
baseado em prioridades atribudas antes da execuo de modo a que a cada
instante da execuo seja definida qual a tarefa que processada.
Por sua vez, os algoritmos dinmicos apenas necessitam ter conhecimento dastarefas activas e dos seus requisitos uma vez que o escalonamento feito em tempo
de execuo. Estes algoritmos podem-se dividir de duas formas:
- Algoritmos baseados em planeamento - Nestes algoritmos o escalonamento
adaptado aquando da chegada de uma nova tarefa de modo a que o novo
escalonamento consiga cumprir simultaneamente os requisitos da nova tarefa
e das tarefas anteriormente escalonadas.
- Algoritmos baseados no melhor esforo - Nestes algoritmos no feito um
novo escalonamento aquando da chegadade umanovatarefa. Inclusivamente
a tarefa executada sem o sistema saber se vai conseguir cumprir os seus
requisitos temporais. Este tipo de algoritmos bastante utilizado nos sistemas
de tempo real em que a prioridade das tarefas determinada durante a
execuo, tendo em consideraoas caractersticas das tarefasactivas. A maior
desvantagem deste tipo de algoritmos reside na sua falta de previsibilidade.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
26/133
12 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
2.1.6.1 Earliest Deadline First
O Earliest Deadline First (EDF) um algoritmo de escalonamento dinmico por
prioridades. Este algoritmo baseia-se na atribuio da maior prioridade tarefacujo prazo temporal est mais prximo do fim. Ou seja dada prioridade tarefa
com menor tempo para concluso dentro dos limites temporais definidos.
Este algoritmo considerado ptimo uma vez que existindo um conjunto de
tarefas possveis de serem escalonadas (respeitando os limites temporais) o algo-
ritmo consegue proceder ao seu escalonamento efectivo. No entanto, ele no tem
capacidades de previsibilidade quando um escalonamento efectivo no possvel.
Ou seja, no sendo cumpridos todos os requisitos temporais, o algoritmo no capaz de identificar qual a tarefa ou quais as tarefas que no vo ser cumpridas de
acordo com os requisitos.
2.2 Mecanismos de Verificao
Nesta dissertao entende-se por mecanismos de verificao aqueles que esto
directamente associados aos mtodos formais. Isto , mecanismos baseados emalgoritmos matemticos, capazes de construir ou utilizar provas que determinem a
veracidade de certas propriedades do sistema.
The term formal methods refers to the use of mathematical modeling,
calculation and prediction in the specification, design, analysis and
assurance of computer systems and software. The reason it is called
formal methods rather than mathematical modeling of software is to
highlight the character of the mathematics involved. John Rushby em
[38].
H cerca de 14 anos foi estimado que qualquer pessoa era diariamente con-
frontada com cerca de 25 dispositivos computacionais [4], hoje estes valores so
muito superiores e difceis de quantificar. A nossa dependncia por estes sistemas
cada vez maior. Um bom exemplo disso consiste na utilizao de armas de impulso
electromagnticoparaimobilizarveculosmotorizadosdenovagerao. Jlvoos
temposemqueapolciasconseguiaimobilizarumveculomotorizadobloqueando
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
27/133
2.2. MECANISMOS DE VERIFICAO 13
o caminho, furando os pneus, etc. Este exemplo torna-se ainda mais interessante
considerandoquepartedaelectrnicaestdissimuladaemmecanismosdecontrolo.
Um carro da dcada de 90, exposto utilizao de uma arma destas, no fica
imobilizado mas fica com todo o sistema elctrico danificado. Um carro maisrecente fica com a ECU danificada o que implica a imobilizao do veculo.
Parte destes sistemas so construdos sem qualquer utilizao de mtodos for-
mais. Prova disso reside na falta de fiabilidade dos telemveis, quantas vezes no
necessrio desligar e voltar a ligar estes dispositivos para que voltem a funcionar
correctamente? A utilizao de mecanismo de verificao contnua quase sempre
associada a sistemas crticos. Como j foi referido, um sistema crtico pode ser
entendido como aquele que, em caso de falha, pode por em risco vidas humanas ou
investimentos onerosos. Fala-se geralmente deste tipo de sistemas em reas como
a aeronutica, o aeroespacial, os caminhos-de-ferro, nas centrais nucleares, etc.
As mentalidades e exigncias de mercado mudam e cada vez mais as empresas
procuram oferecer produtos de qualidade certificada. Neste sentido a norma ISO-
15408, designada por Common Criteria (CC), introduziu um modelo de avaliao
da segurana e fiabilidade de sistemas. Este modelo divide-se numa mtrica de7 nveis de confiana designado por Evaluation Assurance Level (EAL). Para os
nveis mais elevados (EAL 5 a 7) os mtodos formais so obrigatrios.
2.2.1 Verificao Esttica
Nesta dissertao vo ser abordados dois tipos de mecanismos de verificao. O
primeiro consiste nos mecanismos de verificao esttica e o segundo nos mecanis-
mos de verificao de modelos.
O primeiro faz uso de processos de verificao em tempo de compilao que
permitem libertar recursos na execuo. Este facto torna este tipo de verificao
bastante interessante para os sistemas de tempo real. Tudo o que puder ser feito em
tempo de compilao, no vai ser feito em tempo de execuo para que os requisitos
temporais sejam mais facilmente atingveis.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
28/133
14 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
A verificao esttica est correlacionada com a linguagem de programao. O
prprio compilador, ou ferramentas construdas separadamente, analisam o cdigo
dos programas e fornecem um resultado formalmente provado. Neste tipo de
verificao tambm se podem incluir tcnicas como o Design By Contract (DBC)no qual se definem contractos sobre aquilo que o programa recebe e produz. Este
tipo de verificao tem ainda a possibilidade de associar um selo de qualidade
(certificado) ao cdigo [21]. No entanto preciso ter em ateno que nem sempre as
tcnicas de DBC so implementadas estaticamente. possvel que as mesmas sejam
implementadas dinamicamente isto , em tempo de execuo, ou dinamicamente e
estaticamente.
Nesta dissertao feita a distino entre as ferramentas industriais e as ferra-
mentas acadmicas. Enquanto as ferramentas industriais, de verificao esttica,
providenciam algumas garantias, nomeadamente no suporte das mesmas, as fer-
ramentas acadmicas servem essencialmente para investigao. Este ltimo tipo
de ferramentas tambm peca por algumas vezes no ter a devida documentao e
muito raramente suporte.
2.2.1.1 Perfil Ravenscar
O estudo dos mecanismos de verificao comeou com o estudo de um perfil
de segurana. Em 1997 na 8th International Real-Time Ada Workshop (IRTAW)
ficou definido o perfil Ravenscar [11][12][34]. Este perfil destina-se aos sistemas
de tempo real crticos e consiste numa coleco de primitivas concorrentes e de
restries linguagem Ada, no entanto no se limita a esta. O Ravenscar permite
um desenvolvimento eficiente de aplicaes capazes de serem verificadas quer na
sua componente funcional como temporal.
Este perfil promove o suporte da concorrncia ao nvel da linguagem, permitindo
verificao esttica quer pelo compilador como por outras ferramentas. O perfil
introduz um conjunto de restries com objectivo de aumentar a eficincia e pre-
visibilidade dos programas. Para isso probe a utilizao de funcionalidades com
um overhead elevado. Reduz a utilizao de mecanismos da linguagem Ada que
levam a situaes no deterministas. Remove a utilizao de funcionalidades de
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
29/133
2.2. MECANISMOS DE VERIFICAO 15
fraco suporte na verificao formal bem como funcionalidades que inibem anlises
temporais efectivas.
Em termos concretos o perfil Ravenscar permite que a declarao de tarefas
e objectos protegidos seja apenas feita ao nvel da biblioteca. No permite a
alocao dinmica quer de tarefas como de objectos protegidos. S permite objectos
protegidoscomuma ou nenhuma entrada. Todas as tarefas soassumidas como no
terminais. No permite o uso de instrues abort ou ATC (Asynchronous Transfer
of Control). Na construo das tarefas peridicas no pode ser utilizada a instruo
delay, s sendo permitido o delay until. No permitida a utilizao de estruturas
de controle Select. No permitido o uso de prioridades dinmicas. O pacote
calendrio no pode ser utilizado, sendo apenas permitido a utilizao do pacote
Real-Time, entre outras restries.
2.2.1.2 SPARK (industrial)
O SPARK [3][14][13] uma linguagem de programao desenvolvida pela Praxis
combase no Ada. Desde sempre que esta linguagem segue uma abordagem correcta
por construo (Correctness by Construction) recorrendo a anotaes. Estas anotaespermitem uma extensa anlise esttica incluindo anlises de fluxo de controlo, de
dados e informao.
Em 2003 o SPARK adoptou o perfil Ravenscar para permitir o desenvolvimento
de aplicaes concorrentes e fiveis. No entanto num modelo de desenvolvimento
tradicional o Spark no substitui nem dispensa o processo de modelao [10].
As ferramentas envolvidas na verificao do SPARK so o SPARK Examiner, oSPADEProof Checker e o Automatic Simplifier. Na prticao processo de verificao
iniciado com o Examiner. Quando o Examiner enceta a sua execuo feita uma
anlise lexical e sintctica de cada unidade de compilao. No segundo passo
feita uma anlise semntica de cada unidade de compilao. No terceiro passo
feita uma anlise de fluxo de controlo que verifica se o cdigo est bem estruturado.
No quarto passo feita a anlise de fluxo de dados e informao para controlar a
estabilidade dos ciclos, a existncia de variveis declaradas mas no utilizadas, a
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
30/133
16 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
existncia de instrues sem efeito, a utilizao de variveis no inicializadas e a
consistncia entre o fluxo de informao esperado e o actual.
No quinto passo feita a deteco dos erros que podem ocorrer em tempo de
execuo (diviso por zero, ndice fora do tamanho, etc.) e so geradas obrigaes
de prova sobre esses possveis erros. No sexto passo pretende-se provar que
as obrigaes de prova, anteriormente geradas, nunca vo ocorrer. Neste passo
algumas das obrigaes de prova so descartadas com uma ferramenta automtica,
o Simplifier, no entanto as restantes devero ser provadas manualmente recorrendo
ao SPADE Proof Checker.
No stimo e ltimo passo feita uma anlise do pior caso de execuo(WCET)
bem como das necessidades de memria do programa. Isto feito combinando o
grfo de control de fluxo para cada subprograma e o WCET de cada objecto. O
resultado imediato desta combinao permite a obteno da execuo que origina
o WCET do programa.
De seguida so apresentadas algumas das anotaes em forma de exemplo.
- global Torna visvel uma varivel global com o modo especificado.1 procedure Control;
2 # g l o b a l i n S e n so r . S t a t e ;
3 # o u t V a l v e . S t a t e ;
- derives Especifica o fluxo de informaoentre os parmetros e variveis globais
de um procedimento.1 procedure Flt_Integrate(Fault : in Boolean;
2 T r ip : i n o u t Boolean;
3 C o u n te r : i n o u t Integer)4 # d e r i v e s T r ip f ro m , F a u lt , C o un t er &
5 # C o u n t e r f r o m , F a u l t ;
- pre Especifica um requisito essencial para o correcto funcionamento do pro-
grama.
- post Especifica o resultado garantido aps uma correcta execuo.
- assert Utilizado para especificar condies que devem ser sempre verdadeiras.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
31/133
2.2. MECANISMOS DE VERIFICAO 17
1 procedure D i v ( M , N : in I n te g er ; Q , R : out Integer)
2 # d e r i v e s Q , R f r o m M, N ;
3 # p r e (M >= 0 ) a n d ( N > 0 ) ;
4 # p o s t (M = Q N + R ) a n d ( R < N ) a n d ( R >= 0 ) ;
5 is
6 begin
7 Q : = 0 ; R : = M ;
8 loop9 # a s s e r t (M = Q N + R ) a n d ( R >= 0 ) ;
2.2.1.3 Giotto (acadmico)
O Giotto [23][26][24][28] uma linguagem de programao para sistemas em-
bebidos com tarefas peridicas. A principal caracterstica do Giotto reside na
abstraco que feita ao nvel da arquitectura. A componente lgica (funcional
e temporal) divide-se da componente fsica na qual o cdigo vai ser executado. Esta
particularidade torna os programas completamente independentes da plataforma,
necessitando apenas da existncia de uma implementao do ambiente de execuo
para o sistema de destino.
Num programa Giotto as tarefas representam a funcionalidade de base da lin-
guagem. Elas so executadasem intervalos de tempos regulares (tarefas peridicas).
Estas tarefas so associadas a funes e possuem um nmero arbitrrio de portosde entrada e sada. A funo que dita a funcionalidade da tarefa, no entanto ela
implementada forado Giotto recorrendo(teoricamente) a uma qualquer linguagem.
Apesar da abstraco feita, para a implementao de um programa Giotto numa
dada mquina o compilador necessita conhecer o WCET de todas as funes.
Num programa Giotto as tarefas agrupam-se em modos que so executados
ciclicamente. De notar que, um programa s pode estar num modo de cada vez
mas os modos podem conter instrues para troca de modo.
Os portos utilizados nas tarefas representam variveis tipadas num espao par-
tilhado. Esse espao pode ser de memria partilhada ou de outro tipo. Cada
porto persistente no sentido que mantm o seu valor ao longo do tempo at ser
actualizado. Por sua vez os drivers so os elementos que permitem a comunicao
entre os portos das tarefas.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
32/133
18 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
Outra caracterstica fundamental no Giotto so as anotaes. Enquanto o cdigo
puro do Giotto independente da plataforma, o mesmo pode ser refinado com
directivas de compilao na forma de anotaes dependentes da plataforma. Essas
directivas podem mapear uma determinada tarefa para uma unidade de processa-mento, escalonar uma tarefa num intervalo de tempo ou ainda escalonar um evento
de comunicao entre tarefas num intervalo de tempo. Todavia estas anotaes
no influenciam as funcionalidades do programa, apenas introduzem indicaes ao
compilador para implementao numa dada plataforma.
Existem trs nveis de anotaes no Giotto, o primeiro designado por Giotto-H
(H de Hardware). Neste especificado o conjunto de unidades de processamento
disponveis, as redes e informaes sobre os WCET de cada tarefa bem como outras
informaes sobre os tempos de comunicao. O segundo nvel designado por
Giotto-HM(M de Map) e neste acrescentada informao sobreo mapeamento entre
as tarefas e as unidades de processamento. O terceiro e ltimo nvel designado
por Giotto-HMS (S de Scheduling) e especifica informaes sobre o escalonamento
de cada unidade de processamento.
Estas anotaes servem de directivas que indicam como os programas Giottose devem comportar numa dada plataforma. Apesar de a linguagem possuir
boas propriedades no existe nenhuma garantia de escalonamento dos programas.
No entanto a dada altura foi apresentado um mtodo que permite verificao
de programas Giotto. Esse mtodo consiste num esquema de traduo manual
da linguagem para um modelo de redes de autmatos temporizados [37] (mais
precisamente para a ferramenta de verificao de modelos UPPAAL). Este esquema
de traduo divide-se em duas partes. Numa primeira considerado apenas o
cdigo puro do Giotto (sem as anotaes) e numa segunda parte so consideradasasanotaes. Estaverificaopermitenaprimeirapartedeterminarseumprograma
Giotto cumpre ou no com determinados requisitos temporais e na segunda se ou
no escalonvel.
Infelizmente poucos resultados so apresentados e o esquema de traduo nunca
chegou a ser automatizado. Apesar de tudo, a dissertao inspira-se nesta ideia de
construo de um modelo a partir de uma dada linguagem.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
33/133
2.2. MECANISMOS DE VERIFICAO 19
2.2.1.4 Schedule Carrying Code (acadmico)
Em termos prticos, do processo de compilao do Giotto obtm-se o designado
Embedded Code (E-Code). Este executado numa mquina virtual, a EmbeddedMachine (E-Machine). O E-Code considerado time-safe se for encontrado um
escalonamento possvel para a plataforma na qual se quer implementar a aplicao.
Deste facto surge o Schedule Carrying Code (SCC) [27][15][25] que introduz um
novo conceito linguagem Giotto. Mais precisamente o Scheduling Code (S-Code),
i.e. uma linguagem mquina executvel que permite especificar o escalonamento
(despacho). Ao contrrio do que acontece no Giotto original, neste modeloo E-Code
independente da plataforma e este novo S-Code dependente da plataforma.
O S-Code s gerado se for encontrado um escalonamento que considere a
execuo do programa como time-safe. Este cdigo pode ser visto como uma
prova de escalonamento para uma determinada plataforma semelhana do Proof
Carrying Code (PCC). O S-Code consiste ento num conjunto de instrues que
determinam qual a tarefa a ser executada at que um determinado evento ocorra.
Esse evento pode estar relacionado com o relgio, com uma tarefa ou at mesmo
com um sensor. Outra particularidade interessante que o S-Code pode ser gerado
consoante qualquer estratgia de escalonamento, seja em tempo de compilao,
execuo ou parcialmente em compilao e parcialmente em execuo.
2.2.1.5 xGiotto (acadmico)
Na continuao do processo de melhoramento do Giotto surgiu o eXtended Giotto
(xGiotto) [19][39], como uma extenso da linguagem anterior. Esta nova linguagemliberta-se da dependncia das tarefas peridicas e passa a ser auto-contida inte-
grando o cdigo funcional das tarefas.
O xGiotto realiza adicionalmente vrias anlises de integridade. A primeira visa
rejeitar programas que contenham possveis race conditions, i.e. quando duas tarefas
escrevem no mesmo porto e so terminadas pelo mesmo evento. Isto permite
que os programas continuem deterministas. Numa segunda anlise feita uma
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
34/133
20 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
previso sobre a capacidade de memria necessria. Na terceira anlise verificado
o escalonamento do programa para uma determinada plataforma. Esta ltima
anlise requer que os WCET das tarefas esteja especificado segundo a plataforma
de destino.
No entanto, tal como referido em [20], esta linguagem rapidamente torna
o processo de determinao do escalonamento intratvel. Esta situao torna a
linguagem muito menos atractiva apesar de no se limitar a tarefas peridicas.
2.2.1.6 TDL e HTL
O Giotto ainda deu origem a outras linguagens como o Timing Definition Language
(TDL) [35][43] e o HTL [20][29][17][18]. O TDL foi desenvolvido no projecto
MoDECS e disponibiliza uma sintaxe mais conveniente bem como um conjunto
de ferramentas adicionais. Este representa o primeiro passo para tentar tornar
estas linguagens, derivadas do Giotto, menos acadmicas e mais industriais (http:
//www.preetec.com).
O TDL ainda acrescenta um novo conceito relativamente ao Giotto. Trata-se da arquitectura baseada em componentes (mdulos). Isto proporciona uma
maior flexibilidade na construo de programas uma vez que estes mdulos so
independentes uns dos outros.
Por sua vez, o HTL o resultado mais recente do Giotto. Esta nova linguagem
reconhecida como uma linguagem de coordenao. Ao contrrio do TDL e do
xGiotto, o HTL no auto-contido uma vez que tal, como o Giotto, no inclui na
sua especificao a componente funcional das tarefas.
Esta linguagem possui no entanto caractersticas bastante interessante como a
noo de precedncia de tarefas, refinamentos hierrquicos, mdulos, etc.. Como
vantagem sobre o xGiotto, o HTL consegue simplificar o processo de prova de
time-safety, muito devido sua estrutura hierrquica. Num programa HTL basta
garantir que o modelo time-safe ao nvel mais alto da hierarquia. A linguagem
descrita com maiores detalhes no captulo 4.
http://www.preetec.com/http://www.preetec.com/http://www.preetec.com/http://www.preetec.com/ -
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
35/133
2.2. MECANISMOS DE VERIFICAO 21
2.2.2 Verificao de Modelos
Num processo de desenvolvimento com uso de mtodos formais comum serem
utilizados mais do que um tipo de mecanismos de verificao. Mecanismos dis-tintos tendem a complementar-se mas as ferramentas que empregam mecanismos
idnticos tambm podem verificar propriedades distintas se usarem lgicas/algo-
ritmos distintos. Sucintamente a verificao de modelos (Model Checking) [4][7]
consiste numa formulao matemtica representativa do sistema (o modelo), num
formalismo de especificao de propriedades e num conjunto de algoritmoscapazes
de explorar sistematicamente todos os estados do modelo. Os algoritmos so a
parte nuclear da verificao, so estes os responsveis por indicar se uma dada pro-
priedade verificada ou no. Se a propriedade no for verificada, tradicionalmente,a ferramenta produz um contra-exemplo, i.e. um exemplo de execuo no qual
possvel verificar a falha dessa propriedade.
Emtodasaslinguagensanteriormentereferidasmuitodoquefeitoemtermosde
verificao temporal consiste numa anlise de escalonamento (Scheduling Analysis).
Mas pouco ou nada feito em termos de anlise temporal (Timing Analysis). Poucas
so as situaes em que possvel estabelecer comparaes sobre os perodos
ou relaes temporais entre a execuo de tarefas. Na verificao esttica, vista
anteriormente, o importante determinar se o programa ou no escalonvel. Nada
referido sobre a possibilidade das tarefas no serem executadas pela sequncia
correcta. Desde que elas sejam escalonveis tudo est bem do ponto de vista da
anlise de escalonamento.
Apesar de no ser assim to recorrente, possvel encontrar estudos sobre a
utilizao da verificao de modelos juntamente com as ferramentas anteriormente
referidas [37][10][34]. Um dos grandes problemas da utilizao da verificao de
modelos reside no facto de ser necessrio traduzir o modelo pelo cdigo ou o cdigo
pelo modelo. Este processo penoso, repetitivo e pode adulterar a verificao se
no for garantido que o modelo corresponde precisamente ao sistema.
Any verification using model-based techniques is only as good as the
model of the system. Em [4]
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
36/133
22 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
Um modo de tornar a utilizao deste mecanismo de verificao mais apelativo
consiste em automatizar o processo de traduo do modelo para a linguagem na
qual o sistema implementado, ou em automatizar a traduo da linguagem para
o modelo. Uma vez que o modelo tendencialmente mais abstracto do que alinguagem, este processo de traduo dificilmente se automatiza na totalidade,
no entanto o contrrio j pode ser feito de forma mais eficiente. Da linguagem
facilmente se consegue abstrair a informao desejada para a construo de um
modelo e consequentemente torna-se possvel proceder verificao do mesmo.
Nos sistemas de tempo real, a verificao de modelos baseia-se bastante nas
lgicas temporais. De notar que estas lgicas dividem-se em diversas famlias com
expressividades distintas e como tal nem todas as ferramentas de verificao de
modelos utilizam a mesma lgica temporal.
Genericamente as lgicas temporais permitem verificar as seguintes classes de
propriedades:
- Segurana (Safety) - Em certas condies, um determinado acontecimento no
vai ocorrer.
- Acessibilidade (Reachability) - Uma situao particular pode ser atingida.
- Equidade (Fairness) - Em certas condies, um determinado evento vai ocorrer
(ou no vai ocorrer) uma infinidade de vezes.
- Vivacidade (Liveness) - Em certas condies, um determinado evento vai
acabar por acontecer.
- Ausncia de DeadLock- O sistema no pode chegar a uma situao a partir da
qual nenhum progresso possvel.
A compreenso deste tipo de classes de propriedades determinante para uma
correcta metodologia de modelao e especificao das propriedades do sistema. Se
o tipo de propriedades que se querem verificar no corresponde a estas classes, ento
a verificao de modelos temporizados no adequada. De notar ainda que neste
tipo de verificao de modelos, as propriedades de acessibilidade e de segurana
so em geral mais importantes porque so mais fceis de verificar. Deste modo
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
37/133
2.3. CONCLUSO 23
conveniente definir boas estratgias de modelao (incluindo transformaes no
modelo, se necessrio) para que as propriedades visadas possam ser verificadas.
No estudo feito, s ferramentas de verificao de modelos [22][7][4][31], sumari-
amente destacam-se as seguintes:
- RT-Spin - Extenso da linguagem promela com noes temporais e Lgica LTL
com asseres. Adequado para sistemas concorrentes interactivos.
- Kronos e UPPAAL - Autmatos temporizados (Lgica TCTL). Adequados
para sistemas de tempo real.
- SMV - Autmatos temporizados (Lgica CTL). Adequado para sistemas con-correntes.
- HyTech - Autmatos Hbridos Lineares. Adequado para sistemas embebidos
crticos.
2.3 Concluso
Neste captulo apresentaram-se os mecanismos de verificao estudados no mbitoda dissertao. Apesar de no terem sido estudadas todas as ferramentas, o estudo
foi suficiente para ficar com uma percepo geral do tipo de verificao desejvel
nos sistemas de tempo real. Um dos aspectos que tem dominado a investigao na
matria concentra-se muito na questo do escalonamento das tarefas. No entanto
muito ainda pode e deve ser feito relativamente ao cumprimento total dosrequisitos
temporais e funcionais.
Os mecanismos actuais no se focam o suficiente sobre questes como: A tarefaX nunca pode ocorrer simultaneamente que a tarefa Y, ou Se a tarefa X ocorrer,
passado T unidades de tempo a tarefa Y tem de ocorrer, ou A tarefa X alguma
vez vai ser atingida. Este aspecto faz com que um sistema at possa ser escalonado
mas funcionalmente o resultado no o desejado. Se apenas forem verificadas
propriedadesdestetipotambmsepodeperderaverificaosobreoescalonamento,
pelo que o ideal combinar ambas.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
38/133
24 CAPTULO 2. VERIFICAO DE SISTEMAS DE TEMPO REAL
De modo a tirar benefcio das duas situaes, esta dissertao apresenta uma
soluo onde ambas so conjugadas. Para isso foi necessrio escolher uma lin-
guagem que permitisse alguma verificao esttica. Infelizmente cada uma destas
linguagens possui as suas prprias restries. O SPARK e as linguagens querespeitam o perfil Ravenscar so mais completos em termos de verificao, mas
inibemautilizaodediversastcnicasdeprogramao. Desconhece-seaexistncia
deumaprovaqueindiquequeestaslinguagensnopermitamfazertudooquesefaz
comassuasversesnolimitadas. Todaviareconhece-sequeasrestriesdificultam
significativamente o processo de desenvolvimento. Para alm disto, o facto do
HTL funcionar como linguagem de coordenao, possuir hierarquias, permitir
precedncia de tarefas e garantir o escalonamento despertou interesse suficiente
para descartar linguagens baseadas no perfil Ravenscar. Tanto que num futuro,
mais ou menos distante, aceitvel considerar que o HTL permita a especificao
funcional em ADA ou numa linguagem DBC.
Estando a linguagem nuclear identificada, restava escolher a ferramenta de
verificao de modelos. Sendo o objectivo da soluo apresentada no captulo 5
complementar a verificao dos requisitos temporais, a escolha preferencialmente
recaia numa ferramenta baseada na Lgica TCTL. Das ferramentas identificadas
verificou-se que aquelas que empregam este tipo de lgica adaptam-se melhor aos
sistemas de tempo real. Entre o Kronos e o Uppaal a escolha facilmente tendeu para
o Uppaal, quer pela quantidade de informao existente sobre a ferramenta como
pelas qualidades reportadas na literatura.
Nosdoisprximoscaptulossoapresentadosalgunsconceitosrelacionadoscom
a ferramenta Uppaal, bem como a linguagem HTL. Nos captulos seguintes a estes,
apresentado o tradutor de HTL para Uppaal e os resultados obtidos na aplicaodo tradutor ao caso de estudo Tree Tank System (3TS).
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
39/133
Captulo 3
UPPAAL
Estecaptulobaseia-senoslivros[ 4][31][7]enosdocumentos[6][5][2][1][30]. Introduz-
se neste captulo alguns conceitos sobre a ferramenta de verificao de modelos
Uppaal. No mbito da dissertao foi produzido um documento descritivo da
componente prtica da ferramenta que pode ser consultado no URL http://floyd.
di.ubi.pt/release/jcarvalho/TutorialPT_Uppaal.pdf. Esse documento com-
plementa, de alguma forma, a informao exposta na dissertao.
Apesar da verificao de modelos ser vista, nesta dissertao, mais na vertentedos autmatos temporizados e da lgica temporal, no se pode ignorar a existncia
de outrasrepresentaes. Nomeadamente no querespeita aos modelosoperacionais
possvel identificar diversos sistemas de transio como, os autmatos de estados
finitos, os autmatos de Bchi, as estruturas de Kripke, etc. No que respeita s
lgicas subjacentes tem-se, as lgicas modais, temporais, dinmicas, etc..
O processo de verificao assume a existncia de, pelo menos, um sistema de
transioque especifica o sistema, uma lgica particular e uma frmulasdesta lgicaque estabelecem o que se pretende verificar. Este processo efectua constataes
baseadas em percursos adequados do sistema de transio (verificao de modelos
directa) ou de uma representao compacta (verificao de modelos simblica).
Sumariamente, a verificao de modelos baseada em autmatos temporizados
(como no caso do Uppaal) recorre-se de uma verso refinada dos autmatos de
25
http://floyd.di.ubi.pt/release/jcarvalho/TutorialPT_Uppaal.pdfhttp://floyd.di.ubi.pt/release/jcarvalho/TutorialPT_Uppaal.pdfhttp://floyd.di.ubi.pt/release/jcarvalho/TutorialPT_Uppaal.pdfhttp://floyd.di.ubi.pt/release/jcarvalho/TutorialPT_Uppaal.pdf -
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
40/133
26 CAPTULO 3. UPPAAL
Bchi. Um autmato de Bchi consiste num autmato de estados finitos estendido
de forma a aceitar entradas infinitas. Este sustenta-se na noo de aceitao, i.e.
execuo potencialmente infinita que passa infinitamente pelo estado final. Os
autmatos temporizados so ento autmatos de Bchi com a noo de relgioslocais. Com este formalismo possvel discursar sobre a sequncia das operaes
durante as execues possveis (concorrncia e distribuio), mas tambm sobre
os prazos esperados para cada uma delas (tempo real). No caso do Uppaal este
discurso produzido por um subconjunto da linguagem Timed Computation Tree
Logic (TCTL).
3.1 Sistemas de AutmatosEm forma de reviso, assuma-se a existncia de um conjunto Prop = {P1, . . .} de
proposies elementares.
3.1.1 Autmato
Um autmato o 5 tuplo A = (Q, E, T, Q0, l) onde, Q um conjunto de estados,
E um conjunto de etiquetas (label) de transies, T Q E Q o conjunto dastransies e Q0 Q o conjunto de estados iniciais. Considera-se aqui (sem perda de
generalidade) somente o caso em que h um s estado inicial. q0 o estado inicial
do autmato; E l : Q PF(Prop) uma aplicao que associa a cada estado q de Q
o conjunto finito de propriedades que este verifica.
Apesar de ser pouco relevante para esta dissertao no se deve esquecer que,
caso se pretenda um autmato com output, considera-se uma sexta componente O
que uma aplicao que atribui a cada estado o output que este produz (fala-seneste caso de autmatos de Moore).
3.1.2 Caminho
Considerando a existncia de um autmato A, chama-se caminho de A a uma
sequncia (possivelmente infinita) de transies (q, e, r) encadeadas (i.e. para
toda a transio (q, e, r) da sequncia, a transio seguinte da forma (r, e, s)).
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
41/133
3.1. SISTEMAS DE AUTMATOS 27
Ao comprimento de um caminho nota-se || (nmero de transies do caminho).
|| N {} (o caminho pode ser infinito). Para um caminho , um ndice i < ||,
(i) refere-se ao estado q da i-sima transio (q, e, r) de .
3.1.3 Execuo
Chama-se execuo parcial de A ao caminho comeado pelo estado inicial q0. Chama-
se execuo completa ao caminho parcial mximo (aquele que no pode ser mais
estendido). Chama-se execuo com bloqueio quandoocaminhoconsideradoinfinito
ou quando o caminho acaba num estado a partir do qual no h transies possveis.
A rvore de execuo a representao arborescente de todas as execues possveis
a partir dum determinado estado (em geral q0). Um estado designado de acessvel
(ou atingvel) se aparece na rvore de execuo com raiz q0. Ou seja, se existir pelo
menos uma execuo que passe por ele.
3.1.4 Extenses de Autmatos
Para alm destas caractersticas possvel realizar algumas extenses aos autmatosde base. Por exemplo, pode-se juntar variveis de estado na modelao por
autmatos. Nestasituaoastransiessoestendidascomacapacidadedetestaras
variveis (guardas) e, caso o teste permita a seleco da transio, de alterar o valor
das variveis. O autmato com essa funcionalidade passa a considerar um conjunto
de variveis (tipificadas) e uma transio passa a ser um 5-tuplo (q,g, l, a, r) onde: q
o estado de partida; r o estado de chegada; g uma guarda sobre uma varivel
do autmato; l uma etiqueta; e o conjunto a = {x1 := e1 . . .} das actualizaes de
variveis (atribuies) que so realizadas.
Uma transio (q,g, l, a, r) pode ser seleccionada quando o estado q o estado
de controlo, a guarda g verificada e a entrada do autmato comea pela etiqueta
l da transio. Como consequencia da seleco desta transio a actualizao a
accionada e o estado de controlo passa do estado q para o estado r.
Apesar destes autmatos estendidos serem teis a verificao de modelos no se
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
42/133
28 CAPTULO 3. UPPAAL
faz ao nvel da extenso. Para que se aplique algum algoritmo de verificao torna-
se necessrio passar da extenso para uma representao clssica. Este processo
de traduo resulta no autmato desdobrado, ou no sistema de transio associado.
possvel, sob certas condies, do autmato A (com variveis) obter o autmatofinito equivalente sem variveis. Essas condies so: O conjunto dos valores
possveis para as variveis ser finito; Se o conjunto dos valores possveis para
as variveis for infinito ento deve-se descobrir uma partio finita pertinente
(pares/impares, positivo/negativo...); etc.
3.1.5 Redes de Autmatos /Produto Sincronizado
Considerando uma famlia de n autmatos Ai = (Qi, Ei, q0,i, li) (com i = 1, . . . , n).
Considerando a etiqueta _ que corresponde aco nada por fazer.
Define-seporconjuntode sincronizaessync,umconjuntotalque sync 1i
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
43/133
3.2. AUTMATOS TEMPORIZADOS 29
no desejados. Como por exemplo um evento de alarme ser accionado.
3.1.7 SincronizaesAs sincronizaes podem ser feitas de dois modos distintos, por mensagens ou
por variveis partilhadas. No primeiro caso uma sincronizao corresponde vir-
tualmente ao envio e recepo de mensagens aquando de uma transio. A
sincronizao s contempla transies onde qualquer emisso de mensagem (eti-
queta semelhante a !mensagem) acompanhada pela recepo da prpria (etiqueta
semelhante a ?mensagem). Embora seja possvel evitar o uso das variveis, pode
ser prtico beneficiar do seu uso explcito. No caso das sincronizaes feitas por
variveis estas podem ser utilizadas sobre a forma de flags ou acompanhadas por
sincronizaes de mensagens. No primeiro caso elas apenas funcionam como
ponto de encontro, no segundo caso o ponto de encontro feito pela sincronizao
de mensagem e a varivel partilhada serve de portadora da mensagem (com um
contedo especfico).
3.2 Autmatos Temporizados
Os autmatos clssicos permitem raciocinar sobre a ordem no tempo dos eventos
que nele ocorrem. Mas no permitem raciocinar sobre a durao dos eventos ou
sobre os intervalos de tempo que ocorrem entre eventos. Para tal, Rajeev Alur e
David L. Dill definiram em 1994 uma extenso dos autmatos que cobre os aspectos
quantitativos do tempo. Esta extenso ficou conhecida por autmato temporizado.
Um autmato temporizado composto por um autmato finito clssico e var-
iveis de relgio que permitem quantificar a progresso do tempo. As transiesdeste tipo de autmatos so consideradas instantneas, sendo que o tempo evolui
nos estados. Para se poder discursar sobre a durao de um evento necessrio
considerar um estado que modela o incio do evento e outro o fim. Existindo uma
sequncia de vrios estados, pode no ser necessrio que cada um deles apenas
represente o fim ou o inicio de um evento. Se for considerado que no existe
passagem de tempo entre eventos, define-se um determinado estado como sendo
o fim do evento anterior e simultaneamente o incio do evento actual. Se existir a
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
44/133
30 CAPTULO 3. UPPAAL
necessidade de efectuar alguma transio entre o fim de um evento e o inicio de
outro, ento este tipo de simplificao do modelo no possvel.
3.2.1 Relgios e Transies
Os relgios so variveis reais deR+ com valor inicial 0. Nos autmatos temporiza-
dos todos eles evoluem mesma velocidade. J nos autmatos hbridos o mesmo
no acontece, i.e. neste tipo de autmatos permitido que os relgios evoluam
a ritmos diferentes. As transies dos autmatos temporizados so constitudas
por uma guarda, uma etiqueta ou aco e aces de reinicializao de variveis de
relgio.
Devido s reinicializaes possveis, os relgios medem prazos e no o tempo. O
sistema modelado por este tipo de autmatos funciona considerando a existncia
de um relgio global que permite a sincronizao com todos os relgios utilizados.
3.2.2 Configurao e Execuo
Seja uma aplicao que associa a cada relgio o seu valor (designada valorao)e q o estado de controlo activo. Designa-se por configurao (q, ) ao par do
estado de controlo activo e do valor de cada relgio nesse instante. Ao efectuar-se
uma alterao de configurao tem-se um passo da execuo do autmato (uma
transio).
Para que o sistema mude de configurao preciso que decorra um prazo d R+,
designada transio de prazo na qual todos os relgios so actualizados de acordo
com o prazo d. Ou que o autmato seja activado, i.e seja executada uma transiodo autmato, designada transio discreta ou transio de aco, na qual os relgios
por reinicializar so reinicializados e o valor dos restantes mantido.
A execuo de um autmato temporizado tambm pode ser designada por
trajectria. Esta, pode ser vista como uma aplicao dos reais positivos para as
configuraes. (0) representa a configurao no instante global 0 e (t) representa
a configurao no instante global t. Exemplo: (init, 0) (init, 8.8)?req (process, 0)
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
45/133
3.2. AUTMATOS TEMPORIZADOS 31
(process, 9.4)?req (process, 0) (process, 3.4)
?req (alarm, 0), (9.9) = (process, 1.1).
Pode-se dizer que as execues baseiam-se numa perspectiva em que o tempo
global e externo ao sistema enquanto as valoraes numa perspectiva local e
interna.
3.2.3 Redes e Sincronizaes
Uma Rede de Autmatos Temporizados (RAT) representa o modelo completo do
sistema. Como tal, trata-se de uma composio adequada de diversos autmatostemporizados (com as devidas sincronizaes). execuo da RAT corresponde
uma sequncia, geralmente infinita, de configuraes. Numa RAT a configurao
(q, ) representa o registo do estado de controlo de cada um dos autmatos (vector
de estados q) bem como dos valores de cada um dos relgios ().
As execues da RAT decorrem como as execues de um autmato nico,
com a considerao de que ao ser activada uma aco aplicvel (uma transio
ou vrias transies sincronizadas) apenas o controlo dos estados ligados a essaaco so alterados. Assim todos os autmatos so executados em paralelo e
mesma velocidade.
3.2.4 Invariantes
Os estados podem conter condies (sobre os relgios) designadas por invariantes.
O invariante acrescenta a noo de obrigao de progresso, ao contrrio das guardasnas transies que so uma possibilidade de progresso. Um invariante I num
estado q significa que o controlo s pode estar em q enquanto I for verificado. Na
existncia de invariantes, uma configurao vlidase os invariantes dosestados de
controlo so todos verificados. Assim o tempo s pode decorrer numa determinada
configurao enquanto esta permanecer vlida. Quando esta deixa de o ser, uma
transio elegvel deve ser accionada para evitar o designado livelock (deadlock
temporizado), situao em que nenhuma configurao vlida atingvel.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
46/133
32 CAPTULO 3. UPPAAL
3.2.5 Estados e Sincronizaes Urgentes
Nalgumas situaes pode ser desejvel que certas aces sejam tomadas sem que
o tempo decorra (i.e. de forma urgente). Numa sincronizao urgente no existepassagem de tempo, isto implica que a transio respectiva no contemple guardas
sobre os relgios. Num estado urgente no existe passagem de tempo enquanto
esse estado for de controlo. No Uppaal ainda existe a noo de estado committed,
i.e. estado que urgente e para alm disso obriga imediatamente a execuo de
uma transio que parte dele. Este tipo de estados permite modelar sequncias de
aces atmicas.
3.2.6 Autmato de teste
Dada uma propriedade por verificar sobre uma RAT D, por vezes conveniente
transformar a verificao de num problema de acessibilidade. Isto pode ser feito
recorrendo ao autmato de teste, i.e. ao autmato T cujo objectivo atingir um
estado q, interagindo com D, caso a propriedade seja violada. Afirmar que D
respeita significa verificar que q no acessvel [8]. Mas tambm pode ser feito
acrescentando ao modelo, relgios, variveis, guardas, etc., para que a propriedade
possa ser simplificada [33].
3.3 Lgica Temporal
Nas duas seces anteriores foram vistos fundamentos da teoria dos autmatos
clssicos e dos autmatos temporizados. Seja, fundamentos sobre a modelao do
sistema ao qual se pretende aplicar a verificao de modelos. Falta agora abordar
os fundamentos relacionados com a especificao das propriedades a verificar. Talcomo referido anteriormente, essa especificao feita por intermdio de uma
lgica, no caso do Uppaal da TCTL. A TCTL, por sua vez, uma extenso da
Computation Tree Logic (CTL) e esta um subconjunto da Full Computation Tree
Logic (CTL*).
Muito genericamente, a lgica temporal um formalismo de especificao ad-
equado a sistemas que lidam com propriedades nas quais existe uma relao
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
47/133
3.3. LGICA TEMPORAL 33
temporal, mais precisamente noes de ordenao no tempo. Este tipo de lgica
baseia-se em noes matemticas prximas das construes lingusticas: "sempre",
"enquanto", "nunca", "antes", "depois", etc.
Todavia, a lgica temporal no especifica propriedades sobre o tempo de forma
explcita, mas sim tendo em considerao sequncias de aces (vistas como es-
tados), i.e. os possveis caminhos. As propriedades onde o tempo absoluto
(unidades de tempo) no so, por defeito, apropriadas especificao em lgica
temporal. O que acontece na prtica que existem mtodos capazes de contornar
esta situao, recorrendo por exemplo utilizao das variveis de relgio.
Tal como j tinha sido sugerido, as lgicas temporais diferenciam-se pela forma
como representam o tempo. No modelo de tempo linear, Linear Temporal Logic
(LTL), o comportamento do sistema representado por um conjunto de execues
infinitas. Cada uma das execues independente, sem a existncia de ramificaes
entre elas. No modelo de tempo ramificado, CTL, o comportamento do sistema
representado por uma rvore de computao de profundidade. Devido a estas
especificidades cada modelo possui capacidades de expressividade diferentes.
3.3.1 Full Computation Tree Logic
3.3.1.1 Sintaxe (formato BNF)
, ::= P1 | P2 | (proposies atmicas)
| ( ) | ( ) | ( = ) | (conectivas lgicas clssicas)
X | F | G | ( U) | (conectivas temporais de estado)
E |A (conectivas temporais de caminho)
3.3.1.2 LTL vs CTL
Considerando o conjunto das execues de um autmato. Este pode-se representar
como um conjunto de sequncias (LTL) ou como uma rvore (CTL). Por sua vez a
CTL* rene o poder expressivo da LTL e da CTL.
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
48/133
34 CAPTULO 3. UPPAAL
O tempo do ponto de vista linear apenas permite a utilizao de conectivas de
estado, tais como: X: Na execuo considerada, o estado imediatamente a seguir
(neXt) verifica ; F : Na execuo considerada, um estado qualquer a seguir
(Finally) verifica ; G : Na execuo considerada, todos os estados seguintes(Globally) verificam ; U: Na execuo considerada, at (Until) se chegar a um
estado em que se verifica, verifica-se .
O tempo visto como uma rvore permite tambm a utilizao de conectivas de
caminho, tais como: A : qualquer execuo (All) que parte do estado corrente
satisfaz a frmula ; E : existe (Exist) uma execuo que parte do estado corrente
e que satisfaz a frmula .
Nesta abordagem possvel realizar combinaes entre estes dois tipos de conec-
tivas, no entanto com algumas limitaes. Nomeadamente, as conectivas X, F e U
devem estar sempre no mbito (scope) imediato de uma conectiva de caminho: EX,
AX, EF,AF, E_U_,A_U_. Avalidadedafrmulaaverificardependeexclusivamente
do estado actual (e da explorao de todos os caminhos que saem dele).
3.3.1.3 Estruturas de Kripke
Uma estrutura de Kripke um tuplo (S, i, R, L) onde S um conjunto finito de
estados. i S o estado inicial. R S S uma relao de transio. No caso
presente procura-se relaes totais (que verificam, s S, s S, (s, s) R) para
garantir a ausncia de deadlock. L : S P(P) uma funo que etiqueta cada
estado com o conjunto de frmulas atmicas vlidas nesse estado.
Estas estruturas so na realidade um modelo da CTL* e definem formalmenteo que se entende por ser verdade em CTL*. So estas estruturas que permitem
estabelecer a relao entre a lgica e os autmatos, uma vez que elas so um mero
caso particular de autmato onde as etiquetas so ignoradas. As consideraes
de semntica permitem estabelecer as regras para afirmar quando um autmato
respeita ou no uma frmula (propriedade) CTL*. A verificao de modelos ento
o processo algortmico que permite estabelecer esta afirmao (ou no).
-
8/4/2019 Verificao Automatizada de Sistemas de Tempo Real Crticos
49/133
3.4. TIMED COMPUTATION TREE LOGIC 35
Sendo A uma estrutura de Kripke (autmato), uma execuo, i N {}um momento na execuo e (i), o estado correspondente (o i-simo elemento daexecuo). Notao: A, , i |= , ou , i |= . No tempo i da execuo do autmatoA, vlida.
, i |= P sse P l((i))
, i |= sse , i |=
, i |= sse (, i |= ) (, i |= )
, i |= X sse i < || , i + 1 |=
, i |= F sse j i, j < || , j |=
, i |= G sse j i, j < || = , j |=
, i |= U sse j i, j < || , j |=
k, i k< j = , k |=
, i |= E sse , (0) . . . (i) = (0) . . . (i) , i |=
, i |= A sse , (0) . . . (i) = (0) . . . (i) , i |=
A |= sse para toda a execuo de A verifica-se , 0 |= .
3.4 Timed Computation Tree Logic
3.4.1 Sintaxe (formato BNF)
, ::= P1 | P2 | (proposies atmicas)
| ( ) | ( ) | ( = ) | (conectivas lgicas classicas)
EFk | EGk | E( Uk ) | (conectivas temporais)
AFk |AGk |A( Uk ) |
onde {, } e k Q.
A TCTL estendea CTL introduzindoastaisvariveisderelgiotambmpresentes
nos autmatos temporizados. Contudo, como o tempo contnuo a conectiva
X desaparece. Na TCTL qualquer frmula passa a assumir equivalncias como
AG = AG0, etc. Informalmente, uma configurao verifica, por exemplo, EU3
se existe uma trajectria iniciada nesta confi