Dördüncü Alt Probleme İlişkin Bulgular ve Yorumlar

A presente seção tem por objetivo apresentar o formalismo Event-B e contextualizar os mo- tivos pelos quais neste trabalho permanecemos com o uso do B clássico. Conforme apresentado neste capítulo, o método formal B é voltado à especificação, desenvolvimento e verificação de programas sequenciais como base em refinamentos. Observa-se que o método formal Event- B[Abr10] é mais recente e recebe influência de B. No entanto, essa nova abordagem não deve ser encarada como uma evolução do método formal B, como poderia-se supor, uma vez que o foco de Event-B é diferente do B clássico, a saber, a modelagem e a verificação de sistemas re-

ativosconcorrentes. Dessa forma, o comportamento de uma máquina Event-B, sua notação e as obrigações de prova para verificação de máquinas e refinamentos são voltadas à especificação dessa categoria de sistemas, diferenciando-se do B tradicional.

O modelo de um sistema em Event-B é composto por máquinas, contextos e refinamentos. Nos contextos declaram-se os componentes estáticos de uma máquina, formado por conjun- tos, constantes e as propriedades que esses elementos devem obedecer. A parte dinâmica é a máquina em si, cujos principais elementos são as variáveis de estado, o invariante e os eventos. Observa-se que os eventos, assim como as operações do modelo em B clássico, relacionam- se à mudança de estado da especificação. A aplicação de um evento é condicionada à satisfação da sua guarda, composta por uma conjunção de predicados. Um evento pode ser aplicado em um determinado estado, sempre que a sua guarda seja avaliada como verdadeira. No entanto, é importante enfatizar que a aplicação de um evento é atômica e, mesmo que em algum estado mais de um evento possa ser aplicado (suas guardas são simultaneamente satisfeitas), ainda assim apenas um deles, de forma não determinística, será aplicado.

MACHINE Transport SEES Transport_Context VARIABLES balance card_type INVARIANTS inv1 : balance∈ N inv2 : balance≥ 0

inv3 : card_type ∈ CARDS

inv4 : card_type = gratuitous ⇒ balance = 0

CONTEXT Transport_Context SETS CARDS CONSTANTS gratuitous student entire AXIOMS

axm1 : partition(CARDS, {gratuitous}, {student}, {entire})

END

Figura 3.4: Máquina Event-B Transport (esq.) e contexto Transport_Constants (dir.)

Como exemplo, o modelo Event-B da aplicação Java Card de bilhetagem eletrônica Trans- port do capítulo 2 é exibido nas figuras 3.4 e 3.5. A figura 3.4 apresenta a declaração das variáveis de estado e a especificação do invariante, no qual são inseridas as restrições de que o cartão não deve ter saldo negativo (inv2) e, caso o cartão seja de gratuidade, o saldo deve ser 0 (inv4). Pode-se observar que cada restrição é inserida em uma linha separada, precedida por uma marcação (inv1 .. inv4). Essas marcações são exigência da ferramenta Rodin [ABH+_10],

utilizada na construção deste exemplo, para que ela possa gerenciar cada elemento da especifi- cação, facilitando a localização de erros e a construção e exibição para o usuário de obrigações de prova.

Ainda na figura 3.4, tem-se o módulo de contexto Transport_Constants, que declara o con- junto CARDS, utilizado na máquina Transport. Os possíveis elementos do conjunto (especifi-

cado na cláusula AXIOMS) são as contantes gratuitous, entire e student, que correspondem aos tipos de cartão que podem ser emitidos.

EVENTS Initialisation

begin

act1 : balance:= 0

act2 : card_type := entire

end Event addCredit=b any cr where grd1 : cr∈ N grd2 : cr> 0 grd3 : card_type 6= gratuitous grd4 : balance+ cr ≥ 0 grd5 : balance+ cr ∈ N then

act1 : balance:= balance + cr

end END

Figura 3.5: Eventos da especificação Transport

Observa-se pela figura 3.5 que na máquina Transport são definidos dois eventos, a saber, o evento de inicialização e o evento addCredit que modela a adição de créditos em um cartão. Ressalta-se que o evento de inicialização ocorre antes da ativação de qualquer outro evento para estabelecer o estado inicial da máquina de forma consistente com o seu invariante.

Um evento pode ser especificado através de três formas [ABH+_{10], são elas:}

1. evt b= any t where P(t, v) then S(t, v) end 2. evt b= where P(v) then S(v) end

3. evt b= begin S(v) end

A primeira forma é a mais geral e define um evento que possui parâmetros de entrada (t), uma guarda que atua sobre os parâmetros e as variáveis de estado (P(t,v)) e uma ação (S(t,v)). A ação é o componente responsável pela mudança de estado do evento caso a sua guarda seja estabelecida. As outras formas especificam, respectivamente, um evento sem parâmetros e um evento apenas com ação. Neste último caso, considera-se que a guarda do evento é sempre verdadeira.

É importante observar que as ações em Event-B são restritas a um pequeno conjunto de ações simples para atualização das variáveis de estado (também presentes em B na forma de

substituições), conforme pode ser visto na figura 3.6. Essa característica, para o tipo de de- senvolvimento requerido pelas aplicações smart card caracterizaria uma certa dificuldade na especificação de um serviço. Por exemplo, caso necessitássemos especificar um serviço que pode tomar mais de uma ação a partir da avaliação de condições, o que é comum em qualquer aplicação, então teríamos que especificar cada ação em um evento distinto, com a sua condição de aplicação definida como guarda.

Atribuição simples (becomes equal to): x := E (x é substituído pela expressão E)

Escolha a partir de um conjunto (becomes in): x :∈ S (x recebe um elemento qualquer do conjunto S) Escolha a partir de um predicado (becomes such that): x :| P

(x recebe um valor qualquer que satisfaça ao predicado P)

Figura 3.6: Ações presentes em Event-B.

Ressalta-se que Event-B é mais flexível que B no que diz respeito a mecanismos permitidos para especificação e refinamento. Por exemplo, uma máquina pode ser decomposta em mais de uma máquina para gerenciar a complexidade da especificação. Um evento, por sua vez, pode ser refinado por mais de um evento. Finalmente, mais de um evento pode ser unido em um evento único. É também possível introduzir novos eventos em um refinamento. Nesse caso, o evento concreto implicitamente refina um evento abstrato contendo uma substituição skip em seu corpo e o especificador deve assegurar o novo evento não leve a máquina a um estado de deadlock.

Evidencia-se que na abordagem utilizada no método BSmart, as aplicações smart card são traduzidas após serem especificadas, refinadas e implementadas em B. A composição de máqui- nas e refinamentos em B, conforme demonstrado neste capítulo, é mais restritiva que Event-B. Por outro lado, B oferece um ambiente mais adequado para se introduzir um estilo de desenvol- vimento algorítmico, composto por diversas substituições, muitas delas possuindo uma relação estrita com construções encontradas em linguagens, tais como C e Java. Além disso, ressalta- se que o refinamento de implementação não está presente em Event-B. Como consequência, as substituições determinísticas necessárias para a geração de código não são parte da notação Event-B, tais como, condicional (IF), sequência (“;”), repetição (WHILE), etc.

Diante do exposto nesta seção, conclui-se que a especificação e refinamento de uma aplica- ção Java Card, seguindo o método BSmart em Event-B traria um série de dificuldades, devido ao paradigma de especificação em Event-B não ser adequado à especificação de sistemas se- quenciais. As etapas de tradução também seriam prejudicadas, uma vez que não há em Event-B um módulo de implementação, determinístico, a partir do qual as aplicações Java Card fossem

traduzidas. No entanto, uma oportunidade para a aplicação de Event-B seria na especificação de propriedades globais do sistema smart card, por exemplo, no modelo da comunicação entre as aplicações cliente e cartão. Essa possibilidade será explorada como trabalho futuro.