Formal Methods in Software Development (WS 2019/20)
Section outline
-
Friday 8:30-11:45, MT 226/1, Start: October 11, 2019
Important: To take part in the course, you have to enrol in the KUSSS system.The course is offered simultaneously as
- KV3/326.013 (for the master program "Computer Science") and
- KV4/326.053 (for the master program "Computer Mathematics").
Please enrol for the course intended for your degree program.
This course gives a survey on the use of formal methods for the development of reliable software. More specifically, we deal with
- specifying sequential programs and concurrent systems,
- computer-supported verification,
- extended static checking,
- model checking.
Furthermore, a guest lecture by Janos Sztrik (University of Debrecen) will give an introduction on
- queueing theory and its application to the performance analysis of computing systems.
The course consists of two parts:
- a lecture part where the fundamental issues of the field are taught, and
- an exercise part where practical skills are trained using freely available software tools.
The grading of the course will be based on a couple of exercises and a final exam.
Since the exercises will be submitted via Moodle, you also have to login in Moodle and register as a course participant. You will then also receive per email all messages posted in the Announcements forum and may yourself post messages in the Questions and Answers forum.
-
Lectures in italics are mandatory for KV4 students but also strongly recommended to KV3 students.
- October 11: introduction and organization, the language of logic, the RISC Algorithm Language.
- October 18: specifying and verifying (part 1).
- October 25: specifying and verifying (part 1).
- October 31 (15:30-18:45, S3 047): exponential distribution and its properties, poisson process, Markov chains, etc. (Sztrik).
- November 4 (12:00-15:15, S3 047): Markov-type queueing systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations. (Sztrik).
- November 8: modeling tools, retrial queueing systems, case studies. (Sztrik).
- November 15: specifying and verifying (part 1), the art of proving, the RISC ProofNavigator,
- November 29: specifying and verifying (part 2), the RISC ProgramExplorer.
- December 6: JML (part 1), ESC/Java2.
- December 13: ESC/Java2, the Key Verifier.
- December 20: JML (part 2), modeling concurrent systems.
- January 10: specifying in temporal logic.
- January 17: the Spin model checker.
- January 24: automatic model checking, verifying safety properties by computer-supported proving.
- October 11: introduction and organization, the language of logic, the RISC Algorithm Language.
-
Thinking Programs (draft manuscript, password will be handed out in class)
Chapter 8: Computer Programs (teaser pages only)
- Computer Programs/Systems as Subject of Formal Reasoning
- Introduction (4 on 1)
- Fehler im System: der Traum von Software ohne Bugs (restricted)
- Retrospective: Hoare: An Axiomatic Basis for Computer Programming (restricted)
- Formal Methods: Practice and Experience (local copy)
- Formally Verified Software in the Real World (restricted)
- Demonstration Examples
- Logic, Checking, and Proving (4 on 1)
- Specifying and Verifying Sequential Programs
- Specifying and Verifying Programs: Part 1 (4 on 1)
- Assigning Meaning to Programs (restricted)
- An Axiomatic Basis for Computer Programming (restricted)
- summation.txt, linsearch2.txt, linsearch3.zip
- Specifying and Verifying Programs: Part 2 (4 on 1)
- Specifying and Verifying Java Programs
- The Java Modeling Language: Part 1 (4 on 1)
- Behavioral Interface Specification Languages (restricted)
- Specification and Verification: The Spec# Experience (restricted)
- Extended Static Checking with ESC/Java 2 (4 on 1)
- Verifying Java Programs with KeY (4 on 1)
- The Java Modeling Language: Part 2 (4 on 1)
- Specifying and Verifying Concurrent Systems
- Modeling Concurrent Systems (4 on 1)
- Specifying and Verifying System Properties (4 on 1)
- Model-Checking Concurrent Systems (4 on 1)
- Abstrakte Kunst: Fehler finden durch Model Checker (restricted)
- Talking Model Checking Technology (restricted)
- ClientServer.txt
- Queueing Theory and its Application to the Performance Analysis of Computing Systems (Janos Sztrik)
The password to this area is handed out in class.
-
The following software is used in this course (how to use the software):
- RISC Algorithm Language
- RISC ProofNavigator
- RISC ProgramExplorer
- Java Modeling Language (JML) tools
- Use the stable release 5.5 from the archive (not the newer release candidates); also note that the JML tools need an installation of Java 1.4.2.
- Documentation
- OpenJML
- Extended Static Checking for Java (ESC/Java 2)
- KeY Verification Environment
- Tutorial (local copy), More Tutorials and Examples
- Spin Model Checker
-
10 exercises are handed out. From these 10 exercises,
- KV3: the best 7 are used for grading (in total 350 points have to be earned),
- KV4: the best 8 are used for grading (in total 400 points have to be earned, 1 exercise must be from the part of Sztrik).
-
The final exam must be passed positively; it accounts for 50% of the course grade.
- 1st Exam: Inspection is possible in Room S2 0327 (or one of the two neighboring rooms) at the following dates:
- Tuesday, March 3, 11:15-12:00.
- Thursday, March 5, 17:15-18:00.
- Friday, March 6, 12:00-12:45.
- 2nd Exam: Online Exam May 19, 2020 (see below)
-
Date: Tuesday, May 19, 16:00-18:30, Zoom/JKU Moodle
- To participate in the exam, you have to do until Tuesday, May 12 the following:
- You have to register in KUSSS for the exam (326.013 or 326.053) and
- you have to upload in the corresponding course of the JKU Moodle in the assignment "Exam May 26, 2020" a picture file "Ausweis.*" with a photo of your student id card:
-
326.053, KV Formale Methoden in der Software-Entwicklung, Wolfgang Schreiner / Janos Sztrik, 2019W
- If you have not been registered in KUSSS for one of these courses in the WS 2019/2020, you do not have yet access to this Moodle course. In this case, send me by Tuesday, May 5 an email with your id number such that I can register you in KUSSS.
- I will announce per email in KUSSS by Friday, May 15, who may participate in the exam.
- To take part in the exam, you need a computer with internet connection and Web-/Laptop-Cam (mandatory). You also need a device to convert handwritten DIN A4 pages into picture files of good quality (smartphone, tablet, scanner).
- The exam will proceed as follows:
- Login into the corresponding course of the JKU Moodle (one of the links above).
- At 16:00 (not later) you enter the Zoom Meeting whose id and password is announced in the JKU Moodle course. Join the meeting with your full name and registration number (format: "FAMILYNAME GivenName (kXXXXXXX)"). Activate your webcam and position it such that it shows yourself and your work place. Make sure that no one else is in the room and that no one
will enter the room during the exam.
- At 16:15 I will make the exam questions (a PDF file) visible in the Moodle course (you may print the file, but this is not necessary). From that time on, you may start your elaboration. You may use any materials (open book exam) but not perform any attempt at external communication.
- The exam is to be written manually with a dark pen on empty DIN A4 pages within the area well covered by your webcam. This area must not be left during the whole exam.
- You may ask questions (only) via the "Questions and Answers" forum in the JKU Moodle course (German or English, no audio questions).
- At 18:00 (not before) you stop your elaboration and start to photograph/scan and upload your results in the form indicated below.
- Until 18:15 latest the results of the exam have to be uploaded in the assignment "Exam May 19, 2020" of the JKU Moodle in the following form:
- One picture file "Foto.*" with a photo that shows your face, your student id card, and the first page of your manually written elaboration (Example).
- Picture files "Seite1.*", "Seite2.*", etc. with photos of every page of your manually written elaboration.
- At 18:15 (not before), position your camera such that it clearly shows (on your desk or in your hand) your student id card and the first page of your elaboration (as you have submitted it). Stay till 18:30 in the Zoom meeting.
- The meeting will not be recorded. If your Zoom connection is interrupted during the exam or above regulations are violated, I may not grade your exam.
- After the exam, preserve your written elaboration without changes. If the quality of your photos is not good enough for grading, I may ask for new ones.
- Please use the upload of the photo of your student id card to test your abilities to take photos and upload them in the Moodle course. Also test with some sample Zoom meetings your equipment (webcam).
