An Algebraic Specification of HDLC Procedures and Its Verification

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

Research output: Contribution to journalArticlepeer-review

11 Citations (Scopus)


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
Issue number6
Publication statusPublished - Nov 1984


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

ASJC Scopus subject areas

  • Software


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

Cite this