Jan 7 ~ Feb 7 (completed)
- Exchanged emails and met with Rick about our selected topic to get more information about it.
Feb 20 (completed)
- Project-specific topic is selected (mobile ad-hoc networking) and potential properties are proposed.
Feb 24 (completed)
- Meeting to pick specific mobile ad-hoc routing protocols and to discuss future plans for the project.
- Cody will briefly study B.A.T.M.A.N (Better Approach to Mobile Ad-Hoc Networking) to determine any assumptions and guarantees that we could formalize.
- Yvette will briefly study DYMO (Dynamic MANET On-Demand Routing Protocol) to determine any assumptions and guarantees that we could formalize.
- Planned to meet again to discuss our findings.
Feb 25 (completed)
- Meeting with Rick to discuss routing protocol and properties we found. Mostly a check on our progress; we agreed that we would read more about our protocols and try to decide on one and construct a list of properties.
Mar 3 (completed)
- Meeting to decide on which protocol to choose. Both participants wrote a summary for the protocols we researched and came up with a list of properties for each. Based on BATMAN’s greater resources (more documentation and use), it was decided that we would formalize properties of BATMAN for our project. We agreed that the next step is to further read the documentation of BATMAN to develop an understanding of how it works so we can come up with a list of five guarantees that we can formalize.
Mar 7 (completed)
- Constructed website for project.
Mar 18 (completed)
- Understand the bulk of how the BATMAN routing protocol operates. Choose a list of five safety/liveness properties in BATMAN and note any assumptions that those guarantees make.
Mar 25 (completed)
- Arrange meeting with Rick to check that our list of five properties is okay.
- With his advice, choose either SPIN or Alloy to model our properties (dependent on the nature of the properties).
- The language has decided to be SPIN based on the top 5 properties we defined
Apr 17 (completed)
- Become comfortable with syntax of the language of choice (either Alloy or Spin).
Understand the network model code we are given and expand it as necessary.
- Make our own Spin Model
- Formalize the five properties that we chose.
May 1 (completed)
- Expand the model to verify the properties that we chose. Add contradictions to the model to verify that violations to the properties are found.
May 6 (completed)
- Write and submit technical writeup and code.
May 10 (projected)
- 20 minutes presentation of our project