Arquitectura e Cálculo

Índice

Objectivos

Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos.

Resultados de aprendizagem

• *Conhecer e caracterizar modelos para computação reactiva baseados em diferentes tipos de sistemas de transição, nomeadamente com evolução não-determinística, em tempo real ou estocástica.
• *Formular propriedades sobre esses modelos e analisar a sua satisfação.
• *Familiarizar-se com a noção de coordenação de software e utilizá-la produtivamente na definição de arquitecturas de sistemas reactivos.
• *Conhecer e utilizar ferramentas computacionais de suporte.
• *Integrar os conhecimentos adquiridos para utilização no projecto de engenharia de sistemas reactivos.

Programa Resumido

• Introdução aos sistemas reactivos
• Fundamentos
  • Semântica: Sistema de transição etiquetado. Morfismo. Noção de simulação e bissimulação. Bissimilaridade e sua relação com noções intuitivas de equivalência de comportamentos.Composição concorrente de sistemas de transição.
  • Lógicas: Introdução às lógicas modais e temporais. Taxonomia de propriedades dos sistemas reactivos. Tempo linear e tempo ramificado. Nominais e lógica híbrida.
• Modelação e análise de sistemas reactivos
  • Sistemas de transição não determinísticos (mCRL2).
  • Sistemas com requisitos de tempo real (Uppaal).
  • Sistemas com evolução probabilística (IMC).
• Arquitectura de sistemas reactivos
  • Motivação: Arquitectura de sistemas reactivos.
  • O paradigma de coordenação: Interacção mediada por conectores.
  • O modelo e a linguagem reo: Sintaxe e semântica. *Projecto e integração de ferramentas.

Material de Apoio (notas e slides)

Software Architecture for Reactive Systems

Background: Labelled Transition Systems

Background: Modal, Temporal, Hybrid Logics

Time-critical Systems

Probabilistic Systems

Architectural design: the coordination perspective

Coordination and Software Composition (Invited Lecture by Prof Farhad Arbab)

Bibliografia recomendada

• J. Groote e M. Mousavi: Modeling and analysis of communicating systems. MIT Press, 2014.
• L. Aceto et al: Reactive systems: Modelling, specification and verification. Cambridge University Press, 2007.
• H. Hermanns: Interactive Markov chains: The quest for quantified quality. Springer Lect. Notes Comp. Sci. (2428), 2002.

Bibliografia complementar

• C. Baier e J.-P. Katoen: Principles of Model Checking. MIT Press, 2008
• P. Blackburn, M. Rijke e Y. Venema: Modal Logic. Cambridge University Press, Cambridge, 2001.
• T. Brauner: Hybrid Logic and its Proof-Theory. Applied Logic Series, Springer, 2010.
• A. Aldini, M. Bernardo e A. Corradini: A Process Algebraic Approach to Software Architecture. Springer Verlag, 2010.

Ferramentas

Funcionamento

Docente

• Luís Soares Barbosa

Avaliação

• Prova individual escrita (70%)
• Mini-projecto de grupo (30%)
• As notas finais superiores ou iguais a 19 valores terão que ser defendidas em prova oral.

• Aviso: exame de recurso é dia 17 --- Todos os alunos, qualquer que tenha sido a nota obtida no teste, poderão comparecer.
• Aviso: dia 17 é também a deadline para a entrega de todos os trabalhos

• As classificações FINAIS encontram-se aqui.

Atendimento

-- Luís Soares Barbosa - 18 Julho 2015, 16.00h