Short Courses/2a. Escola de Linguagens de Programação

Quarta, 26 de maio

• 09:00 - 10:30 .NET Framework (ppt)
  Joel Pereira (Microsoft)
• 10:30 - 11:00 Coffee break
• 11:00 - 12:30 .NET Framework
  Joel Pereira (Microsoft)
• 12:30 - 14:00 Almoço
• 14:00 - 15:30 Programação Orientada a Aspectos com C# (pdf)
  Paulo Borba (UFPE)
• 15:30 - 16:00 Coffee break
• 16:00 - 17:30 Programação Orientada a Aspectos com C#
  Paulo Borba (UFPE)

Quinta, 27 de maio

• 09:00 - 10:30 C# e Programação Genérica (ppt)
  Joel Pereira (Microsoft)
• 10:30 - 11:00 Coffee break
• 11:00 - 12:30 C# e Programação Genérica
  Joel Pereira (Microsoft)
• 12:30 - 14:00 Almoço
• 14:00 - 15:30 Modeling and Analyzing Protocols in Maude (pdf)
  Peter Ølveczky (Univ. of Oslo)
• 15:30 - 16:00 Coffee break
• 16:00 - 17:30 Modeling and Analyzing Protocols in Maude
  Peter Ølveczky (Univ. of Oslo)

Sexta, 28 de maio

• 09:00 - 10:30 Linguagens interpretadas na adaptação dinâmica de aplicações (pdf)
  Renato Cerqueira (PUC-Rio)
• 10:30 - 11:00 Coffee break
• 11:00 - 12:30 Linguagens interpretadas na adaptação dinâmica de aplicações
  Renato Cerqueira (PUC-Rio)
• 12:30 - 14:00 Almoço
• 14:00 - 15:30 A Evolução da Plataforma J2EE (pdf)
  Alex de Vasconcellos Garcia (IME)
• 15:30 - 16:00 Coffee break
• 16:00 - 17:30 A Evolução da Plataforma J2EE
  Alex de Vasconcellos Garcia (IME)

Slides: (ppt)

Resumo: Serão abordados os conceitos básicos de uma máquina virtual multilinguagem, assim como as razões de sua existência elencando suas vantagens e desvantagens. Serão mostrados como o padrão se tornou um padrão aberto e as diferenças principais da implementação comercial (.NET Framework) para a versão acadêmica SSCLI (Rotor).

Programação Orientada a Aspectos com C#

Slides: (pdf)

Resumo: Neste mini-curso apresentamos os principais conceitos de programação orientada a aspectos, ilustrando como os mesmos podem ser implementados em uma extensão de C# orientada a aspectos. Discutimos também como esta nova técnica de programação complementa a orientação a objetos com importantes construções para modularização de sistemas.

C# e Programação Genérica

Slides: (ppt)

Resumo: Nesta apresentação serão abordados os conceitos básicos da programaçào genérica, permitindo ao aluno entender as razões de sua existência e que tipos de problemas são mais facilmente resolvidos com o uso desta. Vários exemplos serão mostrados na plataforma .NET que oferece tais funcionalidades que implementam "generics".

Modeling and Analyzing Protocols in Maude

Slides: (pdf)

Abstract: Communication protocols are high-level descriptions of distributed computer systems, and include broadcast and multicast protocols, database protocols, and security protocols. Such protocols are notoriously hard to design and understand due to nondeterminism and reactivity. One notable example is the Needham-Schroeder public-key (NSPK) authentication protocol, a security protocol usually described in three lines, which was widely used and cited for almost 20 years before its fatal flaws were discovered.

It is important to understand and analyze protocols, since it is well known that errors in a software system should be discovered as early as possible in the software development process. Protocols are often described informally using plain text or UML- and C-like notation. Such specifications are usually ambiguous, hard to test and reason about, and usually contain crucial unstated assumptions.

Formal (i.e. logic-based) methods have been advocated to ameliorate this situation by providing specification formalisms in which protocols can be described, so that the meaning of the protocol is clear, so that it is possible to reason about the consequences of the protocol, and so that the protocol can be tested and analyzed automatically. Traditionally, formal methods have been met with some skepticism because:

• some specification formalisms can be non-intuitive and mathematically difficult,
• sometimes different formalisms are needed to describe different kinds of protocols, or different protocol parts,
• flaky and ever-changing tool support, and/or
• belief that formal methods are all about program (or protocol) verification, which is arguably a very hard task.

• the increasing maturity of formal methods and tools,
• better understanding of where, when, and what kind of formal analysis is feasible,
• an increasing number of success stories in the use of formal methods, and
• the complexity, cost, and criticality of modern computer systems.

Maude is a widely used state-of-the-art formal specification language and tool, and has been shown to be well suited to specify and analyze a wide array of sophisticated communication protocols.

The Maude specification language emphasizes ease and generality of specification. The language is intuitive and flexible, in which many different kinds of systems and system parts can be naturally specified. In particular, distributed systems can be naturally specified in an object-oriented way.

Maude specifications are executable, and the Maude rewrite engine is high-performance tool which can perform millions of rewrites per second. The tool supports a wide range of increasing stronger formal methods for automatically analyzing Maude specifications, including

1. symbolic simulation for prototyping purposes, in which one possible behavior of the system is simulated,
2. search for certain states reachable from the initial state,
3. in case the state space reachable from the initial state is finite, one can use Maude's efficient linear temporal logic model checker to analyze all behaviors from the initial state.

I have used Maude for specifying and analyzing some advanced protocols, including new active network multicast and broadcast protocols, and security protocols, and have started working on wireless sensor network protocols. My Maude analysis of the multicast protocol uncovered serious design flaws in the protocol which was not found during traditional testing and simulation, and the Maude analysis revealed a fundamental flaw in the already published and "proved" broadcast protocol.

This talk will introduce Maude and its capabilities in a high-level way, will give some examples of modeling and analysis of broadcast, database, and/or security protocols in Maude, and will give an overview of other protocols analyzed by Maude. The talk will be quite introductory and reasonable non-technical, and does not assume any prior knowledge of formal methods.

Slides: (pdf)

Resumo: As aplicações para computadores têm passado por grandes transformações. A popularização da Internet e as conexões de alta velocidade criaram oportunidades para o desenvolvimento de uma nova geração de aplicações, que integram dados, processos e pessoas ao redor do mundo. Mais recentemente, os avanços das tecnologias de computação móvel apontam para um modelo de computação ubíquo, onde usuários têm acesso às suas aplicações e aos seus dados em qualquer lugar e a qualquer instante. A disponibilidade de uma infra-estrutura computacional distribuída em larga escala e interconectada através de redes de alta-velocidade também traz novas perspectivas para a área de computação de alto desempenho.

Esses avanços tecnológicos trazem novos desafios para o desenvolvimento de aplicações. Entre esses desafios está a necessidade de se desenvolver aplicações capazes de se adaptarem dinamicamente a mudanças em seus ambientes de execução ou nos requisitos a que devem atender. As infra-estruturas de software que dão apoio a essa nova geração de aplicações têm evoluído em direção a oferecer um melhor suporte à adaptação dinâmica. Mas ainda há muito a ser feito, principalmente se considerarmos as ferramentas e modelos de programação oferecidos atualmente aos desenvolvedores de software.

Neste mini-curso, veremos como uma linguagem interpretada pode auxiliar no desenvolvimento de aplicações capazes de serem adaptadas dinamicamente, especialmente no caso de sistemas distribuídos. Apresentaremos algumas ferramentas desenvolvidas pelo nosso grupo na PUC-Rio, assim como alguns experimentos e aplicações industriais desenvolvidas com essas ferramentas.

Slides: (pdf)