Dr. Seyed-Hassan Mirian Hosseinabadi
Recent Students:


Hassan Haghighi (PHD)


Behnaz Changizi (MS)


Javad Taghizadeh Naeini (MS)


Mohammad Sadegh Makarem (MS)
  Mehran Rivadeh (MS)
  Seyed-Shobeir Fakhraei (MS)
  Hessam Chiniforooshan (MS)
  Elmira Movahedi Mehr (MS)
  Hassan Shojaeemend (MS)
  Amir Hossein Assiaee (MS)
  Amir Jahangard (MS)
  Neda Noroozi (MS)
  Ali Hajizadeh Moghadam (MS)
Previous Students
  Research Topics
  Formal Methods
  Software Architecture
  Software Development
  Data Base
Special Events
  Invited lecturer Dr. Maryam Tehrani
Subject: A Distributed and Flexible Workflow Management System
  Upcoming MS Students Seminars
24th & 31st Dec. 2005
  Formal Methods

  Title: NCZ: Non-deterministic Constructive Z  
    Hassan Haghighi (PHD Candidate)  

  Title: Developing executable Program from formal specification in Z  
    Behnaz Changizi

  Abstract: Formal specification is a precise way for stating system requirement. There are some specification languages with a strong mathematical base, but their disadvantage is their difficulty to understanding for user. At the other side we have prototyping to validating user requirement, a comfortable way to deal with user. The purpose of this research is establishing an automatic method to translate formal specification to its prototype.  

  Title: Test Case Generation from Formal Specification  
  Javad Taghizadeh Naeini


  Abstract: Software testing is important activity in the software development Life cycle for checking the correctness of system implementations. Software testing requires test case that usually done manually from specification (formal or non formal) and is laborious, manual and error-prone and takes too much time and too many efforts. The use of formal system specifications makes it possible to automate the derivation of test cases from specifications. Using formal methods in the software development trajectory is very beneficial in the testing phase. These benefits are due to the clarity, preciseness, consistency and completeness of formal specifications, which make that test cases can be efficiently, effectively and systematically derived from the formal specifications. The use of formal system specifications makes it possible to automate the derivation of test cases from specifications. Various approaches have been proposed for automated test case generation such as FSM, ASML, SDL, Lustre, LIS, JML and UML. At this Project, We focus on the Automatic test case Generation From Formal Method and at the end of this research, we present a tool for test case generation from Z Specification.  

  Title: A tool for Executing Lambda Calculus Programs  
  Mehran Rivadeh


  Abstract: A calculus is a notation that can be used mechanically for some calculating purposes, because the rules can be use mechanically and can be define explicitly they can be executed by computers. Some of calculus's with respect to computability theorem are the same as any computer for instance we can remember markov algorithms or lambda calculus. The importance of lambda calculus is it's executablity. The purpose of this project is executing expressions of lambda calculus.  

  Title: User Interface Design: A Formal Approach  
  Amir Hosein Asiaee


  Abstract: User interface is one of important components of today's systems; they have to be built in the way which we can assure important properties of GUIs, such as consistency can be verified. Therefore, we need strong methods for specification and design GUIs. So formal methods are appropriate candidate for this reason. Our effort is to find important properties and structure of GUIs and find a way to specify them by a formal language such as Z, this might need to expand Z notation. By this we can find a way to verify these properties and build robust GUIs.  

  Software Architecture

  Title: Formal verification and Specification of Software Architecture Properties  
  Mohammad Sadegh Makarem


  Abstract: From a general view point, Software Architecture consists of software elements and relationships between them and their externally visible properties. Software elements (sometimes we call them components) contain data and functionality of system. Software architecture should cover system functionality as well as its non-functional requirements. The way that architecture support non-functional (quality attributes) and functional requirements determines Software Quality. Software Architecture Verification is an approach to support and evaluate software quality. This project aims to define an approach to formal specification and verification of software architecture in order to verify it against architectural properties. This approach helps architect to evaluate properties of software architecture in a formal way; these properties include performance, availability, security and more. Modeling architecture and architectural properties is a key task for this verification. We intend to use model checking mechanisms to perform these verifications.  

  Title: Dynamic Architecture of Software: An Aspect Oriented Approach  
  Elmira Movahedi Mehr


  Abstract: Software applications executing in highly dynamic environments are faced with the challenge of frequent and usually unpredictable changes in their execution environment. In order to cope with this challenge effectively, the applications need to adapt to these changes dynamically. In such cases evolution is almost impossible to predict at the design stage. Also throughout the lifetime of a software system or architecture, new requirements may arise that will require the existing system to be altered or evolved in someway. Therefore an effective mechanism for evolution is an important factor in the creation of software systems.
To alleviate the above problems, aspect architecture which can be seen as a software architecture view type proposed which provides an aspect-oriented perspective on software architecture. In an aspect architecture the aspects serve as building blocks. They can be seen as LEGO bricks that can be composed to form more complex aspects incrementally from simpler sub-aspects. Each concern is addressed in a modular way by a collection of aspects, which can be composed when needed.

  Title: An Efficient Query Processor for Data Integration in the p2p Architecture Environment  
  Hassan Shojaee


  Abstract: Data integration is the problem of combining data residing at different sources, and providing the user with a unified view of these data. Most of the formal approaches to data integration refer to an architecture based on a global schema and a set of sources. As observed in several contexts, this centralized architecture is not the best choice for supporting data integration. A more appealing architecture is the one based on peer-to-peer systems. In these systems every peer acts as both client and server, and provides part of the overall information available from a distributed environment, without relying on a single global view.  

  Title: Reconfigurable Software Systems Specification and Verification: An Approach Based on Adaptive Architecture  
  Neda Noroozi


  Abstract: Software systems executing in highly dynamic environments are faced with the challenge of the usually unpredictable changes in their contextual conditions. Having an adaptive behavior in these systems is necessary in order to cope with the mentioned challenges effectively.
In this project we will use dynamic reconfiguration methods in architecture level as a solution for constructing adaptable systems. Our focus will be on the following subjects:
  * Requirements and attributes of reconfigurable systems
  * architectural issues in reconfigurable systems

  Software Development

  Title: Aspect Extraction from Software Design Model  
  Seyed Shobeir Fakhraei


  Abstract: Aspects crosscut the system s basic functionalities. Present methodologies in software engineering fail to support aspects .There are a lot of researches about aspect-oriented techniques but most of them have concentrated on the coding phase in software life cycle. This project is going to present a set of techniques to cover the design phase of software producing life cycle.  

  Title: An Agent Oriented Workflow Management System  
  Hesam Chiniforooshan


  Abstract: Workflow Management System (WFMS) is an enabling technology for the integration of process oriented tasks. Concerning the distribution of information and applications in current world, orchestration and completion of these tasks might be more efficient if there exists an autonomous infrastructure within the architecture of WFMS. We believe that an Agent Oriented WFMS can effectively support such requirement and we are going to elicit common aspects of WFMSs which have the potential of being agent enhanced.  

  Title: A Model for Software Reliability Evaluation for Distributed Web Applications  
  Ali Hajizadeh Moghadam


  Abstract: IEEE: "Software Reliability is the probability that software will not cause a failure for a specified time under specified conditions." In this project, we are studying different approaches to software reliability to adopt them for distributed web applications.  

  Data Base

  Title: Mapping Between Relational Database Schemas and XML Schemas  
  Amir Jahangard


  Abstract: In recent years XML has emerged as a standard for formatting data on Internet. Use of XML as a common format for presentation, transfer, storage and accessing data introduces new challenges to database systems. Since most of data is stored and maintained in relational database systems, we expect that the need for mapping between relational schema and XML schema increases more than before. So far several algorithms have been proposed to do this mapping. Although this algorithms work good in their specific applications, they just consider the structure of the source schema and most of them ignore conceptual constraints. In this project we will study the existing mapping algorithms and will try to extend them (or introduce a new algorithm) so that it becomes possible to preserve some conceptual and integrity constraints. Then we will implement the proposed method and evaluate responsiveness of the result schema in compare with the source schema.  

Sharif University of Technology
Computer Engineering Department
Software Quality Research Laboratory
Room 211 - CE Dep. - Azadi Ave. - Tehran -Iran

By: A.H. Assiaee 2005-2006