MSc: Models Software Systems

From IU
(Redirected from MSc:Models Software Systems)
Jump to navigation Jump to search

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