Objectives

This course teaches the basic principles of Model-Driven Engineering - MDE. Students should learn:

1. The fundamental concepts of MDE, its role in a critical system’s development and safety assessment processes, and the importance of having precise models in this context.
2. How to identify and write functional and non-functional requirements for critical systems, using the best practices and ensuring that they respect the expected quality standards (verifiable, traceable, unambiguous, correct, etc.)
3. Formal models capable of precisely capturing different aspects of UML diagrams, such as labelled transition systems and different logical systems.
4. Understand domain specific standards common in critical systems’ development, and apply them when using an MDE approach; and
5. How to use tools that support requirement specification and management, system modelling and its safety assessment, and the formal models described.

Syllabus

• High-level overview or requirements and associated processes
• Mathematical Preliminaries
  • Basic mathematical notations
  • Set theory
  • PropositionalLogic
    • Syntax, semantics, and reasoning
  • First Order Logic
    • Syntax, semantics, and reasoning

• Behavioural modelling
  • Single component
    • State diagrams and Flow charts
    • Formal modelling: Automata, Process Algebra
  • Many components
    • Communication diagrams and Sequence diagrams
    • Formal modelling: Process algebra with interactions
  • Equivalences
    • (Bi)similarity
    • Realisability
  • Verification
    • Verification of requirements
    • Formal modelling: modal logics
    • Tools: model checking with mCRL2
• Requirement specification using natural language
  • The Easy Approach to Requirements Specification (EARS)
  • The Doorstop tool to manage and document requirements
• An introduction to automatic theorem provers
  • Support for the consistency and correctness of formalized requirements

Material

Slides

• Introduction to MDE and Requirement engineering I (Lecture 1)
• Introduction to MDE and Requirement engineering II (Lecture 1)
• Propositional Logic (Lecture 2)
• Propositional Logic - exercises (Lecture 3)
• First Order Logic (Lecture 4)
• Natural deduction (Lecture 5)
• Natural deduction - exercises (Lecture 6)
• Modelling behaviour: Automata and Process Algebra (Lecture 7)
• Analysing behaviour: Equivalence of systems; Realisability (Lecture 8)
• Logics for behaviour: Modal logics; Model-Checking (Lecture 9)
• Modelling and verification in mCRL2 (Lecture 10)
• Textual requirements: EARS and Doorstop (Lecture 11)

Exercises and Assignments

• Exercises on Logic (individual)
  • Compilation of logic rules
• A1: Modelling Behaviour (group)
• A2: Analysing Behaviour (group)
• A3: Requirement analysis (group)

Useful links

• mCRL2

Bibliography

• Reactive Systems: Modelling, Specification and Verification (2007), by Luca Aceto et al.

• Modeling and Analysis of Communicating Systems (2014), by Jan Friso Groote and Mohammad Reza Mousavi

Pragmatics

Evaluation

• Final mark = Homework (10%) + Individual Exercises (10%) + Assignments (80%)

Homework consists of exercises presented in the slides, partially done during the lessons, that should be submitted as a PDF file per week until the end of the following week. Marks reflect mainly the effort, i.e., bad resolutions are better than no resolutions.

Individual Exercises are to be developed individually, and submitted as a single PDF report, covering mainly logic deduction. Feedback will be given online on request, and marked at the end of the unit.

Assignments (3 in total) are to be developed by teams of 3-4 students. Each team has a dedicated git repository that will contain the software artefacts and a report for each assignment. Feedback will be provided within 2 weeks after each submission deadline, and marked only at the end of the unit.

Deadlines

Homework consists of a PDF report that must be submitted until Sunday @ 23:59 of the following week of being shown during lessons. For example, all exercises presented in the slides used in the week 8 Nov - 12 Nov must be submitted until Sunday 21 Nov. Exercises and Assignments have specific deadlines, mentioned on their instructions. The deadlines are summarised below, and may still suffer changes.

• 28 Nov (Sun) @ 23:59 - Slides of Lecture 7 (pages 1-25)
• 28 Nov (Sun) @ 23:59 - Logic exercises
• 5 Dec (Sun)@ 23:59 - Slides of Lecture 7 (26-end) & Lecture 8 (1-10)
• 12 Dec (Sun)@ 23:59 - Slides of Lecture 8 (11-37)
• 12 Dec (Sun)@ 23:59 - Modelling assignment
• 19 Dec (Sun)@ 23:59 - Slides of Lecture 9 (1-29)
• 9 Jan (Sun)@ 23:59 - Behaviour assignment
• 9 Jan (Sun)@ 23:59 - Requirements assignment

Lecturers

• David Pereira, drp arroba isep ponto ipp ponto pt
• José Proença, pro arroba isep ponto ipp ponto pt
• Eduardo Tovar, emt arroba isep ponto ipp ponto pt

We will use a team in Microsoft Teams where all questions regarding this course unit should be placed, and where we can schedule virtual meetings if needed.