Formal Methods in Software Development (WS 2020/21)
Section outline
-
326.013, Friday 8:30-11:00, Zoom, Start: October 9, 2020
Zoom Session (open from 8:15 on)https://jku.zoom.us/j/93538736451?pwd=OTdnTVNXOVJhcURDMmd4bG1DQTVRQT09
Meeting-ID: 935 3873 6451 Password: formalTo take part in the course, you have to enrol in the KUSSS system. This course is offered simultaneously for the master program "Computer Science" and for the master program "Computer Mathematics".
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.
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.
-
The following is a preliminary schedule of the lecture:
- October 7: introduction and organization, the language of logic.
- October 14: the RISC Algorithm Language, specifying and verifying (part 1).
- October 21: specifying and verifying (part 1).
- October 28: specifying and verifying (part 1).
- November 4: the art of proving, the RISC ProofNavigator.
- November 11: specifying and verifying (part 2), the RISC ProgramExplorer.
- November 18: the Java Modeling Language (part 1).
- November 25: the extended static checking of Java programs with ESC/Java2.
- December 2: verifying Java programs with KeY.
- December 9: the Java Modeling Language (part 2),
- December 16: modeling concurrent systems.
- January 13: specifying in temporal logic.
- January 20: the Spin model checker, automatic model checking.
- January 27: automatic model checking, verifying safety properties by proving.
- October 7: introduction and organization, the language of logic.
-
-
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)
- Formal Methods in Dependable Systems Engineering (local copy)
- 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
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
-
8 exercises are handed out. From these, the best 7 are used for grading (in total 350 points have to be earned).
-
The final exam must be passed positively; it accounts for 50% of the course grade.
- Second Exam: Tuesday, March 23, 17:15-19:30, Zoom/JKU Moodle.
- Second Exam: Tuesday, March 23, 17:15-19:30, Zoom/JKU Moodle.
-
Date: Tuesday, March 23, 17:15-19:30, Zoom/JKU Moodle
- To participate in the exam, you have to do until Friday, March 19 the following:
- You have to register in KUSSS for the exam and
- you have to upload in the corresponding course of the JKU Moodle in the assignment "Exam March 23, 2021" a picture file "Ausweis.*" with a photo of your student id card:
-
- I will announce per email in KUSSS by Monday, March 22, who may participate in the exam.
- To take part in the exam, you need a computer with internet connection and Web-/Laptop-/Phone-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 (the link above).
- At 17:15 (not later) you enter the Zoom Meeting whose id and password is announced in the JKU Moodle course. Join the meeting with only one client using 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 17:30 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. Furthermore, no headsets or earplugs are allowed during the exam.
- 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.
- During the exam, you may ask questions (only) via the "Chat" feature of the Zoom session (German or English, no audio questions).
- At 19:00 (not before) you stop your elaboration and start to photograph/scan and upload your results in the form indicated below.
- Until 19:15 latest the results of the exam have to be uploaded in the assignment "Exam March 23, 2021" 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. You may also combine all files to a single archive file (preferably in
zip format) or to a single document (preferably in PDF format).
- At 19: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 19:30 in the Zoom meeting.
- If your Zoom connection is interrupted during the exam, join the Zoom meeting again as quickly as possible. If there are longer Zoom interruptions or above regulations are violated, I may not grade your exam. The Zoom session will not be recorded., but after the exam I will check the Zoom/Moodle logs for conformance to the regulations.
- 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).
