|
The Distributed Systems Analysis team is involved in research and
development activities that span the following main research areas:
Pattern Based Analysis of Distributed Systems
Pattern based techniques have become widely adopted in the system development process. The team
uses the concept of predefined properties and error descriptions, which was introduced in the
context of program validation and error detection, to help reduce the cost and complexity in
debugging and validating distributed applications. This research includes several directions:
Automated Framework for Trace Analysis of Distributed Systems
The trace analysis framework is developed for the analysis of distributed applications based on
their execution traces (logfiles) generated at runtime. According to this framework, formal models
are first built from collected traces and then checked against user defined properties that specify
functional and non-functional requirements.
The results of this ongoing collaboration with
Siemens AG (since 2001)
include a toolset featuring trace modeling components that extract models from different types of
traces (e.g., traffic control systems and GSM/GPRS/UMTS systems), a pattern-based property
specification library (80 common patterns), an off-the-shelf model checking tool, and a friendly
user interface.
Model Checking based Validation of Web Applications
The goal of this internal research project is to automate properties verification in Web
Applications. A prototype verification environment is implemented in which a browsed Web
application is represented by an automata model and verified (using the SPIN model verification
tool) against user-defined properties using the model checker Spin.
Static Analysis of Multithreaded Java Programs
The team addresses the problem of identifying sources of deficiencies in multithreaded Java
applications. Typical code structures that can cause deficiencies in the code of a multithreaded
Java application are documented in a library of
38 antipatterns. A practical
classification of antipatterns is proposed and detection modules for several antipatterns are
implemented. This project is supported by
SAP.
Dynamic Analysis of Multithreaded Java Programs
The goal of this internal research project is to apply dynamic analysis techniques in
multithreaded programs to complement the analysis performed by static techniques in detecting some
complicated deficiencies (antipatterns). An antipattern detection framework based on dynamic
approaches, as well as supporting tools based on a formal verification technology (model checking)
and automata observers are developed and evaluated.
Model Based Testing Methodologies
Model based testing methodologies enable automating, improving, and reducing the cost of testing
activities by the use of models, which are partial, abstract representations of
functionalities, behaviour, architecture, and data of the system under test. The team also
investigates test and fault models to further improve the quality of testing. This research
includes the following directions:
Automated Test Adaptation for Changing Business Applications
Software inevitably changes. In particular, business applications are constantly modified to
stay in pace with demands and structural changes. The most affected phases in the software
development lifecycle are testing and validation, which are complex by default, especially for
large complex business applications.
In collaboration with
SAP, the team addresses the problem of
improving the testing process while taking into consideration the continuous changes an application
undergoes. It develops an automated framework for test adaptation in which it uses model based
techniques for change detection and test adaptation.
(H3)Test Verification in Model Based Testing
Testing distributed systems has never been easy, while the quality of tests is crucial for the
effectiveness of testing activities for such complex systems under test. At the same time, tests
for distributed systems are in most cases developed manually and may contain flaws and
inconsistencies, especially in absence of any formal model of the system under test.
In collaboration with
Siemens AG, the team is
elaborating a framework, including methods and prototype tools, for automating test verification
activities.
Test Generation for Distributed Systems
In collaboration with
France-Telecom R&D, the team investigated automatic
test generation from specifications of distributed systems using formal verification techniques
(model-checking). It uses a general model, a system of Communicating Extended Finite State Machines
(CEFSM), which combines both control flow and data and is used for test generation. The proposed
techniques combine both specification and fault coverage.
Model Based Testing
The main objective of this research project funded by
NSERC is to contribute to the
development of new methods and technologies to test distributed systems, which takes into account
concurrency, non-determinism, and asynchronous communications.
Software Security
The team designs systems to ensure security of computer networks and their users. Our work
concerns three aspects: formal verification of software security, design of intrusion prevention
and detection systems, and the personal protection of users.
Model Checking Role Based Access Control in Business Scenarios
In collaboration with
SAP, the team developed a formal
approach for the validation of role based access management systems. An Extended Finite State
Machine is used to represent business scenario (workflow) along with access control rules. The Spin
model-checker is used to verify various security properties (such as separation of duties).
Secure Agent Based Distributed System
In collaboration with
SecureOps and ReactSys, the
group developed approaches for the design of distributed architectures, which enable real time
detection and prevention of attacks. These architectures are based on a model of non-mobile
cooperative agents capable of inferring intentions of potential intruders.
Content based WWW Access Filtering
In collaboration with
FokusMedia, the team
investigated a World Wide Web access filtering model dedicated to prevent users from browsing
certain Web sites. It proposed a novel transparent architecture which relies on collaboration with
the DNS service and a filtering of Web pages based on their content.
Development of Intelligent Distributed Computing Systems
The team investigates and develops intelligent distributed computing systems, systems for
automated planning with contingencies, and systems for time scheduling. The research venues
explored in these projects are related to the fields of Multi Agent systems, Peer-to-Peer systems
and artificial intelligence.
Platform for Online Distributed Applications
In collaboration with
TEC, the group investigates a
software platform for secure software distribution. Two aspects are considered:
- the host of the software is protected against possible harmful behaviour of the software
itself
- the software is executed in a protected environment ensuring code integrity and preventing
non-authorized redistribution of the software
The use of online software distributed through the platform is monitored, for instance, in order
to provide billing information.
Automated Planning
In this project, in collaboration with
Defence R&D Canada (DRDC), the
team investigates contingency planning systems. The performance and limitations of existing systems
are studied and an alternative approach, based on formal methods, is proposed.
School Timetabling
The project, supported by the
School board of
Laval and realized in collaboration with CRIM’s Development and Internet Technologies team,
concerns the automatic production of schedules (timetables) for the high schools of Quebec. The
generation of schedules takes into account the particularities of schools (number of students, size
of the school, etc.), courses, professors’ preferences, and student choices along with a set of
global requirements.
Static Analysis of Software
Static analysis of software relies mainly on the availability of the source code and as such
enables the analysis of a software outside of its execution environment.
Program Inspection and Diagnosis through Code Analysis
Low quality design and implementation produce error-prone software that is hard to understand
and maintain. Dedicated measures are always needed to validate both the design and the
implementation.
Such measures include analyzing the source code and detecting flaws in it. Flaws are usually
violations of design principles, quality heuristics and code conventions commonly adopted in the
software development community. In addition, various metrics could be collected to provide
quantitative assessment of code quality.
Detecting Migration Related Problems in Java Programs
In collaboration with
SAP, the team studied the problems
related to migrating from Java 1.4 to Java 1.5. It documented most common problems that could
result from the migration. In addition to classifying the identified problems into practical
categories, the group developed a set of detectors to identify the problems in the code and
proposed guidelines and tips to developers to avoid such problems.
|
