Members

• Abu Nasser Mohammed Abdullah
• Behzad Akbarpour
• Dr. Sofiene Tahar

Description

OFDM (Orthogonal Frequency Division Multiplexing) uses a large number of parallel narrow-band subcarriers instead of a single wide-band carrier to transport information.This technique is easy and efficient in dealing with multi-path fading and also robust against narrow-band interference. It is •sensitive to frequency offset and phase noise. It is used in IEEE 802.11a, IEEE 802.11g, HieperLAN/2, DAB,DVB, DSL. Most of the military communications system have seen its use widely. Theorem Proving (TP) is a Formal Verification (FV) technique. It is FV that makes a design completely bug free. If simulation is not complemented by FV then there is chance that the system has hidden bug which might create problems later. There are many classical examples related to this. In TP, implementation and specification expressed as formulas in a formal logic and the required relationship (logical equivalence/logical implication) described as a theorem to be proven within the context of a proof calculus. I am using HOL (Higher Order Logic) tool for my project. It has many powerful features. I hope to update this page time to time to reflect my progress. Below are two simple diagrams of Physical Layer of IEEE 802.11a which I am planning to verify formally.

Figure 1. OFDM Receiver

Figure 2. OFDM Transmitter