Please enable JavaScript.
Coggle requires JavaScript to display documents.
Métodos Formais: Linguagem B - Coggle Diagram
Métodos Formais: Linguagem B
Sistemas que visão a segurança no contexto safety
Aplicado em sistemas criticos
Metodologia que visa a corretude do software e que o projetista tem a capacidade de visualizar se sua abordagem vai resolver ou falhar e onde isso vai ocorrer em determinado problema.
Conseguimos modelar softwares que não geram excessões
Temos um controle do significado do problema
Carro, trens, metros e avião
AtelierB: Ferramenta utilizada no curso que visa o desenvolvimento baseado na linguagem B
B é voltado para sistemas single-core
B é orientado a especificação
Declaração do behavior esperado pelo projetista
B é uma linguagem que tem forte apoio e inspiração na matemática, baseado em lógica de predicados e teoria dos conjuntos
B é validado por provas matemáticas
B é estruturado com noção de módulo e refinamento
Módulo: Dividido entre especificação do modulo e uma função
Especificação descreve o módulo
Função contém o algoritmo
Refinamento: Outro mecanismo de estruturação em B, significa adicionar detalhes na modelagem
Um projeto em B pode demonstrar normalmente um desenvolvimento em árvore, onde um refinamento leva a outro
ProB: Validação e animação do problema
MotionB: Visualização gráfica do problema
Conceitos:
Máquina abstrata aspecto estático: Onde o projetista irá definir as constantes e o conjunto que será trabalhado no modelo formal
Set: Definição do conjunto
Machine: Definição da máquina abstrata
Constants: Definição das constantes
Properties: Definição das propriedades/restrições
Invariants: Campo no qual espera que as propriedades declaradas não mudam ao decorrer da execução da máquina abstrata
Máquina abstrata aspecto dinâmico: Onde há variação nos estados
Initialisation: Declaração do estado inicial da máquina abstrata
Operations: Declaração das operações que regem o behavior da máquina abstrata
Refinamento: Após a implementação dos aspectos estático e dinâmico, o refinamento serve para aprimorar a máquina abstrata
Assim como na máquina abstrata apresenta também aspectos estáticos e dinâmicos
Estáticos
Variables: Onde declara as variaveis para o refinamento
Initialisation: Onde declara o estado inicial das variaveis
Dinâmicos
Operations: Onde é implementado as operações de refinamento
Implementação: Etapa após a implementação da máquina abstrata e do refinamento
Contém apenas o código B0 e apenas instruções padrão e estruturas de controles
Assim como na máquina abstrata e no refinamento, essa etapa é dividida em parte estática e parte dinâmica
Estática:
Values: Onde fornece valores para constantes
Concrete_variables: Onde há definição concreta de variaveis
Invariants: Campo no qual espera que as propriedades declaradas não mudam ao decorrer da execução da implementação
Initialisation: Onde declara o estado inicial das variaveis concretas
Dinâmica
Operations: Onde é descrito o behavior da implementação