Objectivos

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

Programa resumido

• Introduction to software architecture
• Background
  • (Semantics) Introduction to transition systems (mCRL2)
  • (Logic) Introduction to modal, hybrid and dynamic logic (mCRL2)
• Models and calculi of reactive systems
  • Timed (with real time constraints) (Uppaal)
• Architecture for reactive systems
  • Coordination-oriented architectural design (ECT)
    • Paradigm: The Reo exogenous coordination model
    • Method: Compositional specification of the glue layer
• Resource analysis of concurrent systems
  • Analysis of a Java-based language (ABS tool-set)

Material de apoio

Slides

• 1: Software Architecture for Reactive Systems
• 2: Background - Labelled transition systems
• 3: Introduction to Modal Logic
• 4: Modelling time-critical reactive systems
• 5: Verifying time-critical reactive systems
• 6: Coordination-oriented design with Reo
• 7: Semantics of Reo connectors

Exercícios e projectos

• mCRL2 tutorial - the rope bridge
• Assignment 1 - a mCRL2 exercise
• Assignment 2 - Coordination of Time-critical systems
• Testes anteriores
  • Teste de 2015/2016
  • Teste de 2016/2017

Links úteis

• mCRL2 website
• UPPAAL website
• Reo project
• Reo animations
• Reo Live
• ABS tool-set

Bibliografia

• Formal Modeling and Analysis of Software Architecture: Components, Connectors, and Events
• Principles Of Model Checking
• Modal Logic for Open Minds
• Modal Logic: a semantic perspective
• Reactive Systems: Modelling, Specification and Verification
• A tutorial on Uppaal
• Overview of Thirty Semantic Formalisms for Reo
• Reo + mCRL2 : A framework for model-checking dataflow in service compositions

Anos anteriores

• (actual), 2016/17, 2015/16, 2014/15

AC está a acabar - e agora?

Se gostas de especificação formal de software e de uma vertente matemática na análise de programas, então temos vários projectos com bolsas de investigação no nosso grupo.

Funcionamento

Docentes

Avaliação

• Projecto 1 (10%)
  • Entrega: 23 Março @ 23h59
  • RESULTADOS
• Projecto 2 (20%)
  • Entrega: 3 Junho @ 23h59
  • RESULTADOS
• Prova individual escrita (70%) - 5 Junho @ 10h, DI-0.05 (antiga 0.02)
• Exame de recurso (70%) - 21 Junho @ 8h30, CP2 1.07
• As notas finais superiores ou iguais a 19 valores terão que ser defendidas em prova oral.
• PAUTA PROVISÓRIA com resultados da prova escrita.

Atendimento

• Horário: 4ª 10h-12h (por marcação)
• Marcação: jose arroba proenca ponto org / lsb arroba di ponto uminho ponto pt