Verification of temporal properties in embedded software [Elektronische Ressource] / vorgelegt von Djones Vinicius Lettnin

Mein Name

Sujets

• Informatik

Informations

• Publié par: eberhard_karls_universitat_tubingen
• Publié le: 01 janvier 2009
• Nombre de lectures: 11
• Langue: English
• Poids de l'ouvrage: 3 Mo

Extrait

Verification of Temporal Properties
in Embedded Software
Dissertation
der Fakultat¨ fur¨ Informations- und Kognitionswissenschaften
der Eberhard-Karls-Universitat¨ Tubingen¨
zur Erlangung des Grades eines
Doktors der Naturwissenschaften
(Dr. rer. nat.)
vorgelegt von
M.Sc. Djones Vinicius Lettnin
aus Pelotas - Brasilien
Tubingen¨
2009Tag der mundlichen¨ Qualifikation: 15. Juli 2009
Dekan: Prof. Dr. Oliver Kohlbacher
1. Berichterstatter: Prof. Dr. Wolfgang Rosenstiel
2. Prof. Dr. Thomas Kropf“Jesus said to them,
‘I am the bread of life;
whoever comes to me
shall not hunger,
and whoever believes in me
shall never thirst.’ ”
John 6:35
“What I know is a drop,
what I ignore is an ocean.”
Issac Newton (1642-1727)To my wife Fabi
for your love, patience and support.Acknowledgments
My thanks to my family, colleagues, cooperation partners and friends who accompanying me
during this work. In particular, I thank ...
• my advisor Prof. Dr. Wolfgang Rosenstiel for the comprehensive support and for the excel-
lent opportunity of being his student in these six years during my master and my doctoral
degree. For his insights in the integration of research and real industrial applications. Also
for his support allowing me the participation of conferences and academic activities. His
attention and motivation contributed to my personal and professional improvement.
• Prof. Dr. Thomas Kropf for his support, orientation and opportunity of taking part of the
Formal Methods Group. Thanks for creating links between research and real industrial ap-
plications. Also for his explanatory notes and suggestions for the improvement of this dis-
sertation.
• the researchers Dr. Joachim Gerlach and Dr. Jur¨ gen Ruf. Joachim, for his incentive and
dedication that contributed to the development of this work. Jur¨ gen, for his attention that
gave me the comprehension of verification. I thank you both for your numerous suggestions
and improvements in this dissertation.
• my colleges Dr. Pradeep Nalla and Jor¨ g Behrend. Pradeep, for his support, detailed and
intense discussions on subjects that gave me the comprehension of verification. It really
helped me in many ways to improve my work. Jor¨ g, for discussions and friendly cooperation
work. I thank you both for your numerous suggestions, and improvements in this
dissertation.
• my colleges Dr. Prakash Peranandam, Dr. Axel Braun, Dr. Roland Weiss, Dr. Edelweis Ritt
and Markus Winterholer for discussions and friendship. Mike Bensch, Dominik Brugger,
Dr. Michael Tangermann, Thomas Grosser and Julio Oliveira for your friendship.
• my students Stefanie Ipfling, Alexander Grunhage¨ and Tobias Kirsten for discussions and
support.
• the Eberhard Karls University of Tubingen¨ and the Wilhelm-Schickard-Institute for Com-
puter Science for supporting the necessary conditions for the development of this work.
• the Conselho Nacional de Pesquisa (CNPq) for the financial support that was indispens-
able for the development of this work. Additionally, I thank the Deutscher Akademischer
Austausch Dienst (DAAD) for the opportunity to improve my German skills.
• NEC Electronics (Dusseldorf¨ - Germany) for the embedded software industrial application.
• Bosch (Leonberg - Germany) for cooperation work.
• Cadence Research Laboratories (Berkeley - USA), specially Dr. Andreas Kuehlmann and Dr.
Ken McMillan, for the internship and for the great experience in software formal verification.• my wife Fabi, for your love, patience and support.
• my parents, Remy and Leda, my sister, Nubia, and my brother-in-law, Valdecir, for support-
ing me in all moments of my life.
• my family Geller and my family in Germany, Walter and Hedy Wagner, Regina Kesting,
Hartmut and Lidia Heider for supporting me in many moments.
• the kindly God for everything.
Djones Vinicius LettninAbstract
For some years ago the main statement among verification engineers was “Bugs in hardware
cost money”. Nowadays, the embedded software is playing an important role in the embedded
systems industry and the statement can be updated to “Bugs in hardware and in software cost a lot
of money”. Embedded software is very powerful in embedded systems in order to implement im-
portant functionalities and functional innovations. The developing costs of embedded software are
becoming huge and its amount in safety critical systems is increasing. Therefore, the verification
of complex systems needs to consider the verification of both hardware and embedded software
modules.
The most commonly used approaches to verify embedded software are based on co-simulation or
on co-debugging, which consume long verification time and additionally have coverage limitations.
Formal verification assures complete coverage, but is limited to the size of the module that can be
verified. This dissertation extends the conventional verification limitations with methodologies that
are based on temporal properties and formal verification. This work proposes to combine temporal
assertions with testing, which is suitable to be applied in existing design flows due to the experience
of the verification engineers with conventional verification approaches. Thus, the formalization
of the requirements by means of temporal properties is able to improve the understanding about
the design and the assertions can be re-used later in the combination of simulation and formal
verification approaches.
The main contributions in this dissertation are (1) two new approaches to integrate assertion-
based verification in embedded software verification and (2) one new semiformal verification ap-
proach to increase state space coverage compared to simulation-based methods. The developed
solutions are evaluated against an industrial automotive embedded software application.
Targeting at simulation-based verification techniques, new approaches are identified and investi-
gated to efficiently integrate assertions in the verification of embedded software: On the one hand,
a SystemC hardware temporal checker is extended with interfaces to monitor the embedded soft-
ware variables and functions that are stored in a microprocessor memory model. On the other hand,
a SystemC model is derived from the original C code to integrate directly with the SystemC tem-
poral checker. The first approach shows the advantage to verify temporal properties in C programs
straightforward under real conditions, however, requiring to explicitly model the microprocessor
itself. For the second approach, a shorter verification time is achieved, however, a SystemC model
has to be generated with more abstraction information.
Due to the limitations of simulation-based approaches, a new semiformal verification is devel-
oped. Targeting at semiformal verification techniques, an approach called SofTPaDS (Semifor-
mal Verification of Temporal Properties in Hardware-Dependent Software), which is based on the
combination of both assertion-based and symbolic simulation strategies for the verification of em-
bedded software with hardware dependencies, is designed. In this approach, a simulation-based
traversing of the state space is combined with local (temporal restricted) explorations of specific
states on the simulation traces. The semiformal approach is evaluated to be more efficient than
state-of-the-art model checkers in order to trace deep state spaces, and shows improvements in the
state coverage relative to a simulation-based software verification approach.