MSc: Models Software Systems.previous version

Models of Software Systems

• Course name: Models of Software Systems
• Course number: 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

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
• Propositional Logic
• First Order Logic
• Formal Systems

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:

• INTRODUCTION to SET THEORY - DISCRETE MATHEMATICS
• INTRODUCTION to PROPOSITIONAL LOGIC - DISCRETE MATHEMATICS
• (Logic) Predicate Logic
• What is Formal Verification?

It can be an advantage to read introductory chapters of the book: M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press (2004)

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

• 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

What should a student be able to understand at the end of the course?

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
• Explain Strengths and weaknesses of specific models and logics
• Explain State machines and temporal logics
• Abstract formal models for certain classes of systems

What should a student be able to apply at the end of the course?

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

• 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

Course evaluation

Course grade breakdown

		Proposed points
Labs/seminar classes	20	40
Interim performance assessment	30	30
Exams	50	30

If necessary, please indicate freely your course’s features in terms of students’ performance assessment: None

Grades range

Course grading range

		Proposed range
A. Excellent	90-100	80-100
B. Good	75-89	65-79
C. Satisfactory	60-74	50-64
D. Poor	0-59	0-49

If necessary, please indicate freely your course’s grading features: The semester starts with the default range as proposed in the Table 1, but it may change slightly (usually reduced) depending on how the semester progresses.

Resources and reference material

• Handouts supplied by the instructor

Course Sections

The main sections of the course and approximate hour distribution between them is as follows:

Course Sections

Section	Section Title	Teaching Hours
1	Mathematical Foundations	12
2	Concepts of computation and software	8
3	Formal Modelling	32

Section title:

Mathematical Foundations

Topics covered in this section:

• Propositional & Predicate Logic
• Sets, Relations, Functions

What forms of evaluation were used to test students’ performance in this section?

|a|c| & Yes/No
Development of individual parts of software product code & 0
Homework and group projects & 1
Midterm evaluation & 1
Testing (written or computer based) & 1
Reports & 1
Essays & 0
Oral polls & 0
Discussions & 1

Typical questions for ongoing performance evaluation within this section

1. What is a formal system? What is a rewriting system?
2. What is the difference between propositional and predicate logic?
3. What is a predicate? What is a connective?
4. What is a quantifier? Existential? Universal?
5. Given a specific formula define the truth table?
6. Check if a specific formula is a tautology or a contradiction.
7. State the difference between relation and function
8. Computing the intersection or union of two sets
9. What are De Morgan Laws? Example of applications.
10. Operators of set theory.

Typical questions for seminar classes (labs) within this section

1. Check if given formulas are well-formed. For those that are not briefly explain why.
2. Prove that a given statement is a theorem in a given formal system.
3. Augment a given formal system so that given statements become theorems in that formal system.
4. Construct a truth table for given propositions.
5. For given satisfiable propositions, provide z3 code that proves their satisfiability.
6. Translate given predicates into English sentences using the provided translation key.
7. Translate given sentences into predicate logic, using the translation key provided.
8. Identify theorems among given propositional statements using z3.
9. Provide a linear/tree proof of a statement identified as a theorem.
10. Prove in Isabelle proof assistant a statement identified as a theorem.

Test questions for final assessment in this section

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 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?

|a|c| & Yes/No
Development of individual parts of software product code & 0
Homework and group projects & 1
Midterm evaluation & 1
Testing (written or computer based) & 1
Reports & 1
Essays & 0
Oral polls & 0
Discussions & 1

Typical questions for ongoing performance evaluation within this section

1. What is a state machine and how it is formally defined?
2. What is s state, initial state, final state?
3. What is the language accepted by a machine?
4. Design a state machine for some specific purpose
5. Verify that a state machine performs a given goal
6. How does a proof system work?
7. What is natural deduction and for what it is used?
8. What is an inference rule?
9. Prove specific theorems in natural deduction
10. What are preconditions and postconditons?

Typical questions for seminar classes (labs) within this section

1. Give a 4-tuple description of a state machine.
2. What are the reachable states of a state machine?
3. Implement a state machine in the LTSA tool; provide your code.
4. Does a state machine have any progress or safety violations? Provide the corresponding output from LTSA. .
5. Given a UML class diagram, annotate its classes with class invariants in OCL.
6. Given a UML class diagram, annotate its methods with preconditions in OCL.
7. Given a UML class diagram, annotate its methods with postconditions in OCL.

Test questions for final assessment in this section

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 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?

|a|c| & Yes/No
Development of individual parts of software product code & 1
Homework and group projects & 1
Midterm evaluation & 0
Testing (written or computer based) & 1
Reports & 1
Essays & 1
Oral polls & 0
Discussions & 1

Typical questions for ongoing performance evaluation within this section

1. What are the UML diagrams and what is their purpose?
2. What is OCL and what is its purpose?
3. What is Z and what is its purpose?
4. What is Design-by-contract and what is its purpose?
5. Design UML Use Cases diagrams for some given system
6. Design UML Class Diagrams for some given system
7. Define OCL constraints for some parts of some given system
8. Specify system requirements for a given system in Z
9. Use temporal logic and model checkers to specify and verify system properties
10. Use Design-by-contract and Autoproof to specify and verify system properties

Typical questions for seminar classes (labs) within this section

1. Specify a state space in Z.
2. Specify initial states of a state space in Z.
3. Specify CRUD operations of a state space in Z.
4. Define a robust version of a Z specification.
5. Provide an Alloy specification of a state space.
6. Enrich an Alloy specification with axioms.
7. Implement CRUD operations on an Alloy specification of a state space.
8. Specify an assertion that you want to hold on an Alloy specification.
9. Check an assertion in an Alloy specification using Alloy analyzer; correct the specification if the assertion does not hold.

Test questions for final assessment in this section

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