Minicurso 1 - Safety Critical Applications Development with Atelier B (em Inglês)
Thierry Lecomte atualmente dirige Pesquisa e Desenvolvimento no ClearSy (http://www.clearsy.com/en/) , companhia francesa especializada em sistemas críticos. Suas atividades estão relacionadas ao desenvolvimento de ferramentas CASE, modelagem formal e validação de configurações, incluindo Atelier B (http://www.atelierb.eu/en/).
Resumo:
This session is divided into 2 parts:
-
Software development with Atelier B 5.0 The development of proven software in B is introduced through a number of examples (formal modelling and proof, C code generation). The focus is on the new features that ease the modelling process:
- Functional modelling: the software model is built independently from B model architectural constraints. The B project is generated automatically from this modelling.
- Improved proof performances: connected third party provers/solvers slightly reduce the proof effort when proving a software project.
The examples are chosen among simplified industrial applications from railways. The B language is introduced little by little as required by the formalizing of the software properties. Examples are demonstrated with Atelier B 5.0 Community Version. Code generation requires basic knowledge of gcc (compilation, linking). This session is a continuation of the course given at ETMF 2016 and hence requires a basic knowledge of the B language.
-
LCHIP (Low Cost High Integrity Platform)
LCHIP is a new technology aimed at revolutionizing the development of lightweight safety critical applications, up to SIL4. LCHIP building blocks are already embedded in certified railway applications (platform screen-doors controllers of Stockholm Citybanan and São Paulo L15 metros) and are expected to significantly lower the development and production costs of such systems. LCHIP is based on two concepts:
- A unique formal model (B language) of a function, to obtain a safe application embedding two redundant binaries of this function.
- A low cost high integrity execution platform, to ensure a safe execution through the detection of any divergent behavior.
Clique para baixar os slides utilizados no minicurso.
Minicurso 2 - Modular Static Analysis with Infer (em Inglês)
Jules Villard é atualmente engenheiro de software na equipe de ferramentas de análise estática no Facebook em Londres.
Resumo:
Infer is an open-source static analyzer that is used to find bugs in code at Facebook. Every month, Infer runs on thousands of code changes and detects hundreds of bugs that are fixed by developers before they reach production. Over the years, Infer has evolved from a standalone separation logic-based analyzer to a powerful framework for quickly implementing modular interprocedural analyses. This framework can take a simple intraprocedural analysis that computes the summary for a single procedure and lift it to a compositional interprocedural analysis that scales to millions of lines of code. Because of compositionality, the analysis can run much more quickly on a code change than on an entire codebase, opening the way to a “move fast” form of deployment which keeps pace with the workflow of developers.
Material utilizado no minicurso disponível em: https://github.com/jvillard/infer/tree/lab
Tutorial 1 - Model Checking de Código
Marcelo D’amorim é Professor Associado do Centro de Informática da UFPE (http://www.cin.ufpe.br/~damorim/). Sua área de pesquisa é Engenharia de Software, com foco em Testes, Verificação e Validação de Software. Seu interesse principal de pesquisa é em encontrar, diagnosticar, e reparar erros e vulnerabilidades em software.
Resumo:
Este tutorial foca em checagem de modelos para código C e Java. O tutorial terá uma parte teórica, para ilustrar conceitos e técnicas básicas, e uma parte prática onde demonstrações de conceitos serão feitas usando ferramentas como Java PathFinder, KLEE e ESBMC.
Material utilizado no tutorial disponível em: http://model-checking.dmtsj.com.br
Tutorial 2 - Validation of Critical Systems with Rewriting Logic in Maude
Christiano Braga é Professor Associado de Ciência da Computação do Instituto de Computação da Universidade Federal Fluminense (UFF) e pesquisador do Laboratório FR∀M∃. . Seus principais interesses em pesquisa são métodos formais e semântica de linguagens de programação. Grande parte de sua pesquisa tem Lógica de Reescrita como formalismo lógico e semântico subjacente, no sistema Maude em particular.
Resumo:
Sistemas críticos possuem características que, em caso de falha, podem afetar diretamente a 'raison d’être' do sistema ou seu entorno. Os chamados sistemas ciber-físicos, ubíquos hoje em dia, que têm, por exemplo, Internet das Coisas como subproblema, são intrinsecamente complexos dadas as características que os definem: concorrência, reatividade, sincronismo, tempo-real e alta-interação com o mundo físico.Neste tutorial estudamos o problema da verificação de algumas destas características. Utilizamos uma abordagem baseada em Lógica de Reescrita, onde computações são identificadas à deduções numa lógica apropriada, implementada no sistema Maude. Verificação é feita através de simulações num sistema concorrente, possivelmente de tempo-real, representado por um sistema de reescrita no qual os termos denotam os estados do sistema e as regras de reescrita seu comportamento. Validação de invariantes é realizada através de busca no espaço de estados do sistema, e a validação de propriedades temporais é feita, tanto explicitamente quanto simbolicamente, via 'model checking'.
Clique para baixar os slides utilizados no tutorial.
Material adicional para o tutorial.
Tutorial 3 - Cálculo Lambda: unindo Computação e Lógica
Rodrigo Machado é professor adjunto no Departamento de
Informática Teórica da UFRGS. Tem experiência em
lógica e semântica de programas, atuando principalmente nos seguintes temas:
semântica formal, modelos de computação, sistemas de reescrita de grafos e
linguagens de programação funcionais.
Resumo:
O Cálculo Lambda é um sistema formal criado na década de 1930 por Alonzo
Church que define como operações primitivas a definição e aplicação de
funções. Assim como o modelo de máquina proposto por Alan Turing, o Cálculo
Lambda foi um dos primeiros modelos de computação propostos, sendo de
fundamental importância para o início da Teoria da Computação. Na década de
1940 foi proposto o Cálculo Lambda Tipado, que introduziu regras de
compatibilidade para a construção de termos. Variações do Cálculo Lambda
Tipado servem como base para o desenvolvimento de linguagens de programação
funcionais (como Haskell e OCAML) e como base matemática para o estudo formal
da semântica de linguagens de programação em geral. Segundo a Correspondência
Curry-Howard, o Cálculo Lambda Tipado pode ser interpretado como uma lógica
dotada de sistema dedutivo onde tipos são vistos como propriedades e termos
são vistos como demonstrações. Essa é a ideia fundamental por trás dos
modernos assistentes de prova (como Coq e Agda) que permitem a prova de
propriedades sobre programas e a geração de código correto por construção.
Esta apresentação visa introduzir o formalismo Cálculo Lambda, contar um
pouco da sua história e clarificar sua influência nos campos da Ciência da
Computação e da Lógica.
Clique para baixar os slides utilizados no tutorial.
Tutorial 4 - Practices and challenges in Refactoring (em inglês)
Volker Stolz is an associate professor at the Western Norway University of Applied Sciences and the University of Oslo, Norway. He is site-leader for the European Horizon 2020 project "COEMS -- Continuous Observation of Embedded Multicore Systems", vice chair of the EU COST Action IC1402 "ARVI -- Runtime Verification Beyond Monitoring", and Visiting Professor at the Guizhou Academy of Sciences, Guiyang. Before moving to Norway, Dr. Stolz held an Assistant Research Fellow position at UNU-IIST, Macao (now UNU-CS), where he was principal investigator in the MSTDF-funded project on "Applied Runtime Verification".
Resumo:
Refactoring is an important software engineering task. In this tutorial, we will first look at the underlying principles and the improvements we can expect from refactoring code. Then, we compare refactoring support in common integrated development environments (IDEs) and editors for popular programming languages. We will also discuss the limitations of current tools, and give potential research directions (ranging in difficulty from a Master thesis project to problems that are very well worth a PhD).
Clique para baixar os slides utilizados no tutorial.
