Preliminary program
Detailed SBMF Schedule
Download complete schedule (Word document).
Invited talks
- Claude Kirchner (INRIA, FR)
- Logical Aspects of the Rewriting Calculus (Invited talk 1)
- The rewriting calculus or rho-calculus uniformly integrates the
notions of pattern,
abstraction and application. This calculus makes explicit and first-
class all of its
components: matching (possibly modulo given theories), abstraction,
application and
substitutions.
The rewriting calculus is designed and used for logical and semantical purposes. It could be equipped with powerful type systems and used for expressing the semantics of rule based as well as object oriented languages. It allows one to naturally express exception handling mechanisms and elaborated rewriting strategies. It can be also extended with imperative features and cyclic data structures.
After presenting the motivations, the context and some history of the calculus, we will develop its logical side and show its relationship with sur-deduction modulo. - Rustan Leino (Microsoft, USA)
- Object Invariants in Specification and Verification (Invited talk 2)
- Spec# is research programming system that aims to provide programmers with a higher degree of rigor than in common languages today.
The Spec# language extends the object-oriented .NET language C#, adding features like non-null types, pre- and postconditions, and object invariants.
The system includes a static program verifier for proving that the program lives up to its specifications.
It is difficult to design a sound approach for specifying and verifying programs using object invariants. Spec# has used an approach known as the Boogie methodology. In our experience, we have found the need to extend the basic Boogie methodology to handle more common programming patterns. In this talk, I will describe the approach and our recent extensions.
The talk will also include a demo of the Spec# system.
Joint work with Mike Barnett, Bart Jacobs, Manuel Fahndrich, Peter Mueller, Wolfram Schulte, Herman Venter, and Angela Wallenburg. - Daniel Jackson, joint speaker with ICGT2006 (MIT, USA)
- Idioms of Logical Modelling (Invited talk 3)
- Most modeling languages embody a particular idiom: the state / invariant / operations
idiom for VDM and Z; the variable-update/temporal-logic idiom for SMV and
Murphi; the imperative-programming idiom for Promela and Zing; and so on. Fixing
an idiom makes tools easier to build, and helps novice modellers. But it also makes the
language less flexible.
Alloy is a modelling language that was designed, in contrast, to support multiple idioms. Its core is a simple but expressive relational logic, whose semantics consists of a set of bindings of relations to global variables. In other words, an Alloy model is a constraint, and its meaning is a set of graphs with labelled edges of varying arity. The Alloy Analyzer is a constraint solver that can find a graph satisfying a given constraint.
A variety of idioms can be readily expressed in Alloy, and analyzed using the Alloy Analyzer. You can structure the state as a global state variable with multiple components, or follow an object-oriented style, where the state is collection of objects, each with components whose values vary of time. You can express and analyze individual operation executions, using the inductive approach of languages like Z, or introduce traces and check them against linear temporal logic properties. Frame conditions can be written as conventional equalities in each operation, or in the style invented by Reiter.
In my talk, I'll explain the basics of Alloy, show how to express a variety of idioms, and describe some case studies using these idioms, including most recently an analysis by Tahina Ramanandro of the Mondex electronic purse (developed by NatWest Bank, and originally modelled in Z by Susan Stepney, David Cooper and Jim Woodcock).
Selected papers
The following papers have been accepted for presentation and publication in the conference proceedings:- Type Checking Circus Specifications. Manuela Xavier (Universidade Federal de Pernambuco), Ana Cavalcanti (University of York), Augusto Sampaio (Universidade Federal de Pernambuco)
- Formal Specification Generation from Requirement Documents. Gustavo Cabral (Universidade Federal de Pernambuco), Augusto Sampaio (Universidade Federal de Pernambuco)
- A Compositional Automata-based Approach for Model Checking Multi-Agent Systems. Mário Benevides (COPPE/Sistemas - Universidade Federal do Rio de Janeiro), Carla Delgado (COPPE/Universidade Federal do Rio de Janeiro and University of Edinburgh), Carlos Pombo(Unuversidad de Buenos Aires), Luis Lopes (COPPE/Universidade Federal do Rio de Janeiro), Ricardo Ribeiro (COPPE/Universidade Federal do Rio de Janeiro)
- Formal, Time Aware Modelling of Communication Channels for VLSI Systems. Tomi Westerlund (University of Turku), Juha Plosila (University of Turku)
- Domain-specific Refinement of Object Models. Jim Davies (Oxford University), David Faitelson (University of Oxford), James Welch (University of Oxford)
- Viewing CSP specifications with UML-RT diagrams. Patricia Ferreira (Universidade Federal de Pernambuco), Augusto Sampaio (Universidade Federal de Pernambuco), Alexandre Mota (Universidade Federal de Pernambuco)
- Undecidable Control Conditions in Graph Transformation Units. Karsten Hölscher (Universität Bremen), Renate Klempien-Hinrichs (Universität Bremen), Peter Knirsch (Universität Bremen)
- A calculus for team automata. Maurice ter Beek (CNR Pisa), Fabio Gadducci (University of Pisa), Dirk Janssens (University of Antwerp)
- Invariants for Non-Hierarchical Object Structures. Ronald Middelkoop (Technische Universiteit Eindhoven), Cornelis Huizing (Technische Universiteit Eindhoven), Ruurd Kuiper (Technische Universiteit Eindhoven), Erik Luit (Technische Universiteit Eindhoven)
- Conformance Testing Using Timed Extended Finite State Machines and Model Checking. Adilson Bonifácio (Universidade Estadual de Campinas), Arnaldo Moura (Universidade Estadual de Campinas), Adenilso Simão (ICMC-Universidade de São Paulo), José Maldonado (ICMC-Universidade de São Paulo)
- A Formal Framework for Establishing Conformance between Object Models and Object-Oriented Programs. Tiago Massoni (Universidade Federal de Pernambuco), Rohit Gheyi (Universidade Federal de Pernambuco), Paulo Borba (Universidade Federal de Pernambuco)
- Specification and Verification of the IEEE 802.11 Medium Access Control and an Analysis of its Applicability to Real-Time Systems. Frederico Barboza (Universidade Federal da Bahia), Aline Andrade (Universidade Federal da Bahia), Flávio Assis Silva (Universidade Federal da Bahia), George Lima (Universidade Federal da Bahia)
- An Institutional Theory for #-Components. Francisco Carvalho (Universidade Federal do Ceará), Rafael Lins (Universidade Federal de Pernambuco), Ana Teresa Martins (Universidade Federal do Ceará)
- Implementing Pointer in Temporal Logic Programming Languages. Zhenhua Duan (Xidian University), Xiaobing Wang (Xidian University)
- Identificação de Nomes Ativos em Cálculo-pi baseada em Tipos. Gleison Nascimento (Universidade Federal do Rio Grande do Sul), Alvaro Moreira (Universidade Federal do Rio Grande do Sul)
Mini-cursos (in Portuguese)
- Derivação Formal de Programas Concorrentes usando Circus (da especificação ao código)
- Marcel Oliveira - DIMAp/UFRN
- 18/09 (Segunda-feira) 10:30-12:30 e 20/09 (Quarta-feira) 10:30-12:30
-
Circus é um formalismo que combina CSP, Z e uma linguagem de comandos, e com isso consegue descrever os aspectos
de dados e de comportamento de um sistema elegantemente. Apesar de existir outras combinações que tentam
apresentar esta mesma característica, Circus é a única combinação que apresenta um
cálculo de refinamentos.
Neste mini-curso, apresentaremos um método de derivação formal de programas concorrentes. Uma vez aplicado, este método derivará, a partir de uma especificação formal em Circus, o código Java que implementa aquele sistema. A aplicabilidade do nosso método será ilustrada com o desenvolvimento de um estudo de caso industrial: um sistema de controle de incêndio. - Ferramentas de Apoio à Construção de Software Concorrentes e de Tempo Real Confiáveis
- Aline Andrade, Frederico Barboza - DCC/UFBA
- 18/09 (Segunda-feira) 10:30-12:30 e 20/09 (Quarta-feira) 10:30-12:30
- Softwares concorrentes e de tempo real fazem parte de muitas aplicações complexas e que envolvem risco e, portanto, a confiabilidade destes softwares é uma questão fundamental. Garantir confiabilidade de software não é trivial e existe muita pesquisa em torno deste tema. Uma das abordagens utilizadas com este fim diz respeito à utilização de ferramentas baseadas em métodos formais que permitem a verificação (prova) de propriedades do sistema. Este minicurso abordará conceitos relacionados à verificação de propriedades utilizando verificadores de modelos (model checkers). O foco estará em torno de sistemas concorrentes e de tempo real e serão apresentados conceitos relacionados à verificação de propriedades destes sistemas, propriedades safety, liveness e timeliness. Apresentaremos os verificador de modelo UPPAAL, ferramenta bastante utilizada na verificação de sistemas de tempo real.
- Modelagem e Validação de Sistemas Usando Redes de Petri
- Jorge Figueiredo - DSC/UFCG
- 20/09 (Quarta-feira) 15:30-17:30 e 20/09 (Quarta-feira) 18:00-20:00
-
Sistemas concorrentes e distribuídos são os mais desafiantes sistemas que são desenvolvidos na
prática. Entre muitos exemplos, podemos citar o desenvolvimento de aplicações baseadas na tecnologia
web ou sistemas embarcados. Sistemas dessa natureza são complexos e difíceis de se projetar e testar. É
importante que atividades de depuração e teste de partes
centrais dos sistemas sejam consideradas antes mesmo da implementação. Uma forma de se ter isso é
através da construção de um protótipo. Uma outra forma, em geral mais rápida, é
a construção de modelos executáveis. A inspeção e/ou simulação
destes artefatos podem revelar erros ou inconsistências em fases iniciais do processo de desenvolvimento do sistema.
Redes de Petri é um formalismo bastante interessante para tratar sistemas que exibam características de concorrência e distribuição. O formalismo de redes de Petri possui uma sólida teoria desenvolvida nas últimas quatro décadas, desde o estudo inicial, no começo dos anos 60, quando Carl Adam Petri, em sua tese de doutoramento, propôs uma teoria geral de concorrência. Além da simplicidade de seus conceitos, este formalismo apresenta uma notação gráfica que possibilita a apresentação do comportamento dos sistemas modelados, permitindo o uso de seus conceitos de forma intuitiva. Redes de Petri Coloridas (CPN) é talvez o mais conhecido e utilizado tipo de redes de Petri. CPN combina o poder de descrição de sincronização de processos concorrentes da teoria de redes de Petri com a definição de tipos de dados das linguagens de programação. Essa combinação resultou no desenvolvimento de uma poderosa linguagem de modelagem de sistemas, ao mesmo tempo bem embasada teoreticamente e bastante versátil para ser usada na prática, permitindo descrições de alto nível de sistemas através de redes de Petri. Este curso tem como foco principal a modelagem e validação de sistemas utilizando Redes de Petri Coloridas. O curso tem como público-alvo alunos de graduação e mestrado nas áreas de Ciência da Computação e Engenharia Elétrica.
Poster Session
- A Simulation-Oriented Formalization for a Psychological Theory
- Paulo Salem (USP), Ana Cristina V. De Melo (USP)
- Composition or Coordination:Two Models, Two Libraries
- Marco Castro Barbosa (Universidade do Minho), Jacome Cunha (Universidade do Minho), Luis Barbosa (Universidade do Minho)
- Management and Distributed Data Allocation for Digital Tutoring Systems based on Petri Nets
- Jussara Barros (Universidad de Salamanca)
- Distributed Model-Checking using Computational Grids
- Paulo Barbosa (UFCG), Cássio Rodrigues (UFCG), Jairson Cabral (UFCG), Jorge César Abrantes de Figueiredo (UFCG), Dalton Serey Guerrero (UFCG)
- Towards Modular Formal Islands: A Case Study for TOM
- Anderson Santana de Oliveira (INRIA and LORIA)
- Regras em Linguagem B para Mapeamento de Especificações Formais em Dados de Teste
- Fernanda de Souza (UFRN), Itamir Filho (UFRN)
- Comparação entre as notações Z e B através de um Estudo de Caso em Sistemas Integrados
- Gustavo Girão (UFRN), Monica Pereira (UFRN), Karla Ramos (UFRN), Ivan Silva (UFRN)
- KitSmart: Um kit de tipos e estruturas de dados projetados com o método B para o desenvolvimento rigoroso em JavaCard.
- Thiago Dutra (UFRN), Itamar Filho (UFRN), Katia Moraes (UFRN)
- Proof strategies for assertions with "generally"
- Leonardo Vana (UFRJ), Paulo Veloso (UFRJ), Sheila Veloso (UFRJ)
- Um procedimento de decisão para aritmética linear de inteiros
- Diego Oliveira (UFRN)
- Batcave: Um ambiente de verificação automática para o método B
- Cláudia Tavares (UFRN), David Déharbe (UFRN), Eberton Marinho (UFRN), Valério Gutemberg de Medeiros Júnior (UFRN)
- E-LIFT: Verifying E-LOTOS Specifications with SPIN
- Breno Ribeiro (UFS), Giovanny Lucero (UFS)
- Characterizing and Specifying Optimal and Correct Interval Functions in CASL
- Benjamín Bedregal (UFRN), Regivan Hugo Nunes Santiago (UFRN)
Overall Schedule
| ICGT/SBMF | Sunday 17/09 | Monday 18/09 | Tuesday 19/09 | Wednesday 20/09 | Thursday 21/09 | Friday 22/09 | ||||||||||||
| ROOMS | A1 | A2 | A3 | A1 | A2 | A3 | A1 | A2 | A3 | A1 | A2 | A3 | A1 | A2 | A3 | A1 | A2 | A3 |
| 10:30 - 11:00 | LSFA | MC1 | GCM | MC2 | TS1 | TS3 | TS4 | MC1 | MC2 | TS7 | SeTra | GraBaTs | PNGT | |||||
| 11:00 - 11:30 | ||||||||||||||||||
| 11:30 - 12:00 | ||||||||||||||||||
| 12:00 - 12:30 | ||||||||||||||||||
12:30 - 14:00 |
Lunch | Lunch | Lunch | Lunch | Lunch | |||||||||||||
| 14:00 - 14:30 | LSFA | IT1 | GCM | IT1 | TS4 |
IT3 |
IT2 |
SeTra | GraBaTs | PNGT | ||||||||
| 14:30 - 15:00 | ||||||||||||||||||
| 15:00 - 15:30 | GRA TRA tutorial |
B | B | B | B | TS8 | ||||||||||||
| 15:30 - 16:00 | TS1 | TS2 | TS5 | MC3 | B | B | ||||||||||||
| 16:00 - 16:30 | B | CB | SeTra | GraBaTs | ||||||||||||||
| 16:30 - 17:00 | IT2 | GraBaTs | PNGT | |||||||||||||||
| 17:00 - 17:30 | CB | CB | PS | |||||||||||||||
| 17:30 - 18:00 | LSFA | GRA TRA tutorial |
GCM | CB | CB | CB | ||||||||||||
| 18:00 - 18:30 | TS2 | TS3 | P | TS6 | MC3 | SeTra | GraBaTs | |||||||||||
| 18:30 - 19:00 | ||||||||||||||||||
| 19:00 - 19:30 | ||||||||||||||||||
| 19:30 - 20:00 | ||||||||||||||||||
| Conventions: |
| TS: Technical Session |
| IT: Invited talk |
| MC: Mini-course |
| PS: Poster Session |
| P: Panel |
| B: Break |
| CB: Coffee break |
| CEMF: SBC meeting |
| ICGT |
| SBMF |
| Joint ICGT+SBMF |
| satellite workshop |