February 2014 Edition – Vol.6 no.2

SIGNAL is the main monthly information medium of the Microsystems Strategic Alliance of Québec (ReSMiQ). This newsletter aims to be an active link between the members of ReSMiQ and all individuals who have an interest in research and innovation in microsystems. We commit ourselves to promote in it our members’ research and increase ReSMiQ’s visibility.

ReSMiQ is a group of researchers in an interuniversity research center that can count on the support of the Fonds de recherche du Québec – Nature et technologies (FRQNT) and ten (10) Quebec universities involved in microsystems research.

In this issue we present you the news for the month of February 2014.

New format for SIGNAL – As more and more web user are browsing on mobile platforms such as digital tablets and smart phones, we decided to renew the format of our monthly newsletter SIGNAL for a more user-friendly reading. Do not hesitate to send us any comments that could help us improve the quality.

Seminar – Dr. N. Luvig from the Department of Neurology at the NYU Langone Medical Center was in Montreal where he presented a seminar at the Ecole Polytechnique de Montreal organized by the Polystim Lab at Polytechnique Montréal and ReSMiQ. The seminar entitled “Subarachnoid Pharmacodialysis Implant for cerebral cortical disorders” was attended by about 25 graduate students.
See the abstract.Ludvig

Rong2

Intensive course –  Dr. G. Rong from the Shanghai Jiao Tong University was in Montréal where he presented an intensive course entitled “Label free biosensors and applications in frontier research” at the Ecole Polytechnique de Montreal, organized by Montreal Chapter of the IEEE Solid State circuit society (SSCS) and ReSMiQ.
See the abstract.

NEWS FROM OUR MEMBERS

Achievement
– Dr. Fréchette from Université de Sherbrooke and Dr. Peter from Polytechnique Montréal are co-recepient of a Collaborative research and develpment grant from NSERC with a contribution from PROMPT and Teledyne DALSA.

– Dr. Martel from Polytechnique Montréal supervised Dominic Lanauze in the biomedical ingineering program, recipient of the best master thesis award.

Involvement
– Dr. Sawan from Polytechnique Montréal is the technical program co-chair of the International Humanitarian Technology Conference (IHTC) to be held in Montréal from June 1 to 4, 2014.

jir2014

NEWCAS2014

RESMIQ’S ACTIVITIES

To stimulate integration of new students within the affiliated laboratories of ReSMiQ holds annually a financial support competition for undergraduate full time students.

Characteristics
– Duration of three (3) months.
– Starting May 1, 2014.
– 2000$ for the whole duration.

Application information
Applications must be received at ReSMiQ’s administrative office on April 7, 2014 at the latest. Applications must be submitted in PDF format via the online submission page.
Details about eligibility and application

Posted in Uncategorized

UPCOMING CONFERENCES

Call for contributions

XXXIII  Conference on design of circuits and integrated systems (DCIS),
from November 14 to 16, 2018, Lyon, France.
Submission deadline : May 1st, 2018.
More details

IEEE Biomedical Circuits and Systems Conference (BioCAS2018),
from October 17 to 19, 2018, Cleveland, U.S.A.
Submission deadline : June 11, 2018.
More details

IEEE Life Science Conference (LSC2018),
from October 28 to 30, 2018, Montréal, Canada

Submission deadline : June 4, 2018.
More details

Call for participation

31st Canadian Conference on Electrical & Computer engineering (CCECE),
from May 13 to 16, 2018, Québec, Canada.
More details

2018 International Symposium on Circuits and Systems (ISCAS),
from May 27 to 30, 2018, Florence, Italy.

More details

16th IEEE International NEWCAS Conference (NEWCAS),
from June 24 to 27, 2018, Montréal, Canada.
More details

The 31st International Conference on Industrial, Engineering & Other Applications of Applied Intelligent Systems (IAE-AIE2018)
Du 25 au 28 juin 2018, Montréal, Canada.
More details

61st IEEE International Midwest Symposium on Circuits and Systems (MWSCAS),
from August 5 to 8, 2018, Windsor, ON, Canada.
More details

MEMBER PROFILE

Prof. O. Ait Mohamed
Concordia University
Regular membre of ReSMiQ since 2002

Professor Mohamed Ait Otmane received the Ph.D. in Computer Science from the University Henri Poincaré, Nancy I, France. He worked in research and development at Cistel Technology and Nortel Network, Ontario, Canada. He is associate professor in the department of Electrical Engineering and Computer Science at Concordia University. He has published several works on the development of techniques and tools that improve the usefulness of formal verification for the analysis and verification of large systems. More information

Below is a selection of publications in recent years followed by a representative paper of his work.

S. Ouchani, O. Ait Mohamed, and M. Debbabi, "A property-based abstraction framework for SysML activity diagrams," Knowledge-Based Systems, vol. 56, pp. 328-343, 2014.

S. E. Abed, O. Ait Mohamed, and G. Al Sammane, "Automatic verification of reduction techniques in Higher Order Logic," Formal Aspects of Computing, vol. 25, pp. 971-991, 2013. (résumé ci-dessous) / (abstract below)

S. Ouchani, O. Ait Mohamed, and M. Debbabi, "A Probabilistic Verification Framework for SysML Activity Diagrams," New Trends in Software Methodologies, Tools and Techniques, vol. 246, pp. 108-123, 2012.

Fermas, A. Belouchrani, and O. Ait-Mohamed, "Floating-point scaling technique for sources separation automatic gain control," International Journal of Electronics, vol. 99, pp. 995-1004, 2012.

I. Ahmed, S. H. Rahman, O. Ait-Mohamed, and S. E. Abed, "Towards an FPGA implementation and performance evaluation of a digital carrier synchronizer with a portable emulation environment," International Journal of Computer Applications in Technology, vol. 45, pp. 66-76, 2012.

S. E. Abed, K. Hussain, and O. Ait-Mohamed, "Abstract property language for MDG model checking methodology," International Journal of Computer Applications in Technology, vol. 44, pp. 23-36, 2012.

RESEARCH CONTRIBUTIONS

AUTOMATIC VERIFICATION OF REDUCTION TECHNIQUES IN HIGHER ORDER LOGIC

E. Abed, O. Ait Mohamed, and G. Al Sammane. Formal Aspects of Computing, vol. 25, pp. 971-991, 2013.

In this paper the authors propose an automatic methodology to verify the soundness of model checking reduction techniques. The idea is to use the consistency of the specifications to verify if the reduced model is faithful to the original one. The user provides the reduction technique, the specification and the system under verification. Then, using Higher Order Logic he verifies automatically if the reduction technique is soundly applied. The method is completely defined in an MDG-HOL special integration platform that combines an automatic high level model checking tool Multiway Decision Graphs (MDGs) within the HOL theorem prover. We provide two case studies, the first one (Fig.1) is the reduction using SAT-MDG of an Island Tunnel Controller and the second one (Fig. 2) is the MDG-HOL assume-guarantee reduction of the Look-Aside Interface. The obtained results of our approach offer a considerable gain in terms of the correctness of heuristics and reduction techniques as applied to commercial model checking, however a small penalty is paid in terms of CPU time and memory usage.

Fig. 1. Overview of the SAT–MDG reduction methodology

Fig. 2. Overview of the MDG-HOL assume-guarantee reduction methodology