Deutschland online bookmaker http://artbetting.de/bet365/ 100% Bonus.

Download Template Joomla 3.0 free theme.

Thesis Defenses 2008

Diagram Based Verification of Reactive and Real Time Systems Using Temporal Logic. Case Study: Fischer’s Protocol

By: Mohammad Hatami Rashidi
Supervisors: Dr. Ali Moeini
Advisor: Dr. Dara Moazzami

Defense room: Shahid Rajabbeygi Hall
Committee: Dr. Shahriar Heshmati, Dr. Ali Movaghar
Date: Tuesday, June 24, 2008

Abstract: Reactive systems are those systems that have reaction with environment. Because of their application in special cases, function of these systems is important and unavoidable. Air traffic control systems and nuclear reactors are samples of reactive systems that have low fault tolerance in design and production, so reactive formal methods have important function in verification.
Among reactive systems, real time systems are in attendance. A lot of methodologies and approaches were proposed for verification of these systems, For example diagram based approach proposed by Lamport and other researchers .Diagrams integrate deductive and algorithmic verification techniques for the verification of finite and infinite-state systems, thus combining the expressive power and flexibility of deduction with the automation provided by algorithmic methods. Predicate diagrams can be used to verify not only discrete systems, but also some more complex classes of reactive systems such as real-time systems and parameterized systems. It seems that time predicate diagrams and predicate diagrams are complete .Some tools can be used for supporting the generation of diagrams semi-automatically.
In this dissertation, an example of reactive systems is specified and verified. This system included some processes with having each process has a critical section. Number of processes is arbitrary. It is similar to this system: A systems included some processes and a common resource. Common resource is occupied by only one process. For satisfaction of mutual exclusion in entrance to critical section, we use Fischer’s protocol. Initially, systems were specified by temporal logic, then verified by predicate diagrams and timed predicate diagrams.
Previous researches in this field include some limitation, so generality of discussion was decreased. It is attempt to decrease the limitation and condition of problem and solve it in general case. Previous works solve this problem only with two processes, but it generalized number of processes in this dissertation.

Diagram Based Verification of Hybrid and Parameterized Systems, Using Temporal Logic

By: Farid Alaghmand
Supervisors: Dr. Ali Moeini
Advisor: Dr. Dara Moazzami

Defense room: Engineering Science 1
Committee: Dr. Shahriar Heshmati, Dr. Ali Movaghar
Date: Saturday, October 4, 2008

Abstract: Reactive systems are those systems that have an ongoing interaction with their environment and since they are used in critical applications, ensuring their safety is necessary. Formal analysis techniques can be used to verify their safety property.
There are basically two approaches to verification of reactive systems: the algorithmic approach in one hand and the deductive approach on the other hand. Recently diagram based techniques have been proposed to combine some of the advantage of deductive and algorithmic verification approaches. In this thesis, first hybrid and parameterized systems are introduced and then challenges for their verification are explained. Finally a diagram-based algorithm for verification of hybrid systems is proposed.
The main idea behind the algorithm is to modeling hybrid systems with rectangular automata, and then using previous studdings for verification of rectangular automata.
We also use linear temporal logic (LTL) to specify the properties we are interested in. Previous researches and studding are mostly restricted to linear systems and analyze the differential equations directly. While this thesis deals with modeling with rectangular automata and analyzing the automata. The most important advantage of proposed algorithm is that can be applied to both linear and nonlinear systems.