Automated Verification Tools for Embedded Software (Sommersemester 2018)

Lecturer: Prof. Dr. Holger Giese (Systemanalyse und Modellierung)

General Information

• Weekly Hours: 4
• Credits: 6
• Graded: yes
• Enrolment Deadline: 20.04.2018
• Teaching Form: Project seminar
• Enrolment Type: Compulsory Elective Module

Programs, Module Groups & Modules

Description

Many safety critical applications such as, automobiles, avionics, manufacturing processes, nuclear reactors, etc., involve concurrent or parallel subsystems. They are required to be dependable in their performance. Due to the shift from single processor to multi-core processors, there is a growing concern to develop automated methods for formally verifying concurrent embedded systems.  Automated verification techniques also have been playing an important role in pre-silicon validation processes.

Several industries show that the formal property verification in the design verification flow contains many issues and they build up several tools for property verification. Tools are generally used for checking several properties like  safety, liveness, boundedness etc. However, each tool have some limitations. In this course, we would like to evaluate the several tools by running on several benchmarks which are commonly used in both hardware and software industries. 

In this project seminar, we want to introduce several verification tools as well as their evaluation on several benchmarks  for embedded softwares which are widely used in several industries. 
 

Literature

[1] Christel Baier, Joost-Pieter Katoen: Principles of model checking. MIT Press 2008, ISBN 978-0-262-02649-9, pp. I-XVII, 1-975

[2] Manoj G. Dixit, S. Ramesh, Pallab Dasgupta: Early Time-Budgeting for Component-Based Embedded Control Systems. Embedded Systems Development, From Functional Models to Implementations 2014: 123-137

[3] Zohar Manna: Introduction to Mathematical Theory of Computation. McGraw-Hill, Inc. 1974., New York, NY, USA.

[4] Michael Huth, Mark Dermot Ryan: Logic in computer science - modelling and reasoning about systems (2. ed.). Cambridge University Press 2004, pp. I-XIV, 1-427

[5]  Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model checking. MIT Press 2001, ISBN 978-0-262-03270-4, pp. I-XIV, 1-314

[6] Mathias Soeken, Rolf Drechsler: Formal Specification Level - Concepts, Methods, and Algorithms. Springer 2015, ISBN 978-3-319-08698-9, pp. I-VIII, 1-138

[7] Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh: Verification and Validation in Systems Engineering - Assessing UML / SysML Design Models. Springer 2010, ISBN 978-3-642-15227-6, pp. I-XXVI, 1-248
 

Learning

The course is a project seminar, which has an introductory phase comprised by an initial short lecture. After that, the students will work in groups on verification tools applying to given benchmarks and finally prepare a presentation and write a report about their findings concerning the evaluation.

There will be an introductory phase to present basic concepts for the theme including the necessary foundations for several verification tools.

Examination

We will grade the group's evaluation (50%), reports (40%), and presentations (10%) for the evaluation of the tools. Participation in the project seminar during meetings and other groups' presentations in the form of questions and feedback will also be required.

Dates

After the introductory phase with an initial short lecture, we will identify the tools and benchmarks considered by the group and then there will be regular individual feedback meetings of the groups with their supervisors. In addition, there will also be regular meetings during the semester for the whole project seminar to discuss the progress of all groups and open questions in general.

The first meeting will be on Tuesday the 17th of April at 15:15 in room A-1.2.

Zurück