Formal Methods for Embedded Systems
News
| | 08.08.2005 | | Exam results |
| | 14.07.2005 | | The question hour on Jul 20 2005 will start at 3:30 pm. |
| | 27.06.2005 | | The last two exercises will take place on June 29th 2005 and July 13th 2005. On July 20th 2005, we will arrange a question time, where questions considering the exam will be answered. |
| | 15.06.2005: | | Access to your files is now possible. |
| | 10.06.2005: | | On June 23 2005, Dr. Carsten Weise, Ericsson GmbH, will talk about “Modelchecking Timed Automata using UPPAAL”. |
| | 10.06.2005: | | Modified version of the 5th lecture is now online. |
| | 31.05.2005: | | On June 8 2005, the Dies will take place. Therefore, the exercise course will be cancelled. The alternative dates for the exercise will be on June 15 2005 and June 22 2005. |
| | 11.05.2005: | | The lecture for today, 11.05.2005, is cancelled. |
| | 10.05.2005: | | Paragraph on SMV added. |
| | 28.04.2005: | | On 11.05.2005 there will be a lecture instead of the exercise. The exercise will be cancelled for that day. The next exercise will take place on 25.05.2005. Other lecture dates will be held as planned. |
| | 11.04.2005: | | The forum for the lecture is set. You can post your questions there. |
| | 18.03.2005: | | The lecture will start on April 21st 2005 and the exercise one week later on April 27 2005. |
| | 01.12.2004: | | Lecture has been set and schedules have been listed. |
Lecture
The lecture will be held in german.
| | Lecture | | Dates |
| | 1. Lecture | | 21. April 2005 |
| | 2. Lecture | | 28. April 2005 |
| | 3. Lecture | | 12. May 2005 |
| | 4. Lecture | | 02. June 2005 |
| | 5. Lecture | | 09. June 2005 |
| | 6. Lecture | | 16. June 2005 |
| | 7. Lecture | | 23. June 2005 (Guest: Mister Dr. Carsten Weise, Ericsson GmbH) |
| | 8. Lecture, Slides, Script | | 30. June 2005 |
| | 9. Lecture | | 07. July 2005 |
Exercise
The exercise will be held in german.
| | Exercise | | Release |
| | 1. exercise | | 27. April 2005 |
| | 2. exercise | | 25. May 2005 |
| | 3. exercise | | We will finish the 2. exercise |
| | 4. exercise | | 22. June 2005 |
| | 5. exercise | | 29. June 2005 |
| | 6. exercise | | We will finish the 5. exercise |
Tools
SMV
We will be using SMV as the first model checker in the exercise. SMV was developed by Ken McMillan. There are different versions of SMV. The first version is CMU SMV. CMU SMV does CTL model checking. The newer version is Cadence SMV. Cadence SMV supports CTL and LTL Model Checking, but concentrates on LTL model checking. Besides these 'originals' there are some reimplementations and modified SMV versions. We will be using Cadence SMV in the exercise.
SPIN
The second model checker we will be using in the exercise is SPIN. SPIN was developed by Bell Labs and is available for free since 1991. SPIN is a LTL model checker that concentrates on software verification. There are a bunch of modified versions: RT-SPIN, dSPIN, etc. We will be using the original for the exercise.
UPPAAL
The last model checker in this exercise will be the real-time model checker Uppaal. It was developed in cooperation with the university of Aalborg and the Uppsala university. Uppaal concentrates on the verification of safety-conditions. The specification of attributes is carried out through a subset of CTL.
Dates
- Lecture: Thu, 10:00-11:30, AH I
- Exercise: Wed, 15:15-16:45, AH III