Biography
Dr Rachid Hadjidj is a faculty member in the Department of Computer Science and Engineering at the university of Qatar. He has a Phd degree in computer Engineering from the university of Montreal (Ecole Polytechnique) in CANADA, a Master degree in computer science from the university of science and technology Houari Boumedienne in Algeria, and an Engineer degree in computer science from the same university. After getting his PHd degree , Dr Rachid Hadjidj worked as a Post doc fellow for two years at the university of Concordia (Canada), and as a consultant with the Canadian National defense , Fujitsu , and Bell Canada. His fields of research include: Real time systems modeling and verification , System engineering, Hardware and Software verification, Automatic verification and model checking, Computer security and forensics, and Bioinformatics.
Personal Details |
|||||||||
|
|||||||||
Qualifications |
|||||||
|
|||||||
Research Interest |
|
With the advance in technology, systems grow in complexity and become increasingly difficult to develop, verify and maintain. Real time systems are a category systems which behaviors take also into account timing constraints. These systems are in general concurrent, distributed and more difficult to construct and validate. In this context, formal methods are strongly recommended since they rely on sound mathematical bases. Formally verified systems enjoy a high degree of confidence, which allows their designers to be more persuasive when it comes to convince deciders for their installation. My PhD research goal was to develop formal verification techniques to help construct more safe and reliable real time systems and telecommunication protocols. For this, several mathematical formalisms have been investigated and the Time Petri Net model (TPN model) was retained for its power to model both concurrency and timing constraints in a concise and natural way. However, the model has serious drawbacks when it comes to verification due to a lack of research in this field. The objective of my research was to overcome this limitation by proposing efficient approaches to verify timed and untimed properties of real time systems using model-checking techniques. Since the state space of a real time system is in general continuous and infinite, model-checking application requires an additional abstraction step to generate a discrete and finite abstract state space. This state space must also preserve properties we want to verify. For untimed properties, my contributions are propositions to attenuate the state explosion problem. I started first by defining a formal framework to characterize an abstract state model vis-à-vis the properties it preserves, then proposed some abstract state models for a real time system that preserve its reachability, linear and branching properties. These properties can then be verified using classical model-checking methods. For timed properties, I defined a temporal logic and proposed a forward on-the-fly verification technique, based on the so called state class method, then I proved its decidability for all bounded TPN Models. To evaluate the performance of my verification approach, I compared it with the model checking technique implemented in the tool UPPAAL which verifies timed automata modes. In average, I was able to verify TPN models more than ten times faster than UPPAAL for equivalent timed automata models, and with much lesser memory usage. For certain properties, the verification is more than 3400 times faster, with 110 times lesser memory. Another outcome of my PhD work was Real Time Studio, a tool to model and verify real time systems. The tools allows for a modular design of real time systems using interpreted time Petri nets, and implements all my proposed approaches and several other functionalities related enumerative analysis of real time systems, including CTL, LTL, and TCTL model checkers, and a minimizer under bisimulation. The tool is under constant improvement and several extensions are expected, to widen the scope of its use. Two of these extensions are already in progress; one of them is related to the formal verification computer security, the other one deals with bioinformatics for the simulation of bio-pathways using Hybrid functional Petri Nets
|
|
