An Algebraic Specification of HDLC Procedures and Its Verification

Teruo Higashino, Yuji Sugiyama, Kenichi Taniguchi, Tadao Kasami, Masaaki Mori

Research output: Contribution to journalArticle

10 Citations (Scopus)

Abstract

It is well known that algebraic specification methods are promising for specifying programs and for verifying their various properties formally. In this paper, an algebraic specification of information transfer procedures of high-level data link control (HDLC) procedures is presented and some of the main properties of the specification are shown. First, we introduce abstract states, state transition functions, and output functions corresponding to elementary notions extracted from the description of HDLC procedures in ISO 3309–1979 (E) and ISO 4335–1979 (E). Second, we show axioms which represent the relations between the values of functions before and after the state transitions. Then, it is proved that the specification is “consistent,” “sufficiently complete,” and “nonredundant.” Also it is shown that an implementation which realizes the specification is naturally derived. In the last section, verification of various properties of HDLC procedures is formulated in the same framework as the algebraic specification, and some verification examples are presented.

Original languageEnglish
Pages (from-to)825-836
Number of pages12
JournalIEEE Transactions on Software Engineering
VolumeSE-10
Issue number6
DOIs
Publication statusPublished - Nov 1984

Keywords

  • Algebraic specification
  • Church-Rosser property
  • HDLC procedures
  • term rewriting system
  • verification

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'An Algebraic Specification of HDLC Procedures and Its Verification'. Together they form a unique fingerprint.

  • Cite this

    Higashino, T., Sugiyama, Y., Taniguchi, K., Kasami, T., & Mori, M. (1984). An Algebraic Specification of HDLC Procedures and Its Verification. IEEE Transactions on Software Engineering, SE-10(6), 825-836. https://doi.org/10.1109/TSE.1984.5010311