Full course description

Course Date:

Sep 12 - Oct 24, 2016

Duration:

6 weeks

Commitment:

3 hrs/week

Requirement:

None

Course Type:

Instructor-led

Credential:

Badge

Description

Anyone who has ever designed an embedded system or a communication protocol involving several components executing simultaneously knows that such software is inherently susceptible to bugs. Typical problems include race conditions, deadlocks, and unexpected interplay between different components. The parallel nature of these systems makes it notoriously hard to detect such bugs using testing (timing, e.g., plays a crucial role). This course is designed to provide an introduction to the problems that arise in the design of such systems. It provides ways to model such systems and reason about them.

Objectives

The purpose of this course is to learn how to specify the behavior of embedded systems, and to experience the design of a provably correct system. In this course you will learn how to formally specify requirements, and to prove or disprove them on the behavior. You will experience how to apply the techniques in practice in a practical assignment.

Course Instructors

Mohammad Mousavi

Mohammad Mousavi

Professor

Mohammad Mousavi is a professor of Computer Systems Engineering at Halmstad University. He received his Ph.D. in Computer Science in 2005 from TU Eindhoven. Since then, he has been postdoctoral researcher at Reykjavik University, and assistant and associate professor at TU Eindhoven, He specializes in model-based testing and verification. He is the co-author of more than 100 chapters and scientific papers and a book on "Modeling and Analysis of Communicating Systems."

Jeroen Keiren

Jeroen Keiren

Professor

Dr. Jeroen Keiren is assistant professor for Software Engineering at the Faculty of Management, Science and Technology of the Open University of the Netherlands (OUNL). He is also affiliated with the Radboud University in Nijmegen as a member of the Digital Security department of the Institute for Computing and Information Sciences. Keiren obtained his PhD from Eindhoven University of Technology in 2013. He has experience in formal methods and software verification research, in particular model checking. He is also experienced in applying model checking tools in an industrial context, for example in verifying the configuration phase of the IEEE 11073-20601 protocol for medical devices, and the analysis of the detector controls software of the CMS detector in the large hadron collider (LHC) at CERN.