Objectivos

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

Os sumários já estão disponíveis online.

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).
  • Probabilistic (PRISM).
• Architecture for reactive systems
  • Component-oriented architectural design.
    • Paradigm: Software components as monadic Mealy machines
    • Method: The mMm calculus; prototyping in Haskell
  • Coordination-oriented architectural design. (ECT)
    • Paradigm: The Reo exogenous coordination model
    • Method: Compositional specification of the glue layer

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
• 8: Interactive interaction constraints

Exercícios e projectos

• mCRL2 tutorial - the rope bridge [solutions]
• Assignment 1 - a mCRL2 exercise
• Assignment 2 - Time-critical systems
• Assignment 3 - Architecting the coordination layer

Links úteis

• mCRL2 website
• UPPAAL website
• Reo animations
• Interactive constraints (Reo)

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

MFES: outros anos

• (actual), 2016/17, 2014/15, 2013/14, 2012/13, 2011/12, 2010/11, 2009/10.

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. E a lista está sempre a crescer.

Funcionamento

Docente

• José Proença

Avaliação

• Projecto 1 (10%)
  • Entrega: 31 Março @ 14h
  • RESULTADOS
• Projecto 2 (15%)
  • Entrega: 15 Maio @ 23:59
  • Demo: 19 Maio @ 14h
  • RESULTADOS
• Projecto 3 (15%)
  • Entrega: 16 Junho @ 14h
  • Demo: 16 Junho @ 14h
  • RESULTADOS
• Prova individual escrita (60%) - 9 Junho @ 14h
• Exame de recurso (60%) - 30 Junho @ 14h (DI.0.03)
• 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 at proenca dot org