View in EDS PDF Full Text

It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols.

Saved in:
Bibliographic Details
Title: It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols.
Authors: Basin, David1 (AUTHOR) basin@inf.ethz.ch, Foster, Nate2 (AUTHOR) jnfoster@cs.cornell.edu, McMillan, Kenneth L.3 (AUTHOR) kenmcm@cs.utexas.edu, Namjoshi, Kedar S.4 (AUTHOR) kedar.namjoshi@nokia-bell-labs.com, Nita-Rotaru, Cristina5 (AUTHOR) c.nitarotaru@northeastern.edu, Smith, Jonathan M.6 (AUTHOR) jms@seas.upenn.edu, Zave, Pamela7 (AUTHOR) pamela@pamelazave.com, Zuck, Lenore D.8 (AUTHOR) zuck@uic.edu
Source: Communications of the ACM. Aug2025, Vol. 68 Issue 8, p50-61. 12p.
Subjects: Formal methods (Computer science), Computer network protocols, Internet protocols, IEEE Standards Board, Internet Engineering Task Force (Organization), Technical specifications
Abstract: This article focuses on the current lack of use of formal methods (FM) for network protocols and what can be done to overcome challenges and implement FM for networking communities. Specification in networking communities is a focus as well as examples of successful FM use in real-world protocols, including transport layer security and Quick UPD Internet Connection. Lastly, the authors present solutions to this gap which include integration of FM in computer science education and integration of design and verification.
Database: Engineering Source
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 186913162
AccessLevel: 6
PubType: Periodical
PubTypeId: serialPeriodical
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Basin%2C+David%22">Basin, David</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> basin@inf.ethz.ch</i><br /><searchLink fieldCode="AR" term="%22Foster%2C+Nate%22">Foster, Nate</searchLink><relatesTo>2</relatesTo> (AUTHOR)<i> jnfoster@cs.cornell.edu</i><br /><searchLink fieldCode="AR" term="%22McMillan%2C+Kenneth+L%2E%22">McMillan, Kenneth L.</searchLink><relatesTo>3</relatesTo> (AUTHOR)<i> kenmcm@cs.utexas.edu</i><br /><searchLink fieldCode="AR" term="%22Namjoshi%2C+Kedar+S%2E%22">Namjoshi, Kedar S.</searchLink><relatesTo>4</relatesTo> (AUTHOR)<i> kedar.namjoshi@nokia-bell-labs.com</i><br /><searchLink fieldCode="AR" term="%22Nita-Rotaru%2C+Cristina%22">Nita-Rotaru, Cristina</searchLink><relatesTo>5</relatesTo> (AUTHOR)<i> c.nitarotaru@northeastern.edu</i><br /><searchLink fieldCode="AR" term="%22Smith%2C+Jonathan+M%2E%22">Smith, Jonathan M.</searchLink><relatesTo>6</relatesTo> (AUTHOR)<i> jms@seas.upenn.edu</i><br /><searchLink fieldCode="AR" term="%22Zave%2C+Pamela%22">Zave, Pamela</searchLink><relatesTo>7</relatesTo> (AUTHOR)<i> pamela@pamelazave.com</i><br /><searchLink fieldCode="AR" term="%22Zuck%2C+Lenore+D%2E%22">Zuck, Lenore D.</searchLink><relatesTo>8</relatesTo> (AUTHOR)<i> zuck@uic.edu</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Communications+of+the+ACM%22">Communications of the ACM</searchLink>. Aug2025, Vol. 68 Issue 8, p50-61. 12p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Formal+methods+%28Computer+science%29%22">Formal methods (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+network+protocols%22">Computer network protocols</searchLink><br /><searchLink fieldCode="DE" term="%22Internet+protocols%22">Internet protocols</searchLink><br /><searchLink fieldCode="DE" term="%22IEEE+Standards+Board%22">IEEE Standards Board</searchLink><br /><searchLink fieldCode="DE" term="%22Internet+Engineering+Task+Force+%28Organization%29%22">Internet Engineering Task Force (Organization)</searchLink><br /><searchLink fieldCode="DE" term="%22Technical+specifications%22">Technical specifications</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: This article focuses on the current lack of use of formal methods (FM) for network protocols and what can be done to overcome challenges and implement FM for networking communities. Specification in networking communities is a focus as well as examples of successful FM use in real-world protocols, including transport layer security and Quick UPD Internet Connection. Lastly, the authors present solutions to this gap which include integration of FM in computer science education and integration of design and verification.
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=186913162
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1145/3706572
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 12
        StartPage: 50
    Subjects:
      – SubjectFull: Formal methods (Computer science)
        Type: general
      – SubjectFull: Computer network protocols
        Type: general
      – SubjectFull: Internet protocols
        Type: general
      – SubjectFull: IEEE Standards Board
        Type: general
      – SubjectFull: Internet Engineering Task Force (Organization)
        Type: general
      – SubjectFull: Technical specifications
        Type: general
    Titles:
      – TitleFull: It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Basin, David
      – PersonEntity:
          Name:
            NameFull: Foster, Nate
      – PersonEntity:
          Name:
            NameFull: McMillan, Kenneth L.
      – PersonEntity:
          Name:
            NameFull: Namjoshi, Kedar S.
      – PersonEntity:
          Name:
            NameFull: Nita-Rotaru, Cristina
      – PersonEntity:
          Name:
            NameFull: Smith, Jonathan M.
      – PersonEntity:
          Name:
            NameFull: Zave, Pamela
      – PersonEntity:
          Name:
            NameFull: Zuck, Lenore D.
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 08
              Text: Aug2025
              Type: published
              Y: 2025
          Identifiers:
            – Type: issn-print
              Value: 00010782
          Numbering:
            – Type: volume
              Value: 68
            – Type: issue
              Value: 8
          Titles:
            – TitleFull: Communications of the ACM
              Type: main
ResultId 1