Formale Methoden im Software Engineering

Wintersemester 2014/2015

Prof. Dr. Joel Greenyer
Prof. Dr. Joel Greenyer
2V+1Ü
A 310
14.10.2014 - 14.10.2014
Dienstags, 16:00 - 17:30
wird bekannt gegeben

News

Jun 24, 2015

The second exam will be on Friday, September 18th, 11:00 - 12:30 in Room G325. QIS registration is open now until July 6th.

Jan 13, 2015

The exam will be on Wednesday, the 4th of March, 13:00 - 14:30 in Room E001

Oct 21, 2014

You need to join ur Google+ community.

Request to join: https://plus.google.com/communities/116163206527300925070

From now on, most announcements will only be posted there.

Lecture slides will still be available from this website.

Oct 15, 2014

The first hangout on air was not so successful. It seems that after 15 minutes my wifi connection stopped and so did the broadcast as well as the recording.

Next week, I'll check my network connection regularly or use a cable.

I sent the link to the (rather short) recording of the lecture to everyone via email/Stud.IP. Please write me an email if you didn't get any emails from me so far.

Oct 13, 2014

There was another error on this page: The lecture will be in room A310, not in A301.

Oct 13, 2014

For students not residing in Hanover (e.g. ITIS students from Braunschweig, Clausthal or Göttingen), the lecture and tutorials will be broadcasted via a Google Hangout on Air (HOA). Also, we plan to provide students with recordings of the lectures.

The HOAs will not be listed publicly. If you want to be invited to the HOA or be able to view the recordings afterwards, please create a Google Plus account and send your Gmail address (edit: send me the URL of your Google+ page) via e-mail to greenyer@inf.uni-hannover.de. You will then receive invitations for the Hangout events.

Oct 10, 2014  

Time and place of the Tutorial (currently scheduled for Tuesdays 15:00-16:00) will be changed, since there are collisions with other lectures (especially MEM). The date is yet to be determined. Probably we will find a suitable time for everyone during the first lecture.

Oct 10, 2014  Note that the lecture will be on Tuesdays 16:00 - 17:30!! and not Thursdays, as was indicated on this page before. 

 

Material

 Lecture week Lecture Material Tutorial material
1. slides (PDF)  
2. slides (PDF) (note: material on LTSA-tool will be covered next week)  
3. slides (PDF)  
4. slides (PDF) (preliminary version, may change after the lecture)

assignments (PDF)

description project II (PDF)

5. slides (PDF)  
6. no lecture  
7. slides (PDF)  
8. slides (PDF)  
9. slides (PDF)  
10. slides (PDF) assignments (PDF)
11. slides (PDF)  
12 slides (PDF)  
13. slides (PDF)  assignments (PDF)
14. slides (PDF)  

General Information

Motivation

Software-intensive systems take an increasingly critical role in many areas of our lives. For example, today's cars, trains, and airplanes run millions lines of code, industrial manufacturing systems are highly automated, and, moreover, software controls critical applications in businesses, government, and healthcare.

To ensure the quality of these software systems, formal development and analysis techniques become increasingly important. Their application today, however, is limited by three factors. The first factor (1) is certainly the growing complexity of systems, which often prevents exhaustive automated techniques to be applied. The second factor (2) is that formal analysis tools often operate on simple mathematical models, so that integration with the tools and models used by engineers during the development is a challenge. Third (3), many domains lack the expert knowledge of successfully applying formal development analysis techniques.

Learning Objectives

The goal of this lecture is to, first (1), introduce the students to formal modeling techniques, such as different forms of automata and formal temporal logics. The second goal (2) is to give the students a detailed knowledge of selected analysis techniques and the involved algorithms. The third goal is to give the students an elementary knowledge of applying formal analysis techniques to solve practical software and systems engineering problems.

Contents

The prominent analysis technique covered in this lecture is model checking, which is a technique for automatically proving that a dynamic model of a system satisfies a given specification. This lecture also introduces how formal modeling an analysis techniques are applied in the development process of software and systems. Furthermore, this lecture introduces the basic principles of automatically synthesizing software models that satisfy a given specification. On the side, we may explore selected advanced topics, such as formal techniques for real-time systems.

Format

This lecture combines theoretical concepts with their practical application. In order to achieve the above learning objectives, the lecture will be accompanied by a tutorial. In the tutorial, we discuss small exercises. Mainly, however, the students shall work on small-size projects where they will, for example, prototypically implement model-checking algorithms or apply model-checking tools to model and analyze example systems.

Students shall work together on the exercises and projects in groups of three to four people.

This lecture will be held in English. It is offered also to students of the international Master program Internet Technologies and Information Systems (ITIS) for students in Braunschweig, Clausthal, Göttingen, and Hanover.

To accommodate for the students not residing in Hannover, we plan to broadcast the lecture and tutorials live via a Google Hangout on Air (HOA), as well as provide students with recordings of the lectures.

The HOAs will not be listed publicly. If you want to be invited to the HOA and view the recordings, please create a Google Plus account and send the URL of your Google+ page via e-mail to greenyer@inf.uni-hannover.de. You will then receive invitations for the Hangout events.