|
|
|
| |
Formal Methods |
 |
|
| |
Title: NCZ: Non-deterministic Constructive Z |
|
| |
|
Hassan Haghighi (PHD Candidate) |
|
|
|
|
| |
Title: Developing executable Program from formal
specification in Z |
|
| |
|
Behnaz
Changizi
behnaz_changizi@yahoo.com |
|
| |
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 |
|
|
taghizadn_j@yahoo.com |
| |
| |
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 |
|
|
mehran_rev@yahoo.com |
| |
| |
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 |
|
|
a_assiaee@ce.sharif.edu |
| |
| |
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 |
|
|
makarem@ce.sharif.edu |
| |
| |
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 |
|
|
emovahedimehr@yahoo.com |
| |
| |
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 |
|
|
hassan_shojaie@yahoo.com |
| |
| |
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 |
|
|
noroozi@ce.sharif.edu |
| |
| |
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 |
|
|
shobeir@gmail.com |
| |
| |
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 |
|
|
http://ce.sharif.edu/~chineeforoushan/ |
| |
| |
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 |
|
|
ali.moghadam@gmail.com |
| |
| |
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 |
|
|
ajr1360@yahoo.com |
| |
| |
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. |
|
|
|
