Método Formal B

1

Método Formal B

Alunos:Eduardo Akira YonekuraRogério Esteves Salustiano

Eduardo Akira Yonekura (025989) - Rogério Esteves Salustiano(982094) MO409

Tópicos abordadosTópicos abordados

Histórico IntroduçãoNotaçãoAplicação ao Estudo de CasoB-ToolkitConclusõesDesvantagensVantagensReferências Bibliográficas


HistóricoHistó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)


IntroduçãoIntroduçã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.


Notação – cláusulas de uma máquinaNotação – cláusulas de uma máquina

MACHINE define o nome da máquina abstrata

EXTENDS permite importar instâncias de outras máquinas

SEES outras máquinas que serão utilizadas dentro desta

SETS especifica os conjuntos que são manipulados

CONSTANTS define todas as constantes que são manipuladas PROPERTIES expressões lógicas que são satisfeitas pelas

constantes

VARIABLES define as variáveis utilizadas na máquina

DEFINITIONS uma série de definições utilizadas na máquina

INVARIANT propriedade dos atributos definidos nas VARIABLES

INITIALIZATION atribuição de valores iniciais às VARIABLES

OPERATIONS define todas as operações (procedimentos e funções) da máquina; deve ser a última cláusula a ser declarada

END fim da máquina abstrata


Notação – exemploNotação – exemplo

MACHINE machine_nameVARIABLES 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


Diagrama de Classes do Sistema de Elevadores Diagrama de Classes do Sistema de Elevadores


NotaçãoNotaçã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


NotaçãoNotação

VARIABLES Ex: elev, dir, andar_dest, por_stat, est_elev

INVARIANT Ex: elev <: ELEVADOR & botao <: BOTAO ultimo > terreo


NotaçãoNotação

OPERATIONS

chama_elevador(ll,fl) =PRE ll : elev & fl : ANDARTHEN ...

WHENest_elev(ll) = pronto & fl > andar_dest(ll) THENandar_dest(ll):= fl ||dir(ll) := sobe ||est_elev(ll) := em_mov


Ferramenta B-ToolkitFerramenta B-Toolkit


Ferramenta B-ToolkitFerramenta B-Toolkit


Especificação B para o sistema de elevadoresEspecificação B para o sistema de elevadores


Vantagens e DesvantagensVantagens 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.


Referências BibliográficasReferências Bibliográficas

Using the B formal approach for incremental specification design of interactive systems. Yamine Ait-Ameur, 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


Sistema de elevadores MACHINE TypesSistema 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

PROPERTIESterreo : NAT &ultimo : NAT &terreo < ultimo &ELEVADOR <: OBJECTS &BOTAO <: OBJECTS

END


Sistema de elevadores MACHINE ElevadorSistema de elevadores MACHINE Elevador

MACHINE Elevador

SEES Types

VARIABLES elev, dir, andar_dest, por_stat, est_elev

INVARIANTelev <: ELEVADOR &dir : elev-->DIREC &andar_dest : elev-->ANDAR &por_stat : elev-->P_STATUS &est_elev : elev-->ELEV_ESTADO

INITIALISATION ANY ll WHEREll <: ELEVADOR &ll /= {}THENelev := ll /* || *//* dir := ll * {dir_sobe} /* || *//* andar_dest := ll * {terreo} || *//* por_stat := ll * {p_fechado} || *//* est_elev := ll * {pronto} */END

DEFINITIONSANDAR == {terreo,ultimo}

OPERATIONSelevador_desce(ll) = PRE

ll : elev THEN dir(ll) := desce END;

elevador_sobe(ll) =PRE ll : elev

THEN dir(ll) := sobeEND;

elevador_setdestino(ll,fl) =PRE ll : elev & fl : ANDARTHEN andar_dest(ll) := flEND;

fl <-- elevador_getDestino(ll) =PRE ll : elevTHEN fl := andar_dest(ll)END;


Sistema de elevadores MACHINE Elevador (cont.)

Sistema de elevadores MACHINE Elevador (cont.)

elevador_fechport(ll) =PRE ll : elevTHEN por_stat(ll) := p_fechadoEND;

elevador_abrport(ll) =PRE ll : elevTHEN por_stat(ll) := p_abertaEND

END


Sistema de elevadores MACHINE BotãoSistema de elevadores MACHINE Botão

MACHINE Botao

SEES Types

USES Elevador

VARIABLES botao, botao_andar, botao_estado, elev_botao

INVARIANTbotao <: 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}] ) = 2 )

INITIALISATION ANY bb, ff, lb WHEREbb <: BOTAO &ff : bb --> ANDAR &ran(ff) = ANDAR &lb : bb -->elev &!(ll,fl).(ll:elev & fl : ANDAR =>

card(lb~[{ll}]/\ff~[{fl}] ) = 2 )

THEN botao := bb || botao_andar := ff || botao_estado := bb * {botao_off} || elev_botao := lb

END

DEFINITIONS ANDAR == (terreo...ultimo)

OPERATIONS fl <-- botao_getAndar(bt) = PRE

bt : botao THEN fl := botao_andar(bt) END;

botao_mudaOffOn(bt) = PRE bt : botao & botao_estado(bt) = botao_off THEN botao_estado(bt) := botao_on END;


Sistema de elevadores MACHINE Botão (cont.)

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


Sistema de Elevadores MACHINE ControleSistema de Elevadores MACHINE Controle

MACHINE Controle

SEES Types

VARIABLES elev, dir, andar_dest, por_stat, est_elev, botao, botao_andar, botao_estado, elev_botao

INVARIANTelev <: 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 ) */

INITIALISATIONANY 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 := lbEND

DEFINITIONSANDAR == {terreo..ultimo}


Sistema de Elevadores MACHINE Controle (cont.)

Sistema de Elevadores MACHINE Controle (cont.)

OPERATIONSelevador_ocupado(ll) =PRE ll : elev THEN SELECT

est_elev(ll) = em_visita THENpor_stat(ll) := fechada || est_elev(ll) := pronto

ELSEskip

ENDEND;

chama_elevador(ll,fl) =PRE ll : elev & fl : ANDARTHEN SELECT

est_elev(ll) = em_visita & fl = andar_dest(ll) THEN

por_stat(ll) := aberta || est_elev(ll) := em_visita WHENest_elev(ll) = pronto & fl > andar_dest(ll) THENandar_dest(ll):= fl ||dir(ll) := sobe ||est_elev(ll) := em_mov

ELSEskip

ENDEND;

elevador_chega(ll,fl) =PRE ll : elev & fl : ANDARTHEN 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}] THENbotao_estado := botao_estado<+{b1|->botao_off,b2|-

>botao_off} END || est_elev(ll) := em_visita || por_stat(ll) := aberta ELSE skip ENDEND;

aperta_botao(bt) = PRE bt : botaoTHEN SELECT botao_estado(bt) = botao_off THEN botao_estado(bt) := botao_on ELSE skip ENDEND END

Documents

Método Formal B