T. Toyoshima and K. Takahashi (Japan)
AIS, model checking, PRISM, probability, formal method
This paper shows the analysis and verification of an Au tomatic Identification System (AIS) using a probabilistic model checker. AIS is a communication system between ships for safe sailing. Its communications are not interac tive, and hence ships may try to send messages at the same time and be unaware that the messages have not been re ceived. If such communication failures occur frequently, dangerous conditions will result. In actual practice, each ship is assigned a turn for message transmission, and this is determined probabilistically. However, neither the limit of this probability nor the allowable rate of communication failure is known. We construct several models with dif ferent strategies for this system, investigate the probability that safety is ensured, and verify it.
Important Links:
Go Back
