Difference between revisions of "MSc: Models Software Systems"

From IU
Jump to navigation Jump to search
 
Line 1: Line 1:
  +
 
= Models of Software Systems =
  
= Models of Software Systems =
  +
* '''Course name''': Models of Software Systems
  +
* '''Code discipline''': SE-07
  +
* '''Subject area''':
   
  +
== Short Description ==
−
* <span>'''Course name:'''</span> Models of Software Systems
  
  +
This course covers the following concepts: Formal Models; Software Specification; Software Verification.
−
* <span>'''Course number:'''</span> SE-07
  
−  
−
== Course characteristics ==
  
−  
−
=== Key concepts of the class ===
  
−  
−
* Formal Models
  
−
* Software Specification
  
−
* Software Verification
  
−  
−
=== What is the purpose of this course? ===
  
−  
−
Formal models and formal methods are gaining an increasing importance today - in academia and in industry - in particular due to the emerging of tool support used for modeling and analysis of systems. An important question is asked world-wide when developing academic curricula: what a software engineer should know about formal modeling? On what specific aspect a course should focus and help the perspective engineer to navigate such a complex and fast changing field? The course attempt to give a partial although consistent answer to this question by providing an introduction to the foundations and uses of formal modeling. The course can be seen as organized in three parts: the first part sets out the mathematical foundations on which the rest of the course is based. It presents the mathematical concepts, such as logics, proofs, theories, sets, functions, relations, etc., on which all modern modeling approaches build. The second part presents the concepts that allow to relate mathematics to computation and to software: state machines, invariants, pre- and post-conditions, proving properties about programs. The third part consists of particular notations and method of formal modeling showing how the general concepts of the second part can be turned into effective engineering tools.
  
   
 
== Prerequisites ==
  
== Prerequisites ==
   
  +
=== Prerequisite subjects ===
−
The course has been designed to be self-included as much as possible. However, it has a strong formal flavour for which it can be very useful to have a general understanding of the following topics:
  
 
* Set theory
  
* Set theory
 
* Propositional Logic
  
* Propositional Logic
 
* First Order Logic
  
* First Order Logic
 
* Formal Systems
  
* Formal Systems
  +
* INTRODUCTION to SET THEORY - DISCRETE MATHEMATICS
  +
* INTRODUCTION to PROPOSITIONAL LOGIC - DISCRETE MATHEMATICS
  +
* (Logic) Predicate Logic
  +
* What is Formal Verification?
   
  +
=== Prerequisite topics ===
−
Recommendations for students on how to succeed in the course:
  
   
−
I suggest here some simple video material that can help a smooth introduction with the course:
  
−
* [https://www.youtube.com/watch?v=tyDKR4FG3Yw INTRODUCTION to SET THEORY - DISCRETE MATHEMATICS]
  
−
* [https://www.youtube.com/watch?v=itrXYg41-V0 INTRODUCTION to PROPOSITIONAL LOGIC - DISCRETE MATHEMATICS]
  
−
* [https://www.youtube.com/watch?v=h5UTvdcgFHw (Logic) Predicate Logic]
  
−
* [https://www.youtube.com/watch?v=-CTNS2D-kbY What is Formal Verification?]
  
   
  +
== Course Topics ==
−
It can be an advantage to read introductory chapters of the book:
  
  +
{| class="wikitable"
−
M. Huth and M. Ryan. [https://books.google.ru/books/about/Logic_in_Computer_Science.html?id=sVLOaObSBHkC&redir_esc=y Logic in Computer Science: Modelling and Reasoning About Systems]. Cambridge University Press (2004)
  
  +
|+ Course Sections and Topics
  +
|-
  +
! Section !! Topics within the section
  +
|-
  +
| Mathematical Foundations ||
  +
# Propositional & Predicate Logic
  +
# Sets, Relations, Functions
  +
|-
  +
| Concepts of computation and software ||
  +
# Proof Techniques, Induction
  +
# State Machines
  +
|-
  +
| Formal Modelling ||
  +
# UML
  +
# Z/B/Event-B
  +
# Model Checking
  +
# Linear Temporal Logic
  +
# Concurrency
  +
# Petri Nets
  +
# Alloy
  +
# Process Algebra
  +
# CSP
  +
# Autoproof
  +
|}
  +
== Intended Learning Outcomes (ILOs) ==
   
  +
=== What is the main purpose of this course? ===
  +
Formal models and formal methods are gaining an increasing importance today - in academia and in industry - in particular due to the emerging of tool support used for modeling and analysis of systems. An important question is asked world-wide when developing academic curricula: what a software engineer should know about formal modeling? On what specific aspect a course should focus and help the perspective engineer to navigate such a complex and fast changing field? The course attempt to give a partial although consistent answer to this question by providing an introduction to the foundations and uses of formal modeling. The course can be seen as organized in three parts: the first part sets out the mathematical foundations on which the rest of the course is based. It presents the mathematical concepts, such as logics, proofs, theories, sets, functions, relations, etc., on which all modern modeling approaches build. The second part presents the concepts that allow to relate mathematics to computation and to software: state machines, invariants, pre- and post-conditions, proving properties about programs. The third part consists of particular notations and method of formal modeling showing how the general concepts of the second part can be turned into effective engineering tools.
   
  +
=== ILOs defined at three levels ===
−
== Course Objectives Based on Bloom’s Taxonomy ==
  
−  
−
=== What should a student remember at the end of the course? ===
  
−  
−
By the end of the course, the students should be able to recognize and define
  
   
  +
==== Level 1: What concepts should a student know/remember/explain? ====
  +
By the end of the course, the students should be able to ...
 
* Define mathematical notions behind software specification and verification
  
* Define mathematical notions behind software specification and verification
 
* List different specification methods
  
* List different specification methods
Line 48: Line 64:
 
* List Popular verification tools
  
* List Popular verification tools
   
−
=== What should a student be able to understand at the end of the course? ===
 +
==== Level 2: What basic practical skills should a student be able to perform? ====
  +
By the end of the course, the students should be able to ...
−  
−
By the end of the course, the students should be able to describe and explain (with examples)
  
−  
 
* Describe the basic mathematical machinery and how can be applied to improve software development and software quality
  
* Describe the basic mathematical machinery and how can be applied to improve software development and software quality
 
* Explain Strengths and weaknesses of specific models and logics
  
* Explain Strengths and weaknesses of specific models and logics
Line 57: Line 71:
 
* Abstract formal models for certain classes of systems
  
* Abstract formal models for certain classes of systems
   
−
=== What should a student be able to apply at the end of the course? ===
 +
==== Level 3: What complex comprehensive skills should a student be able to apply in real-life scenarios? ====
  +
By the end of the course, the students should be able to ...
−  
−
By the end of the course, the students should be able to apply
  
−  
 
* Formally modelling a system
  
* Formally modelling a system
 
* Reasoning about system properties
  
* Reasoning about system properties
 
* Specifying a system in Z
  
* Specifying a system in Z
 
* Coding in languages like PROMELA for model checking
  
* Coding in languages like PROMELA for model checking
−
* Using SPIN model checker
 +
* Using SPIN model checker
  +
== Grading ==
   
−
=== Course evaluation ===
 +
=== Course grading range ===
  +
{| class="wikitable"
−  
−
{|
 +
|+
−
|+ Course grade breakdown
  
−
!
  
−
!
  
−
!align="center"| '''Proposed points'''
  
 
|-
  
|-
  +
! Grade !! Range !! Description of performance
−
| Labs/seminar classes
  
−
| 20
  
−
|align="center"| 40
  
 
|-
  
|-
  +
| A. Excellent || 80-100 || -
−
| Interim performance assessment
  
−
| 30
  
−
|align="center"| 30
  
 
|-
  
|-
  +
| B. Good || 65-79 || -
−
| Exams
  
−
| 50
 +
|-
  +
| C. Satisfactory || 50-64 || -
−
|align="center"| 30
  
  +
|-
  +
| D. Poor || 0-49 || -
 
|}
  
|}
   
  +
=== Course activities and grading breakdown ===
−
If necessary, please indicate freely your course’s features in terms of students’ performance assessment: None
  
  +
{| class="wikitable"
−  
  +
|+
−
=== Grades range ===
  
−  
−
<div id="tab:ModelsCourseGradingRange">
  
−  
−
{|
  
−
|+ Course grading range
  
−
!
  
−
!
  
−
!align="center"| '''Proposed range'''
  
 
|-
  
|-
  +
! Activity Type !! Percentage of the overall course grade
−
| A. Excellent
  
−
| 90-100
  
−
|align="center"| 80-100
  
 
|-
  
|-
  +
| Labs/seminar classes || 40
−
| B. Good
  
−
| 75-89
  
−
|align="center"| 65-79
  
 
|-
  
|-
  +
| Interim performance assessment || 30
−
| C. Satisfactory
  
−
| 60-74
  
−
|align="center"| 50-64
  
 
|-
  
|-
−
| D. Poor
 +
| Exams || 30
−
| 0-59
  
−
|align="center"| 0-49
  
 
|}
  
|}
   
  +
=== Recommendations for students on how to succeed in the course ===
   
−
</div>
  
−
If necessary, please indicate freely your course’s grading features: The semester starts with the default range as proposed in the Table [[#tab:ModelsCourseGradingRange|1]], but it may change slightly (usually reduced) depending on how the semester progresses.
  
   
−
=== Resources and reference material ===
 +
== Resources, literature and reference materials ==
   
  +
=== Open access resources ===
 
* Handouts supplied by the instructor
  
* Handouts supplied by the instructor
−
*
 
−
*
 
−
*
 
−
*
 
−
*
 
−
*
  
   
−
== Course Sections ==
 +
=== Closed access resources ===
   
−
The main sections of the course and approximate hour distribution between them is as follows:
  
   
  +
=== Software and tools used within the course ===
−
{|
  
  +
−
|+ Course Sections
  
  +
= Teaching Methodology: Methods, techniques, & activities =
−
!align="center"| '''Section'''
  
  +
−
! '''Section Title'''
  
−
!align="center"| '''Teaching Hours'''
 +
== Activities and Teaching Methods ==
  +
{| class="wikitable"
  +
|+ Activities within each section
 
|-
  
|-
  +
! Learning Activities !! Section 1 !! Section 2 !! Section 3
−
|align="center"| 1
  
−
| Mathematical Foundations
  
−
|align="center"| 12
  
 
|-
  
|-
  +
| Homework and group projects || 1 || 1 || 1
−
|align="center"| 2
  
−
| Concepts of computation and software
  
−
|align="center"| 8
  
 
|-
  
|-
  +
| Midterm evaluation || 1 || 1 || 0
−
|align="center"| 3
  
  +
|-
−
| Formal Modelling
  
  +
| Testing (written or computer based) || 1 || 1 || 1
−
|align="center"| 32
  
−
|}
 +
|-
  +
| Reports || 1 || 1 || 1
  +
|-
  +
| Discussions || 1 || 1 || 1
  +
|-
  +
| Development of individual parts of software product code || 0 || 0 || 1
  +
|-
  +
| Essays || 0 || 0 || 1
  +
|}
  +
== Formative Assessment and Course Activities ==
   
−
=== Section 1 ===
 +
=== Ongoing performance assessment ===
−  
−
=== Section title: ===
  
−  
−
Mathematical Foundations
  
−  
−
=== Topics covered in this section: ===
  
−  
−
* Propositional &amp; Predicate Logic
  
−
* Sets, Relations, Functions
  
−  
−
=== What forms of evaluation were used to test students’ performance in this section? ===
  
−  
−
<div class="tabular">
  
−  
−
<span>|a|c|</span> &amp; '''Yes/No'''<br />
  
−
Development of individual parts of software product code &amp; 0<br />
  
−
Homework and group projects &amp; 1<br />
  
−
Midterm evaluation &amp; 1<br />
  
−
Testing (written or computer based) &amp; 1<br />
  
−
Reports &amp; 1<br />
  
−
Essays &amp; 0<br />
  
−
Oral polls &amp; 0<br />
  
−
Discussions &amp; 1<br />
  
−  
−  
−  
−
</div>
  
−
=== Typical questions for ongoing performance evaluation within this section ===
  
−  
−
# What is a formal system? What is a rewriting system?
  
−
# What is the difference between propositional and predicate logic?
  
−
# What is a predicate? What is a connective?
  
−
# What is a quantifier? Existential? Universal?
  
−
# Given a specific formula define the truth table?
  
−
# Check if a specific formula is a tautology or a contradiction.
  
−
# State the difference between relation and function
  
−
# Computing the intersection or union of two sets
  
−
# What are De Morgan Laws? Example of applications.
  
−
# Operators of set theory.
  
−  
−
=== Typical questions for seminar classes (labs) within this section ===
  
−  
−
# Check if given formulas are well-formed. For those that are not briefly explain why.
  
−
# Prove that a given statement is a theorem in a given formal system.
  
−
# Augment a given formal system so that given statements become theorems in that formal system.
  
−
# Construct a truth table for given propositions.
  
−
# For given satisfiable propositions, provide z3 code that proves their satisfiability.
  
−
# Translate given predicates into English sentences using the provided translation key.
  
−
# Translate given sentences into predicate logic, using the translation key provided.
  
−
# Identify theorems among given propositional statements using z3.
  
−
# Provide a linear/tree proof of a statement identified as a theorem.
  
−
# Prove in Isabelle proof assistant a statement identified as a theorem.
  
−  
−
=== Test questions for final assessment in this section ===
  
   
  +
==== Section 1 ====
  +
{| class="wikitable"
  +
|+
  +
|-
  +
! Activity Type !! Content !! Is Graded?
  +
|-
  +
| Question || What is a formal system? What is a rewriting system? || 1
  +
|-
  +
| Question || What is the difference between propositional and predicate logic? || 1
  +
|-
  +
| Question || What is a predicate? What is a connective? || 1
  +
|-
  +
| Question || What is a quantifier? Existential? Universal? || 1
  +
|-
  +
| Question || Given a specific formula define the truth table? || 1
  +
|-
  +
| Question || Check if a specific formula is a tautology or a contradiction. || 1
  +
|-
  +
| Question || State the difference between relation and function || 1
  +
|-
  +
| Question || Computing the intersection or union of two sets || 1
  +
|-
  +
| Question || What are De Morgan Laws? Example of applications. || 1
  +
|-
  +
| Question || Operators of set theory. || 1
  +
|-
  +
| Question || Check if given formulas are well-formed. For those that are not briefly explain why. || 0
  +
|-
  +
| Question || Prove that a given statement is a theorem in a given formal system. || 0
  +
|-
  +
| Question || Augment a given formal system so that given statements become theorems in that formal system. || 0
  +
|-
  +
| Question || Construct a truth table for given propositions. || 0
  +
|-
  +
| Question || For given satisfiable propositions, provide z3 code that proves their satisfiability. || 0
  +
|-
  +
| Question || Translate given predicates into English sentences using the provided translation key. || 0
  +
|-
  +
| Question || Translate given sentences into predicate logic, using the translation key provided. || 0
  +
|-
  +
| Question || Identify theorems among given propositional statements using z3. || 0
  +
|-
  +
| Question || Provide a linear/tree proof of a statement identified as a theorem. || 0
  +
|-
  +
| Question || Prove in Isabelle proof assistant a statement identified as a theorem. || 0
  +
|}
  +
==== Section 2 ====
  +
{| class="wikitable"
  +
|+
  +
|-
  +
! Activity Type !! Content !! Is Graded?
  +
|-
  +
| Question || What is a state machine and how it is formally defined? || 1
  +
|-
  +
| Question || What is s state, initial state, final state? || 1
  +
|-
  +
| Question || What is the language accepted by a machine? || 1
  +
|-
  +
| Question || Design a state machine for some specific purpose || 1
  +
|-
  +
| Question || Verify that a state machine performs a given goal || 1
  +
|-
  +
| Question || How does a proof system work? || 1
  +
|-
  +
| Question || What is natural deduction and for what it is used? || 1
  +
|-
  +
| Question || What is an inference rule? || 1
  +
|-
  +
| Question || Prove specific theorems in natural deduction || 1
  +
|-
  +
| Question || What are preconditions and postconditons? || 1
  +
|-
  +
| Question || Give a 4-tuple description of a state machine. || 0
  +
|-
  +
| Question || What are the reachable states of a state machine? || 0
  +
|-
  +
| Question || Implement a state machine in the LTSA tool; provide your code. || 0
  +
|-
  +
| Question || Does a state machine have any progress or safety violations? Provide the corresponding output from LTSA. . || 0
  +
|-
  +
| Question || Given a UML class diagram, annotate its classes with class invariants in OCL. || 0
  +
|-
  +
| Question || Given a UML class diagram, annotate its methods with preconditions in OCL. || 0
  +
|-
  +
| Question || Given a UML class diagram, annotate its methods with postconditions in OCL. || 0
  +
|}
  +
==== Section 3 ====
  +
{| class="wikitable"
  +
|+
  +
|-
  +
! Activity Type !! Content !! Is Graded?
  +
|-
  +
| Question || What are the UML diagrams and what is their purpose? || 1
  +
|-
  +
| Question || What is OCL and what is its purpose? || 1
  +
|-
  +
| Question || What is Z and what is its purpose? || 1
  +
|-
  +
| Question || What is Design-by-contract and what is its purpose? || 1
  +
|-
  +
| Question || Design UML Use Cases diagrams for some given system || 1
  +
|-
  +
| Question || Design UML Class Diagrams for some given system || 1
  +
|-
  +
| Question || Define OCL constraints for some parts of some given system || 1
  +
|-
  +
| Question || Specify system requirements for a given system in Z || 1
  +
|-
  +
| Question || Use temporal logic and model checkers to specify and verify system properties || 1
  +
|-
  +
| Question || Use Design-by-contract and Autoproof to specify and verify system properties || 1
  +
|-
  +
| Question || Specify a state space in Z. || 0
  +
|-
  +
| Question || Specify initial states of a state space in Z. || 0
  +
|-
  +
| Question || Specify CRUD operations of a state space in Z. || 0
  +
|-
  +
| Question || Define a robust version of a Z specification. || 0
  +
|-
  +
| Question || Provide an Alloy specification of a state space. || 0
  +
|-
  +
| Question || Enrich an Alloy specification with axioms. || 0
  +
|-
  +
| Question || Implement CRUD operations on an Alloy specification of a state space. || 0
  +
|-
  +
| Question || Specify an assertion that you want to hold on an Alloy specification. || 0
  +
|-
  +
| Question || Check an assertion in an Alloy specification using Alloy analyzer; correct the specification if the assertion does not hold. || 0
  +
|}
  +
=== Final assessment ===
  +
'''Section 1'''
 
# Given a set of different formulas define truth tables
  
# Given a set of different formulas define truth tables
 
# Given a set of different formulas define those that are tautology and/or contradiction
  
# Given a set of different formulas define those that are tautology and/or contradiction
Line 215: Line 284:
 
# Determining satisfiability of a formula
  
# Determining satisfiability of a formula
 
# Model natural language as propositional or predicate logic formulas
  
# Model natural language as propositional or predicate logic formulas
  +
'''Section 2'''
−  
−
=== Section 2 ===
  
−  
−
=== Section title: ===
  
−  
−
Concepts of computation and software
  
−  
−
=== Topics covered in this section: ===
  
−  
−
* Proof Techniques, Induction
  
−
* State Machines
  
−  
−
=== What forms of evaluation were used to test students’ performance in this section? ===
  
−  
−
<div class="tabular">
  
−  
−
<span>|a|c|</span> &amp; '''Yes/No'''<br />
  
−
Development of individual parts of software product code &amp; 0<br />
  
−
Homework and group projects &amp; 1<br />
  
−
Midterm evaluation &amp; 1<br />
  
−
Testing (written or computer based) &amp; 1<br />
  
−
Reports &amp; 1<br />
  
−
Essays &amp; 0<br />
  
−
Oral polls &amp; 0<br />
  
−
Discussions &amp; 1<br />
  
−  
−  
−  
−
</div>
  
−
=== Typical questions for ongoing performance evaluation within this section ===
  
−  
−
# What is a state machine and how it is formally defined?
  
−
# What is s state, initial state, final state?
  
−
# What is the language accepted by a machine?
  
−
# Design a state machine for some specific purpose
  
−
# Verify that a state machine performs a given goal
  
−
# How does a proof system work?
  
−
# What is natural deduction and for what it is used?
  
−
# What is an inference rule?
  
−
# Prove specific theorems in natural deduction
  
−
# What are preconditions and postconditons?
  
−  
−
=== Typical questions for seminar classes (labs) within this section ===
  
−  
−
# Give a 4-tuple description of a state machine.
  
−
# What are the reachable states of a state machine?
  
−
# Implement a state machine in the LTSA tool; provide your code.
  
−
# Does a state machine have any progress or safety violations? Provide the corresponding output from LTSA. .
  
−
# Given a UML class diagram, annotate its classes with class invariants in OCL.
  
−
# Given a UML class diagram, annotate its methods with preconditions in OCL.
  
−
# Given a UML class diagram, annotate its methods with postconditions in OCL.
  
−  
−
=== Test questions for final assessment in this section ===
  
−  
 
# Prove theorems in natural deduction
  
# Prove theorems in natural deduction
 
# Design a state machine for some specific purpose
  
# Design a state machine for some specific purpose
 
# Verify that a state machine performs a given goal
  
# Verify that a state machine performs a given goal
 
# Determine the language recognized by a state machine
  
# Determine the language recognized by a state machine
  +
'''Section 3'''
−  
−
=== Section 3 ===
  
−  
−
=== Section title: ===
  
−  
−
Formal Modelling
  
−  
−
=== Topics covered in this section: ===
  
−  
−
* UML
  
−
* Z/B/Event-B
  
−
* Model Checking
  
−
* Linear Temporal Logic
  
−
* Concurrency
  
−
* Petri Nets
  
−
* Alloy
  
−
* Process Algebra
  
−
* CSP
  
−
* Autoproof
  
−  
−
=== What forms of evaluation were used to test students’ performance in this section? ===
  
−  
−
<div class="tabular">
  
−  
−
<span>|a|c|</span> &amp; '''Yes/No'''<br />
  
−
Development of individual parts of software product code &amp; 1<br />
  
−
Homework and group projects &amp; 1<br />
  
−
Midterm evaluation &amp; 0<br />
  
−
Testing (written or computer based) &amp; 1<br />
  
−
Reports &amp; 1<br />
  
−
Essays &amp; 1<br />
  
−
Oral polls &amp; 0<br />
  
−
Discussions &amp; 1<br />
  
−  
−  
−  
−
</div>
  
−
=== Typical questions for ongoing performance evaluation within this section ===
  
−  
−
# What are the UML diagrams and what is their purpose?
  
−
# What is OCL and what is its purpose?
  
−
# What is Z and what is its purpose?
  
−
# What is Design-by-contract and what is its purpose?
  
 
# Design UML Use Cases diagrams for some given system
  
# Design UML Use Cases diagrams for some given system
 
# Design UML Class Diagrams for some given system
  
# Design UML Class Diagrams for some given system
Line 323: Line 297:
 
# Use Design-by-contract and Autoproof to specify and verify system properties
  
# Use Design-by-contract and Autoproof to specify and verify system properties
   
  +
=== The retake exam ===
−
=== Typical questions for seminar classes (labs) within this section ===
  
  +
'''Section 1'''
   
  +
'''Section 2'''
−
# Specify a state space in Z.
  
−
# Specify initial states of a state space in Z.
  
−
# Specify CRUD operations of a state space in Z.
  
−
# Define a robust version of a Z specification.
  
−
# Provide an Alloy specification of a state space.
  
−
# Enrich an Alloy specification with axioms.
  
−
# Implement CRUD operations on an Alloy specification of a state space.
  
−
# Specify an assertion that you want to hold on an Alloy specification.
  
−
# Check an assertion in an Alloy specification using Alloy analyzer; correct the specification if the assertion does not hold.
  
   
  +
'''Section 3'''
−
=== Test questions for final assessment in this section ===
  
−  
−
# Design UML Use Cases diagrams for some given system
  
−
# Design UML Class Diagrams for some given system
  
−
# Define OCL constraints for some parts of some given system
  
−
# Specify system requirements for a given system in Z
  
−
# Use temporal logic and model checkers to specify and verify system properties
  
−
# Use Design-by-contract and Autoproof to specify and verify system properties
  

Latest revision as of 12:02, 29 August 2022

Models of Software Systems

  • Course name: Models of Software Systems
  • Code discipline: SE-07
  • Subject area:

Short Description

This course covers the following concepts: Formal Models; Software Specification; Software Verification.

Prerequisites

Prerequisite subjects

  • Set theory
  • Propositional Logic
  • First Order Logic
  • Formal Systems
  • INTRODUCTION to SET THEORY - DISCRETE MATHEMATICS
  • INTRODUCTION to PROPOSITIONAL LOGIC - DISCRETE MATHEMATICS
  • (Logic) Predicate Logic
  • What is Formal Verification?

Prerequisite topics

Course Topics

Course Sections and Topics
Section Topics within the section
Mathematical Foundations
  1. Propositional & Predicate Logic
  2. Sets, Relations, Functions
Concepts of computation and software
  1. Proof Techniques, Induction
  2. State Machines
Formal Modelling
  1. UML
  2. Z/B/Event-B
  3. Model Checking
  4. Linear Temporal Logic
  5. Concurrency
  6. Petri Nets
  7. Alloy
  8. Process Algebra
  9. CSP
  10. Autoproof

Intended Learning Outcomes (ILOs)

What is the main purpose of this course?

Formal models and formal methods are gaining an increasing importance today - in academia and in industry - in particular due to the emerging of tool support used for modeling and analysis of systems. An important question is asked world-wide when developing academic curricula: what a software engineer should know about formal modeling? On what specific aspect a course should focus and help the perspective engineer to navigate such a complex and fast changing field? The course attempt to give a partial although consistent answer to this question by providing an introduction to the foundations and uses of formal modeling. The course can be seen as organized in three parts: the first part sets out the mathematical foundations on which the rest of the course is based. It presents the mathematical concepts, such as logics, proofs, theories, sets, functions, relations, etc., on which all modern modeling approaches build. The second part presents the concepts that allow to relate mathematics to computation and to software: state machines, invariants, pre- and post-conditions, proving properties about programs. The third part consists of particular notations and method of formal modeling showing how the general concepts of the second part can be turned into effective engineering tools.

ILOs defined at three levels

Level 1: What concepts should a student know/remember/explain?

By the end of the course, the students should be able to ...

  • Define mathematical notions behind software specification and verification
  • List different specification methods
  • List different specification notations
  • Define concurrency and related concepts
  • List Popular verification tools

Level 2: What basic practical skills should a student be able to perform?

By the end of the course, the students should be able to ...

  • Describe the basic mathematical machinery and how can be applied to improve software development and software quality
  • Explain Strengths and weaknesses of specific models and logics
  • Explain State machines and temporal logics
  • Abstract formal models for certain classes of systems

Level 3: What complex comprehensive skills should a student be able to apply in real-life scenarios?

By the end of the course, the students should be able to ...

  • Formally modelling a system
  • Reasoning about system properties
  • Specifying a system in Z
  • Coding in languages like PROMELA for model checking
  • Using SPIN model checker

Grading

Course grading range

Grade Range Description of performance
A. Excellent 80-100 -
B. Good 65-79 -
C. Satisfactory 50-64 -
D. Poor 0-49 -

Course activities and grading breakdown

Activity Type Percentage of the overall course grade
Labs/seminar classes 40
Interim performance assessment 30
Exams 30

Recommendations for students on how to succeed in the course

Resources, literature and reference materials

Open access resources

  • Handouts supplied by the instructor

Closed access resources

Software and tools used within the course

Teaching Methodology: Methods, techniques, & activities

Activities and Teaching Methods

Activities within each section
Learning Activities Section 1 Section 2 Section 3
Homework and group projects 1 1 1
Midterm evaluation 1 1 0
Testing (written or computer based) 1 1 1
Reports 1 1 1
Discussions 1 1 1
Development of individual parts of software product code 0 0 1
Essays 0 0 1

Formative Assessment and Course Activities

Ongoing performance assessment

Section 1

Activity Type Content Is Graded?
Question What is a formal system? What is a rewriting system? 1
Question What is the difference between propositional and predicate logic? 1
Question What is a predicate? What is a connective? 1
Question What is a quantifier? Existential? Universal? 1
Question Given a specific formula define the truth table? 1
Question Check if a specific formula is a tautology or a contradiction. 1
Question State the difference between relation and function 1
Question Computing the intersection or union of two sets 1
Question What are De Morgan Laws? Example of applications. 1
Question Operators of set theory. 1
Question Check if given formulas are well-formed. For those that are not briefly explain why. 0
Question Prove that a given statement is a theorem in a given formal system. 0
Question Augment a given formal system so that given statements become theorems in that formal system. 0
Question Construct a truth table for given propositions. 0
Question For given satisfiable propositions, provide z3 code that proves their satisfiability. 0
Question Translate given predicates into English sentences using the provided translation key. 0
Question Translate given sentences into predicate logic, using the translation key provided. 0
Question Identify theorems among given propositional statements using z3. 0
Question Provide a linear/tree proof of a statement identified as a theorem. 0
Question Prove in Isabelle proof assistant a statement identified as a theorem. 0

Section 2

Activity Type Content Is Graded?
Question What is a state machine and how it is formally defined? 1
Question What is s state, initial state, final state? 1
Question What is the language accepted by a machine? 1
Question Design a state machine for some specific purpose 1
Question Verify that a state machine performs a given goal 1
Question How does a proof system work? 1
Question What is natural deduction and for what it is used? 1
Question What is an inference rule? 1
Question Prove specific theorems in natural deduction 1
Question What are preconditions and postconditons? 1
Question Give a 4-tuple description of a state machine. 0
Question What are the reachable states of a state machine? 0
Question Implement a state machine in the LTSA tool; provide your code. 0
Question Does a state machine have any progress or safety violations? Provide the corresponding output from LTSA. . 0
Question Given a UML class diagram, annotate its classes with class invariants in OCL. 0
Question Given a UML class diagram, annotate its methods with preconditions in OCL. 0
Question Given a UML class diagram, annotate its methods with postconditions in OCL. 0

Section 3

Activity Type Content Is Graded?
Question What are the UML diagrams and what is their purpose? 1
Question What is OCL and what is its purpose? 1
Question What is Z and what is its purpose? 1
Question What is Design-by-contract and what is its purpose? 1
Question Design UML Use Cases diagrams for some given system 1
Question Design UML Class Diagrams for some given system 1
Question Define OCL constraints for some parts of some given system 1
Question Specify system requirements for a given system in Z 1
Question Use temporal logic and model checkers to specify and verify system properties 1
Question Use Design-by-contract and Autoproof to specify and verify system properties 1
Question Specify a state space in Z. 0
Question Specify initial states of a state space in Z. 0
Question Specify CRUD operations of a state space in Z. 0
Question Define a robust version of a Z specification. 0
Question Provide an Alloy specification of a state space. 0
Question Enrich an Alloy specification with axioms. 0
Question Implement CRUD operations on an Alloy specification of a state space. 0
Question Specify an assertion that you want to hold on an Alloy specification. 0
Question Check an assertion in an Alloy specification using Alloy analyzer; correct the specification if the assertion does not hold. 0

Final assessment

Section 1

  1. Given a set of different formulas define truth tables
  2. Given a set of different formulas define those that are tautology and/or contradiction
  3. Compute operations over some specific instances of sets
  4. Determining satisfiability of a formula
  5. Model natural language as propositional or predicate logic formulas

Section 2

  1. Prove theorems in natural deduction
  2. Design a state machine for some specific purpose
  3. Verify that a state machine performs a given goal
  4. Determine the language recognized by a state machine

Section 3

  1. Design UML Use Cases diagrams for some given system
  2. Design UML Class Diagrams for some given system
  3. Define OCL constraints for some parts of some given system
  4. Specify system requirements for a given system in Z
  5. Use temporal logic and model checkers to specify and verify system properties
  6. Use Design-by-contract and Autoproof to specify and verify system properties

The retake exam

Section 1

Section 2

Section 3

Retrieved from "https://eduwiki.innopolis.university/index.php?title=MSc:_Models_Software_Systems&oldid=7479"