Title
Applying Formal Verification Methods to Embedded Systems
Type
Joint weekly Seminar with the Embedded Software Laboratory in Theoretical and Practical CS (at Aachen)
News
- 07.07.2009: The evaluation results are available.
- 05.02.2009: The slides of the introduction are available.
Important Dates
| 05.02.2009 | Introduction to topics |
| (8:30 at seminar room of I11 (no. 2323)) | |
| 6 weeks before talk | literature & structure |
| 2 weeks before talk | final version of paper |
| 1 week before talk | final version of slides |
Contents
An embedded system is a special-purpose computer system designed to perform a dedicated functions. Embedded means that it is part of a complete device including hardware and mechanical parts. Embedded systems control many of the common devices in use today.
The dramatically increasing amount and importance of software in such systems poses new challenges to their engineering. Today's cars, for example, host nearly 1 GByte of code distributed over up to 70 electronic control units interconnected with up to five different buses. The key to meeting the challenges posed by this rising system complexity can be found in a sound design and analysis of the system's architecture. Therefore one is interested in design and analysis methods for system and software architecture that support the achievement of predefined quality goals and, in particular, meet current requirements like composability and exchangeability of software components from different sources and throughout the complete vehicle network.
Traditional methods for achieving safety properties mostly originate from hardware-dominated systems. Software-intensive embedded systems require new approaches, as they are for example suggested by the emerging standard IEC 61508. The goal of this seminar is to study constructive and analytical methods for ensuring safety that have a sound formal basis but are also efficiently applicable in different domains, like automotive or railway systems.
Topics
Each of the following topics is covered by two presentations, covering (a) its formal foundations (theoretical part) and (b) tool-supported applications (practical part), respectively. Talks are scheduled as "double features" from 15:00 to 16:30 on Tuesday at the seminar room of I11 (room 2323). The calendar dates are shown below.
No. | Date | Topic | Student | Supervisor |
|---|---|---|---|---|
1(a) | 21.04. | Data and Control Flow Analysis | Xiaoying Hu | |
1(b) | (entfällt) | Worst-Case Execution Time Analysis | Angel Tchorbadjiiski | |
2(a) | 28.04. | Abstract Interpretation | Holger Hoffmann | |
2(b) | 28.04. | Abstract Interpretation of Reactive Systems | Julia Bley | |
3(a) | (entfällt) | Program Transformation by Slicing | Falak Sher | |
3(b) | 12.05. | Application of Slicing to Model Checking | Wenzheng Gao | |
4(a) | 12.05. | Separation Logic | Philipp Siebenkotten | |
4(b) | (entfällt) | Shape Analysis | Christian Bryllok | |
5(a) | 19.05.
(at I2!) | Model Checking for Computation Tree Logic | Stefan Breuer | |
5(b) | (entfällt) | The [mc]square Tool | Sebastian Kaufmann | |
6(a) | (entfällt) | Runtime Verification Using Linear Temporal Logic | Fehmi Karanfil | |
6(b) | 19.05. | The Java PathFinder Tool | Norbert Wiechowski | |
7(a) | 26.05. | Model Checking for Timed Automata | Daniel Schemmel | |
7(b) | (entfällt) | The UPPAAL Tool | Rajeevan Rabindran | |
8(a) | 30.06. | Model Checking for Hybrid Automata | Ivan Golod | |
8(b) | (entfällt) | The PHAVER Tool | Mustafa Karafil | |
9(b) | 30.06. | Validating Wireless Sensor Network Protocols | Andreas Weigelt | |
9(a) | 14.07. | Probabilistic Model Checking | Mike Schmitz | |
10(a) | (entfällt) | Equivalences: Simulation and Bisimulation | Andreas Hüttig | |
10(b) | (entfällt) | Dead Variable Reduction and Path Reduction | Aamer Shah |
Literature
No. | Literature |
|---|---|
1(a) | Flemming Nielson, Hanne R. Nielson, Chris Hankin: Principles of Program Analysis, 2nd ed., Springer, 2005 (Sct. 1.3 and 2) |
1(b) | Christian Ferdinand, Reinhold Heckmann, Marc Langenbach, Florian Martin, Michael Schmidt, Henrik Theiling, Stephan Thesing, Reinhard Wilhelm: Reliable and Precise WCET Determination for a Real-Life Processor, EMSOFT 2001, LNCS 2211, 2001, 469-485 |
2(a) | Flemming Nielson, Hanne R. Nielson, Chris Hankin: Principles of Program Analysis, 2nd ed., Springer, 2005 (Sct. 1.5 and 4) |
2(b) | D. Dams, R. Gerth, O. Grumberg: Abstract Interpretation of Reactive Systems, ACM Transactions on Programming Languages and Systems 19(2), 1997, 253-291 |
3(a) | F. Tip: A Survey of Program Slicing Techniques, Journal of Programming Languages 3(3), 1995, 121-189 |
3(b) | J.Hatcliff, M.B.Dwyer, H.Zheng: Slicing Software for Model Construction. J. Higher Order Symbol. Comput. 13(4):315-353, 2000 |
4(a) | John C. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures. LICS 2002: 55-74
Alexey Gotsman, Josh Berdine, Byron Cook: Interprocedural Shape Analysis with Separated Heapabstractions A, SAS 2006, LNCS 4134, 240-260 |
4(b) | Dino Distefano, Peter W. O'Hearn, Hongseok Yang: A local shape analysis based on separation logic, In Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems vol. 3920, pp. 287-302, April 2006 |
5(a) | C. Baier, J.-P. Katoen: Principles of Model Checking, MIT Press, 2008 (Sct. 6) |
5(b) | Bastian Schlich and Stefan Kowalewski: [mc]square: A model checker for microcontroller code, In Proc. 2nd Int'l Symp. Leveraging Applications of Formal Methods, Verification and Validation (IEEE-ISoLA 2006), pages 466-473, IEEE Computer Society
Bastian Schlich: Model Checking of Software for Microcontrollers, Dissertation Thesis. AIB-2008-14, RWTH Aachen University, 2008
|
6(a) | V. Stolz, F. Huch: Runtime verification of Concurrent Haskell programs. Proceedings of the Fourth Workshop on Runtime Verification (RV 2004), ENTCS 113, Elsevier, 2004, 201-216 V. Stolz, E. Bodden: Temporal Assertions using AspectJ, Proceedings of the Fifth Workshop on Runtime Verification (RV 2005), ENTCS 144(4), 2006,109-124 |
6(b) | K. Havelund and J. Skakkebaek: Applying Model Checking in Java Verification, In Proc. of the 7th Workshop on the SPIN Verification System, 1999, 216-231, LNCS |
7(a) | François Laroussinie, Nicolas Markey, Ph. Schnoebelen: Model Checking Timed Automata with One or Two Clocks. CONCUR 2004: 387-401. LNCS, Springer Verlag. |
7(b) | Ansgar Fehnker, Lodewijk van Hoesel and Angelika Mader: Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks, Integrated Formal Methods, pages 253-272, LNCS, 2007 |
8(a) | Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, Sergio Yovine: The Algorithmic Analysis of Hybrid Systems. Theor. Comput. Sci. (TCS) 138(1):3-34 (1995) |
8(b) | Goran Frehse: PHAVer: algorithmic verification of hybrid systems past HyTech, International Journal on Software Tools for Technology Transfer (STTT), pages 263-279, 2008 |
9(a) | C. Baier, J.-P. Katoen: Principles of Model Checking, MIT Press, 2008 (Sct. 10) |
9(b) | A. Boulis, A. Fehnker, M. Fruth, A. McIver. CaVi -- Simulation and Model Checking for Wireless Sensor Networks. QEST 2008. (pdf). |
10(a) | C. Baier, J.-P. Katoen: Principles of Model Checking, MIT Press, 2008 (Sct. 7) |
10(b) | Bastian Schlich, Jann Löll, Stefan Kowalewski: Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code, Formal Methods for Industrial Critical Systems, pages 21-37, 2008, LNCS
Karen Yorav and Orna Grumberg: Static Analysis for State-Space Reductions Preserving Temporal Logics, Formal Methods in System Design, pages 67-96, 2004 |
Requirements
- Vordiplom Informatik or Bachelor in Computer Science (in particular: basic knowledge in Automata Theory and Formal Languages)
- The written exposition and the presentation can be done in either German or English.
- Basic knowledge in Embedded Systems and Model-Checking techniques is not mandatory but helpful.
Contact person
