Método Formal B
Alunos:
Eduardo Akira Yonekura
Rogério Esteves Salustiano
1
Tópicos abordados
Histórico
Introdução
Notação
Aplicação ao Estudo de Caso
B-Toolkit
Conclusões
Desvantagens
Vantagens
Referências Bibliográficas
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Histórico
 Desenvolvido por J.R. Abrial em 1985.
 Uma “extensão” com melhorias de VDM e Z.
 Aceitação na indústria a partir de 1992, a partir
de estudos de casos bem sucedidos.
 O método B foi utilizado no projeto do controle
dos trens do metrô de Paris (1998)
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Introdução
 B utiliza o conceito de Máquinas Abstratas (Abstract Machines),
que encapsulam:
estados: que consistem de variáveis restringidas por
invariantes (tipos das variáveis).
operações: que modificam o estado das variáveis, porém sem
alterar os invariantes.
 As MACHINEs podem ser vistas como Classes, porém com um
nível de detalhamento muito mais rigoroso.
 As MACHINEs trabalham com o conceito de substituição: a única
maneira de fazer a máquina ter progresso é alterar (substituir) o
valor do seu estado.
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Notação – cláusulas de uma máquina
MACHINE
EXTENDS
SEES
SETS
CONSTANTS
PROPERTIES
VARIABLES
DEFINITIONS
INVARIANT
INITIALIZATION
OPERATIONS











END

define o nome da máquina abstrata
permite importar instâncias de outras máquinas
outras máquinas que serão utilizadas dentro desta
especifica os conjuntos que são manipulados
define todas as constantes que são manipuladas
expressões lógicas que são satisfeitas pelas constantes
define as variáveis utilizadas na máquina
uma série de definições utilizadas na máquina
propriedade dos atributos definidos nas VARIABLES
atribuição de valores iniciais às VARIABLES
define todas as operações (procedimentos e funções) da
máquina; deve ser a última cláusula a ser declarada
fim da máquina abstrata
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Notação – exemplo
MACHINE machine_name
VARIABLES var1, var2 ...
SEES machine1, machine2, ...
INVARIANT var1  tipo1, var2  tipo2, ...
INITIALIZATION var1 := val1, var2 := var2 ...
OPERATIONS
operação_1(var_aux1, var_aux2, ...)
PRE var_aux1  tipo1, var_aux2  tipo2, ...
THEN <executa substituição de var1, var2, ...>
END;
ret_value  operação_2
BEGIN <atribui valor ao ret_value>
END;
...
END
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Diagrama de Classes do Sistema de Elevadores
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Notação
MACHINE
Ex: MACHINE Elevador
SETS
Ex: DIREC = {sobe,desce};
P_STATUS = {aberta,fechada};
BOTAO_ESTADO = {botao_on,botao_off};
ELEV_ESTADO = {pronto,em_mov,em_visita}
PROPERTIES
Ex: terreo : NAT &
ultimo : NAT
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Notação
VARIABLES
Ex: elev, dir, andar_dest, por_stat, est_elev
INVARIANT
Ex: elev <: ELEVADOR &
botao <: BOTAO
ultimo > terreo
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Notação
OPERATIONS
chama_elevador(ll,fl) =
PRE
ll : elev &
fl : ANDAR
THEN
...
WHEN
est_elev(ll) = pronto & fl > andar_dest(ll) THEN
andar_dest(ll):= fl ||
dir(ll) := sobe ||
est_elev(ll) := em_mov
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Ferramenta B-Toolkit
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Ferramenta B-Toolkit
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Especificação B para o sistema de elevadores
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Vantagens e Desvantagens
 Desvantagens
Alto grau de complexidade.
Não é trivial encontrar bons invariantes.
Poucas ferramentas disponíveis (Atelier-B e B-Toolkit).
 Vantagens
Métodos de prova “exatos” (gerados automaticamente ou pelo
usuário).
As especificações são geradas utilizando uma abordagem
incremental, o que facilita a especificação de um sistema
complexo.
Boa interação com UML e Statecharts.
Extensa bibliografia com estudos de casos complexos.
Boa aceitação na indústria.
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Referências Bibliográficas
 Using the B formal approach for incremental
specification design of interactive systems. Yamine AitAmeur, et. al.
 Supplementing a UML development process with B.
Helen Treharne. FME 2002.
 Using B formal specifications for analysis and verification
of UML/OCL models. R. Marcano. UML 2002, Model
Engineering, Concepts and Tools. Workshop on
Consistency Problems in UML-based Software
Development.
 B Toolkit - User´s manual
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Sistema de elevadores  MACHINE Types
MACHINE Types
SETS
OBJECTS;
DIREC = {sobe,desce};
P_STATUS = {aberta,fechada};
BOTAO_ESTADO = {botao_on,botao_off};
ELEV_ESTADO = {pronto,em_mov,em_visita}
CONSTANTS
terreo, ultimo, ELEVADOR, BOTAO
PROPERTIES
terreo : NAT &
ultimo : NAT &
terreo < ultimo &
ELEVADOR <: OBJECTS &
BOTAO <: OBJECTS
END
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Sistema de elevadores  MACHINE Elevador
MACHINE Elevador
SEES
Types
VARIABLES elev, dir, andar_dest, por_stat, est_elev
INVARIANT
OPERATIONS
elevador_desce(ll) =
PRE
ll : elev
THEN
dir(ll) := desce
END;
elev <: ELEVADOR &
dir : elev-->DIREC &
andar_dest : elev-->ANDAR &
por_stat : elev-->P_STATUS &
est_elev : elev-->ELEV_ESTADO
INITIALISATION
ANY ll WHERE
ll <: ELEVADOR &
ll /= {}
THEN
elev := ll /* || */
/* dir := ll * {dir_sobe} /* || */
/* andar_dest := ll * {terreo} || */
/* por_stat := ll * {p_fechado} || */
/* est_elev := ll * {pronto} */
END
DEFINITIONS
ANDAR == {terreo,ultimo}
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
elevador_sobe(ll) =
PRE
ll : elev
THEN
dir(ll) := sobe
END;
elevador_setdestino(ll,fl) =
PRE
ll : elev &
fl : ANDAR
THEN
andar_dest(ll) := fl
END;
fl <-- elevador_getDestino(ll) =
PRE
ll : elev
THEN
fl := andar_dest(ll)
END;
MO409
Sistema de elevadores  MACHINE Elevador
(cont.)
elevador_fechport(ll) =
PRE
ll : elev
THEN
por_stat(ll) := p_fechado
END;
elevador_abrport(ll) =
PRE
ll : elev
THEN
por_stat(ll) := p_aberta
END
END
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Sistema de elevadores  MACHINE Botão
MACHINE Botao
SEES
Types
USES
Elevador
THEN
botao := bb ||
botao_andar := ff ||
botao_estado := bb * {botao_off} ||
elev_botao := lb
END
VARIABLES botao, botao_andar, botao_estado, elev_botao
DEFINITIONS
ANDAR == (terreo...ultimo)
INVARIANT
botao <: BOTAO &
botao_andar : botao --> ANDAR &
ran(botao_andar) = ANDAR &
botao_estado : botao --> BOTAO_ESTADO &
elev_botao : botao --> elev &
ran(botao_elev) = elev &
!(ll,fl).(ll:elev & fl : ANDAR =>
card(botao_elev~[{ll}]/\botao_andar~[{fl}] ) =
OPERATIONS
fl <-- botao_getAndar(bt) =
PRE
bt : botao
THEN
fl := botao_andar(bt)
END;
2)
INITIALISATION
ANY bb, ff, lb WHERE
bb <: BOTAO &
ff : bb --> ANDAR &
ran(ff) = ANDAR &
lb : bb -->elev &
!(ll,fl).(ll:elev & fl : ANDAR =>
card(lb~[{ll}]/\ff~[{fl}] ) = 2 )
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
botao_mudaOffOn(bt) =
PRE
bt : botao &
botao_estado(bt) = botao_off
THEN
botao_estado(bt) := botao_on
END;
MO409
Sistema de elevadores  MACHINE Botão
(cont.)
botao_mudaOnOff(bt) =
PRE
bt: botao &
botao_estado(bt) = botao_on
THEN
botao_estado(bt) := botao_off
END;
bt1,bt2 <-- getBotao(ll,fl) =
PRE
ll : elev &
fl : ANDAR
THEN
ANY b1,b2 WHERE
b1 : botao &
b2 : botao &
(b1,b2) = botao_elev~[{ll}] /\ botao_andar~[{fl}]
THEN
bt1 := b1 ||
bt2 := b2
END
END;
ll <-- getElevador(bt) =
PRE
bt : botao
THEN
ll := elev_botao(bt)
END
END
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Sistema de Elevadores  MACHINE Controle
MACHINE Controle
SEES
Types
VARIABLES elev, dir, andar_dest, por_stat, est_elev, botao,
botao_andar, botao_estado, elev_botao
INVARIANT
elev <: ELEVADOR &
dir : elev --> DIREC &
andar_dest : elev--> ANDAR &
por_stat : P_STATUS &
est_elev : elev --> ELEV_ESTADO &
botao <: BOTAO &
botao_andar : botao --> ANDAR &
/* ran(botao_andar) : botao --> ANDAR & */
botao_estado : botao --> BOTAO_ESTADO
elev_botao : botao --> elev /* & */
/* ran(elev_botao) = elev /* & */
/* !(ll,fl).(ll:elev & fl : ANDAR =>
card(botao_elev~[{ll}]/\botao_andar~[{fl}] ) = 2 ) */
INITIALISATION
ANY ll,bb,ff,lb WHERE
ll <: ELEVADOR &
ll /= {} &
bb <: BOTAO &
ff : bb --> ANDAR &
ran(ff) = ANDAR &
lb : bb --> ll &
/* ran(lb) = ll & */
/* !(li,fl).(li:elev & fl : ANDAR =>
card(lb~[{li}]/\ff~[{fl}] ) = 2 ) */
THEN
elev := ll ||
dir := ll * {sobe} ||
andar_dest := ll * {terreo} ||
por_stat := ll * {} ||
est_elev := ll * {pronto} ||
botao := bb ||
botao_andar := ff ||
botao_estado := bb * {botao_off} ||
elev_botao := lb
END
DEFINITIONS
ANDAR == {terreo..ultimo}
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409
Sistema de Elevadores  MACHINE Controle
(cont.)
OPERATIONS
elevador_ocupado(ll) =
PRE
ll : elev
THEN
SELECT
est_elev(ll) = em_visita THEN
por_stat(ll) := fechada ||
est_elev(ll) := pronto
ELSE
skip
END
END;
chama_elevador(ll,fl) =
PRE
ll : elev &
fl : ANDAR
THEN
SELECT
est_elev(ll) = em_visita & fl = andar_dest(ll) THEN
por_stat(ll) := aberta ||
est_elev(ll) := em_visita
WHEN
est_elev(ll) = pronto & fl > andar_dest(ll) THEN
andar_dest(ll):= fl ||
dir(ll) := sobe ||
est_elev(ll) := em_mov
ELSE
skip
END
END;
elevador_chega(ll,fl) =
PRE
ll : elev &
fl : ANDAR
THEN
SELECT est_elev(ll) = em_mov & fl = andar_dest(ll) THEN
ANY b1,b2 WHERE
b1 : botao &
b2 : botao &
(b1,b2) = elev_botao~[{ll}] /\ botao_andar~[{fl}]
THEN
botao_estado := botao_estado<+{b1|->botao_off,b2|>botao_off}
END ||
est_elev(ll) := em_visita ||
por_stat(ll) := aberta
ELSE skip
END
END;
aperta_botao(bt) =
PRE
bt : botao
THEN
SELECT botao_estado(bt) = botao_off THEN
botao_estado(bt) := botao_on
ELSE
skip
END
END
END
Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094)
MO409