CloseHelpPrint
Kies de Nederlandse taal
Course module: 201700084
201700084
Software Science
Course info
Course module201700084
Credits (ECTS)5
Course typeCourse
Language of instructionEnglish
Contact personprof.dr. M. Huisman
E-mailm.huisman@utwente.nl
Lecturer(s)
Lecturer
prof.dr. M. Huisman
Contactperson for the course
prof.dr. M. Huisman
Lecturer
prof.dr. J.C. van de Pol
Lecturer
prof.dr.ir. A. Rensink
Lecturer
dr. M.I.A. Stoelinga
Academic year2017
Starting block
2A/  2B
Application procedureYou apply via OSIRIS Student
Registration using OSIRISYes
Learning goals
Q3, Topic 1: Graph-transformation (Arend Rensink)

The student acquires:
  • Knowledge and understanding of the basic concepts of graph transformation
  • Insight in the use of graph transformation for modelling and verification in general
  • Skill in applying graph transformation for the construction and manipulation of syntax graphs and heap graphs
 
Q3, Topic 2: Quantitative Risk Analysis (Mariëlle Stoelinga)
After passing this class, the student is able to
  • Explain the basic concepts of risk management
  • Identify and model system risks via fault trees and FMECAs
  • Quantify risks via appropriate metrics, e.g, risk priority number, reliability, availability
  • Devise appropriate counter measures to reduce the system risks, and study the effect of counter measures on the risk metrics
 
Q4, Topic 1: Verification of Concurrent Software (Marieke Huisman)

The student acquires:
  • Knowledge about the use of program logics to reason about the behaviour of sequential and concurrent software
  • Understanding how tool support for the use of program logics can be developed
  • Practical experience with program verification using program logics
 Q4, Topic 2: Multi-core model checking (Jaco van de Pol)

The student acquires:
  • Knowledge about various model checking algorithms, in particular explicit and symbolic algorithms for CTL and LTL model checking
  • Knowledge about parallel implementations of model checking algorithms, in particular for multi-core shared memory systems
  • Practical skills to implement and experiment with parallel model checking  algorithms.
  • Understanding of the experimental tradeoffs between efficient algorithms and  parallel scalability
Content
Software is everywhere, and our society is depending more and more on software working reliably and efficiently. To make it more reliable and efficient, we need to have a thorough understanding of the behavior of software systems, and how we can analyse and improve this behavior. This course gives insights in current research directions in the area of software systems, and how these new ideas can be used to improve software.
 
The goal of the course Software Science is to teach several topics related to active, on-going research in software engineering and formal methods. Each edition of the course consists of two topics of roughly 4 weeks each. Each topic consists of four lectures, complemented with exercise or lab sessions to gain practical experiences with the material introduced during the lectures. Each topic is finished with an individual homework assignment. The homework assignment is assessed by the topic teacher, and the final grade of the course is the average of the two topic grades.
If one is interested in more than two topics, it is possible to follow the course a second time choosing two different topics. In this way, one can study 4 topics for 10 ECTS.
 
The list of projects and topics will be revised every year. In the course year 2017/2018, we plan to teach the following topics:
  • Q3, Topic 1: Graph-transformation (Arend Rensink)
  • Q3, Topic 2: Quantitative Risk Analysis (Mariëlle Stoelinga)
  • Q4, Topic 1: Verification of concurrent software (Marieke Huisman)
  • Q4, Topic 2: Multi-core model checking (Jaco van de Pol)
 
Q3, Topic 1: Graph-transformation (Arend Rensink)

 
Graph transformation is a very widely applicable modelling paradigm, which here is used to capture the syntax and semantics of programming languages. This involves recognising that both the syntactic structure of a program itself and its effect in terms of what happens during execution can be represented by graphs. Graph transformation rules can then be defined to manipulate these graphs in a deterministic fashion reflecting what happens during parsing and execution of a program.
In this part of the course, we explain the basic concepts of graph transformation and how they can be applied in the way described above. This is supported by a tool called GROOVE (which stands for “GRaphs for Object-Oriented VErification”) in which you can try out everything you have learned and develop rule systems yourself.

 
Q3, Topic 2: Quantitative Risk Analysis (Mariëlle Stoelinga)

 
How do we ensure that robots, drones, Internet of Things devices, and medical systems function correctly? That is the role of risk management: identify the main system risks, assess their impact, and take appropriate counter measures. This class discusses two common methods for quantitative risk analysis, namely fault tree analysis (FMTA) and failure mode, effect and criticality analysis (FMECA), as well as their underlying techniques.

 
Q4, Topic 1: Verification of Concurrent Software (Marieke Huisman)

 
We introduce the notion of program logic to verify software. Traditionally, program logics are used to reason about sequential software. Recently, extensions have been proposed to reason about concurrent software. We introduce the various logics, and discuss in particular permission-based separation logic. We show how this logic is suitable to reason about concurrent software using different concurrency paradigms. We also discuss how use of the program logic can be supported by a tool. The homework assignment will ask the student to use program logics to verify some concurrent programs yourself.

 
Q4, Topic 2: Multi-core model checking (Jaco van de Pol)

 
First, we introduce the basic algorithms for model checking properties of concurrent systems. In particular, we will treat explicit and symbolic graph algorithms for LTL and CTL properties. These algorithms are combinations of Depth-First Search and Breadth-First Search. Next, we study the concurrent datastructures and parallel algorithms that are needed for a high-performance implementation of these graph algorithms. The goal is to understand how the choice for a particular datastructure or algorithm influences the efficiency and parallel scalability of the model checking problem. The practical assignment evolves around the application of the LTSmin toolset to international model-checking benchmarks and competitions.
 
Assumed previous knowledge
-
Required materials
-
Recommended materials
Course material
Papers will be provided via Blackboard
Instructional modes
Lecture

Project unsupervised

Tutorial

Tests
Test

CloseHelpPrint
Kies de Nederlandse taal