Date: Mon, 12 Apr 2004 15:40:33 -0500 (CDT)
From: Sandip Ray
Subject: This week in ACL2


Greetings.

This week, Julien Schmaltz is going to talk about modeling and
verification of ethernet protocols in ACL2. We will meet as usual in ACES
6.442 at 4:00p.m. on Wednesday.

--------------------------------------------------------------------------


ETHERNET: From the IEEE Std to the ACL2 Logic

If Ethernet is used so often and for so many years, to my knowledge, there is
today no formal model of it. So, the project I have started recently is to
write ACL2 functions that represent Ethernet as it is specified in the IEEE
Std 802.3, clause 4, i.e. the Carrier Sense Multiple Access with Collision
Detection (CSMA/CD) algorithm for the Media Access Control (MAC). I will
start by introducing how this algorithm is described in the IEEE std, and
this mainly to point out, even if it might be obvious for us, why executable
formal models are necessary.  Then, I will present the main principles of the
part of the CSMA/CD algorithm I am considering in my formalization.  For
instance, I am not modeling real timing features and we may discuss if it
sounds reasonable or not. I will then show my ACL2 model which consists in
two functions: receiveFrame and transmitFrame. My goal is to prove that
somehow the composition of receiveFrame with transmitFrame yields the
identity. So, we may discuss around one or two small theorems to help me to
determine what is the best way to attack this problem.

-----------------------------------------------------------------------------