· Khaza Anuarul Hoque, O.Ait Mohamed, Sa’ed Abed and Mounir Boukadoum, “SAT Based Model Checking for MDG Models”. The 8th IEEE International NEWCAS Conference, Montreal, Canada, June 20-23, 2010, pp. 241-244, (Best Paper Award), [4 pages].

· Sa’ed Abed, Otmane Ait Mohamed, Zijiang Yang and Ghiath Al Sammane, "Integrating SAT with Multiway Decision Graphs for Efficient Model Checking", In Proc. IEEE International Conference on Microelectronics (ICM’07), Egypt, Dec. 29-31, 2007, pp. 129-132, [4 pages]. 

·              Reduction Techniques for Multiway Decision Graphs (MSDs):

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.

Publications:

Conference Papers

· Sa’ed Abed and Otmane Ait-Mohamed, "MDGs Reduction Technique Based on the HOL Theorem Prover", The 40th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2010), Barcelona, Spain, May 26-28, 2010, pp. 15-20, [6 pages].

· Ghiath Al Sammane, Sa’ed Abed and Otmane Ait Mohamed, "High Level Reduction Technique for Multiway Decision Graphs Based Model Checking", First International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2007), Algeria, May 5-6, 2007, pp. 1-14, [14 pages].

· Sa’ed Abed, Otmane Ait Mohamed and Ghiath Al Sammane, "Multiway Decision Graphs Reduction Approach based on the HOL Theorem Prover", In Proc. Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS'08), The British Computer Society, Leeds, U.K, July 2-3, 2008, pp. 17-26, [10 pages].

· Sa’ed Abed and Otmane Ait-Mohamed, "MDGs Reduction Technique Based on the HOL Theorem Prover", The 40th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2010), Barcelona, Spain, May 26-28, 2010, pp. 15-20, [6 pages]. 

Technical Reports

· Sa’ed Abed and Otmane Ait Mohamed, "HOL based Reduction Techniques for MDGs Model Checking", Technical Report 2008-1-Abed, Department of ECE, Concordia University, Montreal, Canada, Jan. 2008.

·              Processing APL Properties to Generate Verification-Ready MDG Model:

Multiway Decision Graphs (MDGs) are special decision diagrams that subsume Binary Decision Diagrams (BDDs) and extend them by first-order formulae suitable for model checking of datapath circuits. In this project, we propose a new specification language, Abstract Property Language (APL), for the MDG model-checker. The APL language eradicates the restrictions present in the existing LMDG specification language and introduces new operators to improve expressiveness. The project also presents the design of a front-end translator that accepts specification in APL and builds composite MDG model with the specification directly embedded into its MDG-HDL representation. Finally, some experimental results are presented to show the performance of the APL-Tool and the analysis of the generated code executed on benchmark properties.

Publications:

Conference Papers

· Kamran Hussain, Otmane Ait Mohamed and Sa’ed Abed, "Processing APL Properties to Generate Verification-Ready MDG Model", In Proc. of the 21th IEEE International Conference on Microelectronics (ICM’09), Marrakech, Morocco, Dec. 19-22, 2009, pp. 260-263, [4 pages].

·              A New Approach for the Construction of Multiway Decision Graphs:

Multiway Decision Graphs (MDGs) are a canonical representation of a subset of many-sorted first-order logic. It generalizes classical BDDs with abstract data and uninterpreted functions. In this project, we describe a new MDG construction based on the Generalized- If-Then-Else (GITE) operator. Consequently, we review the main algorithms used for verification techniques i.e. relational product and pruning by subsumption. Unlike an earlier version of the MDG package, basic MDG algorithms are defined uniformly through this single GITE operator which will lead to a more efficient implementation. The new tool, called NuMDG, accepts an extended SMV language, supporting abstract data sorts.

Publications:

Journal Papers

· Sa’ed Abed, Y. Mokhtari, Otmane Ait Mohamed and S. Tahar, " NuMDG: A New Tool for Multiway Decision Graphs Construction", Journal of Computer Science and Technology (JCST), Springer New York, Vol. 26, No. 1, pp. 139-152, Jan. 2011, DOI 10.1007/s11390-011-1117-8, [14 pages], IF: 0.632). 

Conference Papers

· Y. Mokhtari, Sa’ed Abed, Otmane Ait Mohamed, S. Tahar and X. Song, "A New Approach for the Construction of Multiway Decision Graphs", In Proc. 5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08), Lecture Notes in Computer Science, Istanbul, Turkey, September 1-3 ,2008, pp. 228-242, [15 pages].

Technical Reports

· Sa’ed Abed, Y. Mokhtari, O. Ait Mohamed and S. Tahar, " A New Approach for the Construction of Multiway Decision Graphs", Technical Report 2008-3-Abed, Department of ECE, Concordia University, Montreal, Canada, June 2008.

2. Fault Tolerance and Reliability

·              Reliability of Recursive Concentrator Structure:

The inverse omega network possesses various attractive properties and its constituent node has a fixed degree independent of the system size. In this project, a proof for a technique applied recursively to construct an N-input concentrator switching network which is similar in topology to the inverse omega network will be introduced. Also an examination of a reliable inverse omega network in the presence of any single node failure will be presented. The new configuration of the system ensures providing the same high performance results obtained before the failure. In this project, we show how to check the passibility by the inverse omega network of any given connection set and list some of the general patterns passable by this network. We also show that the concentrate operation passable by the inverse omega network is just a special case of the more general alternate sequence operation.

Publications:

Conference Papers

· Sa’ed Abed, Sahel Alouneh and Otmane Ait Mohamed, “Reliability of Recursive Concentrator Structure", In Proc. IEEE Symposium on Industrial Electronics & Applications (IEEE ISIEA'09), Kuala Lumpur, Malaysia, October 4-6, 2009, pp. 136-141, [6 pages].

· Sahel Alouneh and Sa’ed Abed, “Fault Tolerance and Security Issues in MPLS Networks”, In the Proceedings of the 10th WSEAS International Conference on Applied Computer Science (ACS 2010), Iwate, Japan, October 4-10, 2010, pp. 134-138, [5 pages].

· Sahel Alouneh, Sa’ed Abed, Bassam Jamil Mohd and Ahmad M Al-Khasawneh, “Relational Database Approach for Execution Trace Analysis”, In Proc. of the IEEE International Conference on Computer, Information and Telecommunication Systems  (CITS 2012),  Amman, Jordan, May 14-16, 2012, pp. 1–4, 2012, [4 pages]..

3. Distributed Virtual Memory

·              A Novel Approach to Enhance DVM (Funded by Hashemite University: 1,500 USD)

Distributed Virtual Memory (DVM) has been introduced in many researches and models. The idea of this technique was inspired from the comparison between data transfer time in RAM system and the Hard Disk system especially in small networks with many nodes, the usage of such technique results in higher utilization for the whole system and an increased throughput. In this project, we address some practical issues of DVM and present a methodology for managing the virtual memory which outperforms pervious DVM models. In particular, a distributed algorithm for DVM management to detect the memory status and hence to enhance previous DVM techniques is introduced. The DVM data structure tables are similar to those found in current Conventional Virtual Memory (CVM) operating systems with some modifications. The methodology includes Address Translation, Page Out policies and Page Replacement. Finally, we evaluate the performance of our methodology through several test benches made under different system loads, and compare it with the pervious practical DVM and CVM techniques to show the efficiency of our approach. The results have shown that the page faults have been decreased by a considerable gain of 15% and 25%, respectively.

Publications:

Journal Papers

· Sa’ed Abed, Ashraf Hasan Bqerat, Sahel Alouneh and Bassam Jamil Mohd, " A Novel Approach to Enhance Distributed Virtual Memory", Computers and Electrical Engineering, Vol. 38, issue 2, pp. 388-398, Elsevier, DOI: 10.1016/j.compeleceng.2011.11.006, March 2012, [11 pages], (IF: 0.526).  

Conference Papers

· Sahel Alouneh, Sa’ed Abed, Ashraf Hasan Bqerat and Bassam Jamil Mohd,“A Methodology for Distributed Virtual Memory Improvement”, In Proc. of the Informatics Engineering and Information Science (ICIEIS 2011), Kuala Lumpur, Malaysia, Nov. 14-16, 2011, Part III, Communications in Computer and Information Science(CCIS), Springer-Verlag Berlin Heidelberg, Vol. 253, pp. 378–384, 2011, [7 pages].

4. FPGA Implementation (Total Fund by Hashemite University: 245,000 USD) 

·              FPGA-Based Steganographic Processor (Funded by Hashemite University: 15,000 USD)

Steganography is the science of hiding a secret message in a carrier message without being detected. No one is aware of the existence of the secret message except the sender and the intended receiver. Steganography differs from cryptography by the fact steganography hides the secret message, whereas cryptography encrypts the information. In this aspect, steanography is superior compared with cryptography as steganography does not raise the suspicion of ongoing communication since it is hidden. Steganography applications spans from civilian to military and even terrorism. In the military applications, digital data flowing on the internet is a prime target for embedding secret command communications amongst the military units without alerting the enemy with suspicious moves.

In this research, our goal is to implement a stegnography processor using FPGA system to embed and extract messages in real-time. The need for dedicated hardware stems from the fact that stegnographic techniques that are hard to be detected are very complex, and requires software programs lengthy hours to embed and extract the hidden data. In this work, different steganographic schemes will be examined for various data types: audio, image and video. Trade-offs between complexity, signal-noise-ratio and amount of hidden data will be carefully studied. Various processors architectural aspects will be examined such pipelining and multiple processoing units. Next, a full implementation in HDL will be synthesized and loaded in FPGA board. Analysis results of the prototype design will be documented and published.

Publications:

Journal Papers

· Bassam Jamil Mohd, Sa’ed Abed, Bassam Na'ami and Thaier Hayajneh , “Hierarchical Steganography Using Novel Optimum Quantization Technique”, Signal, Image and Video Processing, Springer-Verlag London, Vol. 7, No. 6, pp. 1029-1040,  DOI: 10.1007/s11760-012-0301-9, [12pages], (IF: 0.560).

Conference Papers

· Bassam Jamil Mohd, Sa’ed Abed and Sahel Alouneh, “Image Steganography Optimization Technique”, In Proc. of the International Joint Conference on Advances in Signal Processing and Information Technology (ASP-SPIT 2011), Lecture Notes of the Institute for Computer Sciences, Social Information and Telecommunications Engineering, 1 , Vol. 62, Signal Processing and Information Technology, Part 1, Amsterdam, Netherlands, Dec 1-2, 2011, pp. 205-209, [5 pages].

· Bassam Jamil Mohd, Sa’ed Abed, Thaier Saleh Hayajneh and Sahel Alouneh, “FPGA Hardware of the LSB Steganography Method”, In Proc. of the IEEE International Conference on Computer, Information and Telecommunication Systems  (CITS 2012),  Amman, Jordan, May 14-16, 2012, pp. 5– 8, 2012, [4 pages].

Parallel counters are one of the important components to construct high performance DSP units including column compression multipliers (i.e. tree multipliers). As the multiplier size increases, designing optimized wider counters is critical for its performance, which is the motive of this study. This article proposes a novel approach to design (2n-1, n) parallel counter using a reduction stage and a single (2n-1 -1, n-1) parallel counter. An algorithm to construct the reduction stage for any counter size is presented. The designs of parallel counter examples using the proposed algorithm are discussed. Finally, the proposed design performance metrics (in terms of delay, power and energy-delay-product) are compared with the conventional parallel counter designs. The proposed designs achieve 13% average speed up, 10% power reduction and 32% improvement in energy-delay-product compared with conventional counters.

Publications:

Journal Papers

· Basim Jamil, Sa’ed Abed and Sahel Alouneh, “Carry-Based Reduction Parralel Counter Design”, International Journal of Electronics, Taylor & Francis, London, UK, DOI: 10.1080/00207217.2012.751320, 2012, [19 pages], (IF: 0.44).

In this project, an immersive virtual roller coaster 3D environment has been introduced. A three degree-of-freedom (3DOF) computer controlled simulator with special effects was designed, implemented, and tested. The 3DOF motion platform which moves in response to control signals generated from the virtual gaming environment, and external environmental effects such as; smell, sound, light, and sense of temperature to interact with events happening in a 3D virtual environment. The controlled machine is developed for entertainment purposes and to suit all ages. Also, the game is static, control signals are sent only from the PC to the motion platform and not vice versa, so that the user can’t control the game. The proposed system was tested and verified since the platform is following everything occurs in the virtual environment and the environmental effects succeeded in giving the real impression. This project aims to build a 3D virtual roller coaster which can be used in amusement parks and family entertainment centers and malls.