Deutschland online bookmaker 100% Bonus.

Download Template Joomla 3.0 free theme.

Thesis Defenses 2009

Distributed Runtime Verification and Its Implementation on a Massively Multiplayer Online Game

By: Hamed Zaghaghi
Supervisors: Dr. Ali Moeini

Defense room: Engineering Science 1
Committee: Dr. Dara Moazzami, Dr. Ali Movaghar
Date: Wednesday, January 28, 2009

Abstract: This thesis introduces an implementation of an agent-based system together with an implementation of an agent-based online game so it can verify player’s behaviors. The method introduced verifies player’s behaviors in a distributed way when the player is playing. In other words this method uses distributed runtime verification in order to verify player’s behaviors. Two Runtime verification methods is introduced and used in this thesis.
Always game producers and owners try to publish a better game than the previous games, so they can gain more and more. If game producers want to know more about their players’ behaviors then they should mine game data was produced by players.
With Distributed Runtime Verification one can specify a player behavior using a formal language (Temporal Logic in this method) and then verify his/her play against specified behavior.

Keywords: Temporal Logic, Runtime Verification, Massively Multiplayer Online Games, Verifier Agents, Agent-Based Systems, Distributed Runtime Verification

A New Formal Multi-agent Framework: Supply Chain and Gene Network Application

By: Zahra Zamani
Supervisors: Dr. Ali Moeini

Defense room: Engineering Science 1
Committee: Dr. Dara Moazzami, Dr. Ali Movaghar
Date: Wednesday, February 18, 2009

Abstract: Multi-agent systems are a new solution to the complexity and distributing properties of software. Using standard design methods before implementing the actual system can prevent consuming resources. With this aim, a new framework has been designed for these systems and to ensure its correctness, this framework is specified and verified formally. The advantage of using formal methods is in its strong proof background in theory. The proposed abstract framework is adopted for two different applications. In the supply chain application, this framework can automate the payment process in the supply chain. This system is then specified using the semi-formal language UML, and then verified using the Temporal Logic language. In the gene network application, gene expression data is analyzed using different processes in this framework and the result is then available to the user. To make sure this system is safe and progresses in time, this framework is specified and verified using formal methods. To verify these systems, the SPIN model checker is used and verification results show that this framework is correct and safe to use for further application.

Interpreting literal/art – based texts in artificial intelligence

By: Zeinab Torabi
Supervisors: Dr. Kambiz Badie, Dr. Ali Moeini

Defense room: Engineering Science 1
Committee: Dr. Shahriar Heshmati, Dr. Ghassem Sani
Date: Wednesday, February 18, 2009

Abstract: Text processing is a basic area in artificial intelligence that has received much attention in recent decades. One of the branches in text processing is text interpretation, which include issues such as motivation analysis and message extraction (interpretation). Extracting messages from texts in terms of some phrases that do not initially exist in them, calls for a kind of transition from the existing concepts/predicates onto new ones. Such a process of transition can in this sense be regarded as a basic factor for configuring inference patterns in message extraction from texts.
Such a branch in text processing gets especially important, when a text can be interpretable in different ways due to the variation in the model of both writer and reader. Example can be mentioned for literal or artistic texts, where interpretation can achieve a promising role in their assessment.
Till now, a variety of approaches have been proposed for text interpretation, which can be generally sorted into those with natural language processing(NLP) orientation and those with concept processing orientation using inference rules.
Our emphasis in this thesis, is a kind of concept processing according to which, a text can be finally projected into a conceptual structure (not necessarily observed in the main text) through using a word net, a concept hierarchy, and a schematic network for text representation. In this thesis, an example is represented in the domain of scenario text interpretation, to show the efficiency of the suggested approach.

Application of information fusion in crisis management

By: Maryam lotfi Shahreza
Supervisors: Dr. Dara Moazzami
Co-Supervisor: Dr. Behzad Moshiri
Advisor: Dr. Mahmmod Reza Delavar

Defense room: Engineering Science 4
Committee: Dr. Ali Moeini, Dr. Mehdi Zare'
Date: Wednesday, September 30, 2009

Abstract: Due to the increasing frequency of disasters worldwide, crisis management is one of the most importance challenges. It is proved that information fusion methods can lead to good results in this area.
Self-Organizing Maps (SOMs) are the most well known unsupervised neural network approach to clustering. It is very efficient in handling large and high dimensional datasets. It can be used to reduce the dimensionality of sensor signals while preserving their topological relationships so that sensory information from different sources can be efficiently fused. We use one other algorithm in order to improving the results of Self-Organizing Map, it is Particle Swarm Optimization (PSO) discovered through simplified social model simulation. It is effective in nonlinear optimization problems and easy to implement.
In this research we integrate these two methods and introduce new method for anomaly detection. We have a discussion about our method and compare its results with some other methods and show that it works better than them. Here we implemented it for crisis management as early warning earthquake system and forest fire detection. We show that our algorithm is simple and there is no complex. Furthermore it does not consider information from different sources independent of each other and this causes more accurate results. We can apply it in different domains of anomaly detection. In fact it is a generic method for anomaly detection and needs small changes for implementing of different domains.

Design a model for thought structure Time Road: A Mental model for temporal concepts

By: Meisam Ahmadi
Supervisors: Dr. Ali Moeini, Dr. Kambiz Badie

Defense room: Engineering Science 1
Committee: Dr. Dara Moazzami, Dr. Mehrnoosh Shams Fard
Date: Thursday, October 1, 2009

Abstract: There are serveral methods for interaction betwean human and computer in order to transfter temporal concepts. This thesis, with more emphasis on human sides of interaction, represents a new model which tries to achieve a better understand of events in sequences for user called Time Road.
The Time Road model, is inspired by the logaritmic nature of human mental models to look at a path and is trying to get different properties to create common sense with events in the user mental model. this specification in the form of laws can be seen in the final architecture.
Also there are some descriptions of general method to reach a new model of interaction betwean human and computer with emphasis on the cognitive effects. Some paragraphs are used for showing the lack of attention paid for mental models of users.

Keywords: Mental model, timeline, temporal data, HCI design

An assimilating algorithm for recovery and abandoning two dimentional maovment

By: Mir shahab edin razavi hesabi
Supervisors: Dr. Dara Moazzami
Co-advisor: Dr. Mehrdad Shahshahani

Defense room: Engineering Science 1
Committee: Dr. Ali Moeini, Dr. Niloufar Gheysari
Date: Saturday, October 3, 2009

Abstract: Because of potential application and nature complexity, smart recovery and analyses of human being movement is one the important research filde and include lot’s of difficulties according to definition on mood deduction and movement of a tridimentional , non – rigid and jointed objective.
Different application in this filde could be categorized in three group such as:

  1. monitoring application; Include some classical issue that related to smart minitoring and understanding about very crowded place like airport and subway.
  2. controlling application; Include instrument control at the time of movement evaluation of mood parameters.
  3. Analytic application; Include smart distinguish orthopedic diseases of analyse and optimize of sport man effectiveness.

According to importance of investment in this filde for development and research, Initial model on base of suggested models classification, Primiry quantification which defined as “reliability of self – functional movement, that would starting with multilateral ubderstanding of present sence in place”, principle of modeling would be as follow:

  • following, classification and pursue of human being in one or several moods.
  • Position evalvation in one or several moods.
  • Recognization, clarification of human being. Identity and also activity that done by one or many people.

Formal Specification and Verification of a Cardiac Pacemaker Using Z and NModel

By: Peyman Faizian
Supervisors: Dr. Ali Moeini , Dr. Dara Moazzami

Defense room: Engineering Science 1
Committee: Dr. Kambiz Badie, Dr. Mohammad Reza Meybodi
Date: Saturday, October 3, 2009

Abstract: Considering the life critical nature of the medical devices and the complexity of the software used in them, reliable and error-free design of such systems is highly valuable. Therefor a mechanism to prove the correct function of the software along its correspondence with the project requirements seems necessary. To fulfil this, group of mathematical techniques, namely formal methods, are used to specify, develop and verify softwares.
In this thesis, we are going to specify a cardiac pacemaker using formal methods and their related tools. First we formally specify the informal requirements document using Z language. Then we use the Z/Eves tool for syntax checking, domain checking and type checking of the specifications. Using the refinement techniques and structural similarity between the Z and NModel frameworks, we transform the model to the NModel framework. NModel is a framework based on C# and .NET which facilitates most of the model checking and verification processes. Finally we explore the resulting model, using NModel, and check the safety and liveness properties as a part of verification process.