Apresentação Circulos EFS

7/21/2019 Apresentação Circulos EFS.

http://slidepdf.com/reader/full/apresentacao-circulos-efs 1/43

Especificação formal de

Software



Agenda

● A familia Circus

● A notação Z

● Communicating Sequential Process - CSP

● Circus

● Referências



A Familia Circus

● A família circus de notação tem seu núcleo uma

combinação flexível de Z, CSP, especificação de

Morgan e comando de condição de guarda de Dijkstra.

● A Circus é uma linguagem para especificação,

programação e verificação por refinamento.



A familia Circus

● O projeto de Circus é anterior ao ano 2000 e foi

motivado pela necessidade de uma notação e técnicas

de projeto e implementação de processos “state-rich”.

● Ao longo dos anos foram criadas diversas extensões da

notação “Core” do circus.

● Há versões que focam em: orientação a objetos,sincronismo, mobilidade e compartilhamento. Há

também aplicações industriais que focam em sistemas

de controle.



A Família Circus

● A maioria dos esforços relacionados a Circus estão na

Universidade de York, mas há algumas pesquisas em

andamento na Newcastle, Brasil(Ana Cavalcanti -

UFPE), China, França, etc…

● Pesquisas sendo realizadas: Safety-critical Java

programs (SCJ), avionics control systems, and Systems

of Systems. Definição de uma teoria de testes técnicas

model-based testing.

● Tese de doutorado da universidade de York

Referência: http://www.cs.york.ac.uk/circus/index.html

http://www.cs.york.ac.uk/circus/index.html

http://www.cs.york.ac.uk/circus/index.html



Ferramentas Circus

● ProofPower: é uma ferramenta para apoiar

especificação e provas em Higher Order Logic e na

notação Z.

● CRefine: é uma ferramenta que pode ser usada no

refinamento de sistemas concorrentes. A Ferramenta

verifica especifcações circus aplicando leis de

refinamento. Implementado em Java.

● Circus Type Checker: ferramenta verificadora de

sintaxe para especificações circus.



Ferramentas Circus

● JCircus: é uma ferramenta que automaticamente traduz

programas Circus em Java para o propósito de

animação e simulação.

● ClawCircus: coleção de ferramentas baseadas em Java

com a função de gerar modelos Circus a partir de

diagramas simulink.

● Circus Parser: um parser Circus na comunidade Z tools.



Notação Z

● O modelo formal Z foi criado na Universidade de Oxford no fim da

década de 70, com o objetivo de servir como notação para a

especificação formal de sistemas.

● A notação gerada pela linguagem Z está baseada em princípios dematemática discreta e Lógica de Primeira Ordem.

● Z utiliza estruturas matemáticas como conjuntos, relações efunções para descrever o comportamento do sistema através da

construção de modelos, estados de um sistema e suas transições,

baseados em pré e pós-condições e invariantes.



Notação Z

● A notação Z descreve o estado e propriedades de um sistema e

também certas operações correspondentes a essa estrutura na

forma de pré e pós-condições.

● As operações correspondem a interações do sistema com o meioexterno.

● Quando operações são aplicadas aos componentes da estrutura

lógica, o estado do sistema se altera, refletindo o efeito da

interação no novo estado assumido pelo sistema.



Notação Z

● Propriedades de sistemas especificados em Z podem ser

validados de maneira simbólica, usando apenas o texto das

especificações, sem necessidade de testes sobre algum código

compilado.

● A especificação em Z é formada por um número de

esquemas que são decomposições da especificação em partes

menores.

● Z utiliza tipos para cada objeto definido(permite verificação de

tipos).



Sintaxe da Z

● As definições axiomáticas possuem uma parte declarativa e

outra predicativa.

● A especificação de um documento em notação Z consiste na

declaração de tipos primitivos, iniciais, enumerados, potência,definições axiomáticas, predicados e esquemas.

● Dentre os aspectos estáticos inclui-se:

○ Os estados que o sistema pode ocupar;

○ Os relacionamentos invariantes que são mantidos conforme o

sistema muda de estado;



Sintaxe do Z

● Dentre os aspectos

dinâmicos inclui-se:

○ As operações

possíveis;

○ A relação entre asvariáveis de

entrada e as

variáveis de saída;

○ As mudanças de

estado queacontecem.

Simbolos e operadores...



Sintaxe da Z

Declarações, abreviações,

abreviações genéricas,

definições axiomáticas,

definições genéricas e tuplas

Conjuntos



Sintaxe da Z

r elações binárias, domínio, imagem,imagem relacional, relação inversa,relação de composição e fechos.



Sintaxe Z

Sequencias



Sintaxe Z

Lógica proposicional



Notação Z



Ferramentas Z

● Diversas ferramentas estão catalogadas no

site do Z disponibilizado pela Universidade

de Oxford.

● Tipos de Ferramenta: ferramentas parachecagens sintática, semântica (de tipos),

de domínio e provadores de teoremas estão

disponíveis, assim como simplesvisualizadores da notação.



Ferramentas Z

● O formato do documento de especificação

aceito por estas ferramentas é baseado em

LATEX markup, uma extensão do LATEX.

● Ferramentas: Z/EVES, CADIZ, ZBrowser,

Fuzz, CZT, ZAST.



Exemplo de Especificação de uma FSM

estados = quadros, transições= arcos, evento

que dispara a transição = Labels



Exemplo de Especificação de uma FSM

No estado Patients, pressionando Enter, causa uma

transição para FIELDS e Pressionando Enter

novamente dispara uma Transição para SETUP



Exemplo especificação de um FSM

Tabela de Transição



Especificação em Z




Verificador

Sintático

? = indica que o parágrafonão foi testado.

Y= indica que o parágrafofoi testado e não há erros

sintáticos.

N = Erros sintáticos.




Provador

? = estado da prova nãopode ser determinado.

Y=indica que oparágrafonão possui “goals”

improváveis.

N = Indica que há o

parágrafo possui “goals”improváveis .



Communicating Sequential Process

CSP



● CSP é uma linguagem formal para descriçãode padrões de interações entre processos

concorrentes.

● CSP influenciou o projeto de diversas

linguagens, entre elas Limbo e Go.

● A linguagen foi aplicada na industria como

como uma ferramenta para especificar os

aspectos concorrentes dos sistemas.

CSP



CSP

● CSP foi descrita em 1978 em um artigo de

C.A. R. Hoare(vencedor do premio turing e

inventor do algol 60).

● Foi utilizada para modelar o sistema detolerancia a falhas utilizado na estação

espacial. Foi utilizado o CSP para garantir

que o projeto era livre de deadlock.



CSP

● CSP possui duas classes de primitivas:

○ Eventos: que representam comunicalção e

interação.

○ processos: que representam comportamentos

fundamentais.



CSP Sintaxe

● Uma máquina que demanda pagamento

antes de oferecer um chocolate:

● Uma pessoa que precisa escolher entre

moeda ou cartão para efetuar um

pagamento:



CSP Sintaxe

● Dois processos que podem ser colocados

em paralelo e eles podem interagir entre si.

O comportamento do processo composto

depende do evento que os processosdevem sincronizar.



CSP - Sintaxe

● COPY = *[c:character; west?c → east!c]

● [west::DISASSEMBLE || X::COPY || east::ASSEMBLE]



CSP Ferramenta

● ProCSP. Faz verificação sitática e a

checagem de modelos em CSP.



CSP Ferramenta

● ProCSP. Faz verificação sitática e a

checagem de modelos em CSP.



Circus



Circus

● O objetivo do Circus é prover uma base para

o desenvolvimento de sistemas distribuidos

e concorrentes em um estilo “calculacional”.

● Programas Circus são formados por uma

sequência de parágrafos:

○ Program::=CircusPar*(zero ou mais parágrafos)



Circus

● Linguagens como Z, VDM, ASM(Abstract State

Machines) e B, utilizam uma abordagem (model-based)

baseada em modelos onde elementos da matemática

formam a base da especificação.

● Embora possível de uma forma bastante difícil e

implícita, elementos de especificação para modelar

aspectos comportamentais, tais como escolha,

seqüência, composição paralela, e outros, não são

explicitamente fornecida por qualquer uma dessas

linguagens.



Circus

● A falta de apoio para um refinamento de sistemas

“State-Rich” em um estilo “calculacional” motivou a

criação de circus (Concurrent Integrated Refinement

CalculUS).

● Em Circus sistemas são caracterizados como

processos onde elementos descrevem dados e

controle comportamental. A notação Z é usada para

definir a maioria dos aspectos de dados e CSP(Communicating Sequential Processes) é usada para

definir comportamento.



Circus

● Cada parágrafo pode ser um parágrafo Z (Denotado

pela categoria Par) , uma definição de “channels”, uma

definição de conjuntos de conjuntos “channels” e uma

declaração de processo.

Circus possui também a função de provador de teorema.



Circus Sintaxe

● Channel: “A channel denition declares the channels to

which the processes can refer”. Nomeia cada canal e e

o tipode valor que pode comunicar. Ex

○ channel out : N -> o canal out comunica com os

números naturais.



Circus Sintaxe

● Processes: “A process denition declares itsname and gives a process specication.”



Circus Sintaxe



Referencias

● http://www.cs.york.ac.uk/circus/publications/papers/06-oliveira.pdf

● https://www.lri.fr/~mcg/PDF/VSSTE2012.pdf

● http://www.bcs.org/upload/pdf/ewic_fm01_paper7.pdf

● http://www.graphviz.org/

● http://www.graphviz.org/Download_windows.php

● http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_First_Step

● http://www.cs.york.ac.uk/circus/publications/papers/05a-Freitas.pdf

● https://www.lri.fr/~mcg/PDF/VSSTE2012.pdf

Documents

Apresentação Circulos EFS