The following is a draft for our SPIN model focuses on the 5 properties we are going to check. (The list is only the first draft that is continuously under modification).
OGM’s fields we need to keep track:
- TTL, with type byte. Initially set to a value in the proposed range, [2, 255]
- Seq_No, with type short. Initially set to a value in the proposed range, [0, 65535] (take the modulo 2^16 when exceeds the range).
- Is-Direct-Link_Flag, with type bool. Indication of a direct neighbor or not, initially set to 0.
- Unidirectional_Flag, with type bool. Indication of the neighboring node is bidirectional or not, initially set to 0.
- Originator_Address, with type int, set to the IPv4 address interface on which behalf the OGM has been generated.