Software-Test: Verfa... Hauptseminar Softwar... Software-Test: Verfa...

Formale Methoden für eingebettete Hardware/Software-Systeme

Prof. Dr. Francesca Saglietti, Prof. Dr.-Ing. Jürgen Teich,
Dipl.-Inf. Johannes Drexler, Dipl.-Ing. Christian Haubelt

Seminar im Hauptstudium


Eingebettete Systeme spielen im alltäglichen Leben eine immer größere Rolle. Gleichzeitig nimmt die Komplexität dieser Systeme immer weiter zu. Dies führt dazu, dass es bereits heutzutage so gut wie unmöglich ist, die Fehlerfreiheit eingebetteter Systeme nachzuweisen. Die wesentlichen Gründe für diese Schwierigkeiten liegen in (a) dem hohen Maß an Wiederverwendung von Komponenten (diese sind oftmals einzeln verifiziert, aber die korrekte Funktionsweise im Zusammenspiel mit anderen Komponenten ist hierdurch nicht gegeben) und (b) dem hohen Grad an Vernetzung (nicht nur die Funktionalität der einzelnen Komponenten sondern auch deren Kommunikation muss verifiziert werden).
Dieses Seminar beschäftigt sich mit der Problematik des formalen Entwurfs eingebetteter Hardware/Software-Systeme. Hierbei soll auf Probleme
  1. bei der formalen Spezifikation der Systeme,
  2. bei deren automatischen Verfeinerung in Hard- und Software (Correct-By-Construction),
  3. bei der formalen funktionalen Verifikation sowie
  4. bei zusätzlichen Maßnahmen (Test, Echtzeitanalyse)
eingegangen werden. Ein besonderer Schwerpunkt in diesem Seminar liegt auf dem Aspekt Hardware/Software. Dies scheint immer dringender notwendig zu werden, da der Anteil an eingebetteter Software in eingebetteten Systemen immer weiter steigt.

Das Seminar wird in Kooperation der Lehrstühle für Software Engineering und für Hardware-/Software-Co-Design durchgeführt.

Die Themenschwerpunkte im Einzelnen umfassen: Literatur:
[STG+01]Karsten Strehl, Lothar Thiele, Matthias Gries, Dirk Ziegenbein, Rolf Ernst, and Juergen Teich: FunState - An Internal Design Representation for Codesign. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 9(4):524-544, August 2001.
[ETT98b]Michael Eisenring, Juergen Teich, Lothar Thiele: Domain-Specific Interface Generation from Dataflow Specifications. Codes/CASHE 98, Seattle, Washington, pages 43-47, March, 1998.
[Har87]David Harel: Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8(2), pages 231-274, June, 1987.
[Hoa78] C.A.R. Hoare: Communicating Sequential Processes. Communications of the ACM 21(8), pages 666-677, August, 1978.
[Kro99] Thomas Kropf: Introduction to Formal Hardware Verification, Springer, 1999.
[ABF94]Miron Abramovici, Melvin A. Breuer, Arthur D. Friedman: Digital Systems Testing and Testable Design. September 1994, Wiley-IEEE Press.
[CKT03]Samarjit Chakraborty, Simon Künzli, Lothar Thiele, Andreas Herkersdorf, Patricia Sagmeister: Performance Evaluation of Network Processor Architectures: Combining Simulation with Analytical Estimation. Computer Networks, Vol. 41, No. 5, pages 641--665, 2003.
[Est04] http://www.esterel-technologies.com/
[Pto04]http://ptolemy.eecs.berkeley.edu/
[MVH+04]André Meisel, Markus Visarius, Wolfram Hardt, and Stefan Ihmor: Self-Reconfiguration of Communication Interfaces. In Processings of 15th International Workshop on Rapid System Prototyping (RSP'04), pages 144-150, Geneva, Switzerland, June, 2004.
[EET+00]Egly, U., Eiter, T., Tompits, H., Woltran, S.: Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas. In: Proc. of the 17th Nat. Conf. on Artificial Intelligence. (2000) 417-422
[GNT01]Giunchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for Quantified Boolean Formulas. In: Proc. of the 17th Int. Joint Conf. on Artificial Intelligence. (2001) 275-281
[COD99]Clarke, E., Grumberg, O., Peled D.: Model Checking, MIT Press, 1999
[LS99]de Lemos, R., Saeed, A. : Validating Formal Verification using Safety Analysis Techniques. CS-TR: 668, Department of Computing Science, University of Newcastle, 1999
[Ban04]http://bandera.projects.cis.ksu.edu/
[Abl04]http://www-2.cs.cmu.edu/~able/
[HDD+92]Hu, A., Dill, D., Drexler, A., Yang, C.: Higher-Level Specification and Verification With BDDs. Workshop on Computer-Aided Verification, Montreal, Quebec, June 29 -- July 2, 1992.
[FBK+91]Fujiwara, S., Bochmann, G., Khendek, F., Amalou, M., Ghedamsi, A.: Test selection based on finite state models. IEEE Transactions on Software Engineering, 17(6), 1991
[Dam99]Dams, D.: Flat Fragments of CTL and CTL*: Separating the Expressive and Distinguishing Powers. Logic Journal of the IGPL, Volume 7, Issue 1, 1999.



top