In this project The Laboratory Information Management System (LIMS) will be formally modelled using the latest standard approved by OMG. The model will be verified and analysed using a combination of Model-driven testing techniques and formal verification techniques. A set of critical test cases will be obtained out of the model. This set of test cases will be executed on any implemented LIMS with equivalent specifications to the modelled one. It is enough for the tested system to successfully finish the execution to be completely verified.

This project is in collaboration with Garmen Laboratory, Montreal, QC.

Objectives :
 * Study of sources separation algorithms and their adaptation to hardware implementation,
 * Realization of a platform for design and automatic implementation of VLSI architectures,
 * Verification and evaluation of implementations performances.

In the coming years, information technology will continue to transform the way we think, work, communicate, and learn. The tremendous success of Internet-related technologies (web services, voice over IP, mobile telephony, etc.) coupled with advances both in hardware and software will invigorate the existing proliferation of software intensive systems. This will allow for new services, applications and systems that will recede increasingly into the background of our lives. In this setting, the secure engineering of such software-intensive systems becomes a major concern. This is emphasized by the fact that security breaches of software systems keep appearing at an alarming rate in spite of numerous updates and patches that are constantly being issued.
 
The primary intent of this research is to contribute to the secure engineering of software-intensive systems. To this end, we envision extending current Model Driven Architecture (MDA) paradigms and prominent modern modeling languages, such as the Unified Modeling Language (UML), in order to address security concerns throughout the development lifecycle. This choice is motivated by the wide acceptance of these methods in industry and academia due to their expressiveness, easiness and tool support. In this research, the targeted security concerns are: capturing security requirements, specification and design of security mechanisms, verification and validation of security properties/policies, and automatic generation of secure code. Appropriate security profiles and UML language extensions will be used in the capture of security requirements as well as the specification and design of security solutions.
 
For the purpose of verification and validation, we will automatically derive new semantic models from UML specifications and subject them to verification techniques against a-priori defined security policies. A significant objective of this research is to systematically generate secure code from the extended design models using aspect oriented programming techniques. Finally, we intend to leverage the obtained research results to the de facto language for system engineering i.e. System Modeling Language (SysML).

This project is co-supervised  by Dr. Mourad Debbabi.

The goal of the project is to propose a model checking methodology using a rewriting based SAT solver to prune the transition relation of the circuits to produce a smaller one that is fed to the model checker. In fact we will be using the specification of the design provided as properties to extract a reduced model that will be verified by a model checker tool. We will test our reduction methodology using challenging industrial benchmark in order to compare results with commercial model checking tools..

The hardware designs that described at register transfer level (RTL) have become more complex and difficult to debug. Therefore, using Multiway Decision Graphs (MDGs) the same designs can be defined into more abstract environment. However, to avoid the state explosion problem the MDGs-based designs still need to be reduced. Moreover, all the backward reduction algorithms cannot be used in MDG, due to the presence of abstract state variables. The main feature of this project is to study this problem and propose new reduction techniques in order to deal with the MDGs-based designs.

An Implantable Wireless Body Sensor Network (IWBSN) is a wireless network of smart sensor nodes (worn by or implanted in subject’s body), each capable of collecting the information from the body (like; Temperature, blood glucose, blood pressure, ECG, etc…), processing and wirelessly transmitting such physiological information to a local Base Station (BS) outside the body. The size of an implantable sensor node, with respect to the tiny battery included in the node and therefore its power consumption are the major challenges in the design of implantable IWBSNs. A network of biosensors is fundamentally different from other wireless networks. Although advances in semiconductor technology have made it possible to build miniature and reliable biosensors containing enough low power ADCs and microcontrollers, nevertheless, the current technology of the transceivers even using the most efficient standard communication protocols is still suffering from consuming the big portion of the very small energy source available in the tiny sensor nodes. The battery life time of such implanted sensor nodes inside the body varies from a few days to a few weeks and requires going through chirurgical operations each time the battery needs to be replaced. Even technology of RFIDs is not yet known as a solution because of the coil size and also big amount of radiation against the body. This energy constraint leads us to innovate and introduce a new energy-efficient system. This work is to propose a new ultra light weight communications protocol for the IWBSN applications to eliminate energy wasting in the communication protocol process through the transceivers by keeping them in sleep mode for the longest possible portion of the time and sending the data with minimum activities. The proposed protocol allows the battery to last significantly much longer even for years with a higher throughput in power saving avoiding the high risk chirurgical operations to replace the batteries very often.