Algebraic Formal Specification and Formal Validation of the Standard and an Implementation of the OSPF Protocol 


Vol. 29,  No. 3, pp. 360-374, Mar.  2004


PDF
  Abstract

The OSPF protocol is the most widely used Interior Gateway Routing Protocol. Therefore, for the reliability of behavior of gigabit swiching routers, it is essential to guarantee the interoperability and the safety of the OSPF protocol. In this paper, we analyze the standard document of the OSPF protocol, so that we provide a formal specification that specifies the protocol behaviors by detailed design level using the algebraic formal method. By referring available source codes of the OSPF protocol, we supplement the formal specification to express more detailed behaviors that is not specified definitely in the standard. We also formally verify the interoperability and the safety of the protocol state machine of the specification. By showing that the formal specification specify all of the states and the transition events that appear in the standard document of the OSPF protocol, we prove that the state machine has the completeness, and prove it has the interoperability. To prove that the specification of the protocol has the safety, we formally verify the reachability, the liveness, the livelock-free property, and the deadlock-free property. As a result, we prove the protocol has the consistency. The specification and the validation are also effective to the OSPF Version 3 that inherit the protocol mechanism of the OSPF Version 2.

  Statistics
Cumulative Counts from November, 2022
Multiple requests among the same browser session are counted as one view. If you mouse over a chart, the values of data points will be shown.


  Cite this article

[IEEE Style]

J. Park, "Algebraic Formal Specification and Formal Validation of the Standard and an Implementation of the OSPF Protocol," The Journal of Korean Institute of Communications and Information Sciences, vol. 29, no. 3, pp. 360-374, 2004. DOI: .

[ACM Style]

Jae-Hyun Park. 2004. Algebraic Formal Specification and Formal Validation of the Standard and an Implementation of the OSPF Protocol. The Journal of Korean Institute of Communications and Information Sciences, 29, 3, (2004), 360-374. DOI: .

[KICS Style]

Jae-Hyun Park, "Algebraic Formal Specification and Formal Validation of the Standard and an Implementation of the OSPF Protocol," The Journal of Korean Institute of Communications and Information Sciences, vol. 29, no. 3, pp. 360-374, 3. 2004.

Search
(IN TITLE, AUTHOR, ABSTRACT,KEYWORDS)

Advanced Search ▼

POPULAR KEYWORDS
(TOP 10 KEYWORDS)

Recent Publications
(LAST 3 YEARS)






pISSN : 1226 - 4717
eISSN : 2287 - 3880