CENTRO DE INFORMATICA
POS-GRADUACAO EM CIENCIA DA COMPUTACAO
Raimundo da Silva Barreto
A Time Petri Net-based Methodology for
Embedded Hard Real-Time Software
A thesis submitted to the Centro de
Inform´tica of Universidade Federal de
Pernambuco in partial fulﬁllment of
requirements for the degree of Doctor
Advisor: Paulo Romero Martins Maciel
April 29th , 2005
Then Samuel took a stone,
and put it up between Mizpah and Jeshanah,
naming it Ebenezer, and saying,
Up to now the Lord has been our help.
I Samuel 7:12.
This thesis is dedicated to
my wife, and
my three children.
Whatever you do, work at it with all your heart, asworking for the Lord, not for men.
This journey, which is pleased and diﬃcult at the same time, has not been a solitary one.
First of all, I would like to acknowledge that my ability and patience to complete this work
comes from God. He has blessed me with the intellectual ability, the yearning for knowledge,
and the environments to allow those to grow. It is for Him that Iwork and live.
Many thanks to my wife Lu. Thanks to her unconditional love. She has stood me and
encouraged me throughout this process. Thanks also for patiently listening to me about this
thesis, even when she did not understand a thing what I said. Without her love, care, and
encouragement, I could not be where I am today. I am very grateful to my three children,
Lucas, Elizanne and Jessica.Many thanks to all my family, in particular, my mother, father
(in memoriam), and my sister Maria, for their part in my education. They have always done
what they could to encourage and support my desire to learn more and more.
Many thanks to my advisor professor Paulo Maciel. I could not have completed this thesis
without the support, encouragement, friendship, and tireless eﬀorts of him. Hebelieved in
the project, even when did not exist any possibility of good results. Certainly, he helped me
focus on the light at the end of the tunnel.
For their contributions and service as committee members, I thank Paulo Cunha, Nelson
Rosa, Ricardo Massa, Siang Wun Song, and Antonio Ot´vio Fernandes. I also wish to thank
professor Sergio Cavalcante for his support in the beginning ofthis research.
It has been very pleased to work with the ALUPA (informal name of our research group).
Thanks to all of you. Each one was very encouraging about my work. A special thanks
to Eduardo Tavares who helped me with several implementations; to Meuse who helped
me with case studies; Mar´ for implementing the translator from speciﬁcation to time
Petri net model; and Adilson andGabriel for implementing part of the tools in the EZPetri
environment. I could not forget to thank Sergio Murilo, a person who, in the beginning of
this research, was the ﬁrst to constantly encourage me for writing papers.
Thanks to several colleagues I made at CIn/UFPE. In order to not forget any name, feel
acknowledged all who read this thesis. Thanks to all professors and staﬀ in the center forinformatics. Thanks for the partial ﬁnancial support provided by CAPES.
On a more personal level, there are several people that deserve acknowledgment. Thanks
to several friends (outside the University) I made during my stay in Recife, mainly the
members of the Presbyterian Church in San Martin, which is a very pleasant church. Thanks
to all of you. I certainly learn a lot with you. Manythanks to Rev. Gilberto Barbosa Silva
and his wife Ana Lucia, by your friendship and aﬀection. Thanks to Rev. Silvandro and his
wife Helenilda, the ﬁrst Pastor we had in Recife. Many thanks to Rev. Edmilson Marinho,
his wife Ilza, and their children Priscila and Gabriel, for their support and friendship.
The problem to be addressed in this thesis is expressed in the...