Objectives

This course is focussed on formal models and calculi for different sorts of software architectures, emphasising reactive and quantum systems.

Syllabus

• Software architecture, processes and interaction
• Classical reactive processes
  • (Modelling) Introduction to transition systems and process algebra
  • (Verification) Introduction to modal, hybrid and dynamic logic
  • (Tool) The mCRL2 framework
  • Variants: (Timed | Probabilistic | Hybrid) processes *
• Quantum processes
  • (Modelling) The quantum computational model
  • (Modelling) Quantum algorithmic processes
  • (Verification) Dynamic logic for quantum processes
  • (Tool) The Qiskit platform
• Coordination-oriented architectures
  • The Reo exogenous coordination model
  • Compositional specification of the glue layer

* The specific variant chosen for each course edition may vary

News

Please recall that the lectures scheduled for 4 and 11 April, will be replaced by a whole day session on quantum computation, including the practical, hands-on session with Qiskit, in the contex of the Quantum Days 2019.

The Quantum Days 2019 workshop will continue on Friday, 12 April, as you may check in the programme. You are most welcome to attend this second day, although this is not part of the AC course. Only the first day corresponds to formal lectures in the AC course.

Although participation is free of charge, please register here until March 31, so that coffee breaks are suitably ordered. Do this even if you intend to be present only in the fisrt day. Thanks.

Summaries (2018-19)

• Feb 14 (M): Introduction to the course. Labelled transition systems. Morphisms between transition systems. Notion of process algebra. Introduction to CCS.
• Feb 21 (M): Modelling processes and architectures in mCRL2. Behaviour equivalences and bisimulation.
• Feb 21 (T): Exercices on bisimulations. Modelling training in mCRL2.
• Mar 7 (M): Modelling time-critical reactive systems. Timed automata. Introduction to Uppaal.
• Mar 21 (M): Introduction to quantum computing. Quantum effects as computational resources: superposition and entanglement. The quantum computational model: states, measurements and transformations. Deutsch's algorithm (simplified).
• Mar 28 (M): Verification of time-critical reactive systems. Exercises in Uppaal.
• Abr 11 (M): Quantum algorithms (Morning lecture in the contex of the Quantum Days 2019).
• Abr 11 (T): Hands-on session in Qiskit (Afternoon lecture in the contex of the Quantum Days 2019).
• May 2 (T): Quantum Algorithms: Deutsch-Joza; Grover.
• May 13 (M - extra): Modal and temporal logics for processes. Bisimulation and modal equivalence. The Hennesy-Milner theorem. Modalities index by regular expressions. Introduction to the modal MU-calculus..
• May 23 (M - Short course by Prof Farhad Arbab): Interaction based design and exogeneous software coordination. The Reo coordination language.
• May 23 (T - Short course by Prof Farhad Arbab): Semantics models for Reo: constraint automata and the colour model. Reo tools. Discussion of modelling examples.

Support

Slides

• Software architecture for reactive systems
• Introduction to transition systems and process algebra ----- Examples (mcrl2): (1) (2)
• Bisimilarity
• Modelling time-critical reactive systems
• Verification of time-critical reactive systems in Uppaal
• Introduction to quantum computation
• Quantum processes: The computational model
• Quantum processes: Algorithms
• Modal Logic for processes
• Interaction-centric design with Reo (by Farhad Arbab)

Exercises

• Background, LTS, Process Algebra.
• Verification of time-critical models in Uppaal (demo in zip file)
• Practical Assigmnent

Links

• Arca website
• mCRL2 website
• Reo project
• Reo animations
• IBM Quantum Experience

Bibliography

• Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. CUP, 2007.
• Jan Friso Groote, Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2008.
• Johan van Benthem Modal Logic for Open Minds
  , CSLI, 2010.
• Patrick Blackburn, Maarten de Rijke, Yde Venema. Modal Logic. CUP, 2014.
• Christel Baier, Joost-Pieter Katoen. Principles Of Model Checking. MIT Press, 2008
• Noson Yanofsky, Mirco Mannucci. Quantum Computing for Computer Scientists. CUP, 2008.

Pragmatics

Assessment

• Test (80%) - 6 June 2019 @ 9h
• Project-exercises (20%) - 6 June 2019 23.59h (AoE)
• Marks (6 June 2019) Here!
• Final Marks (1 July 2019) available Here!
• Final Marks (Época Especial) available Here!

Test and Exams

• Test
• Exam

Contact

• Appointments: Wed, 9-11 (please send an email the day before)
• Email: lsb at di dot uminho dot pt
• Last update: 2019.07.25

Lecturer