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 - 1984
Externally publishedYes

Fingerprint

Specifications

Keywords

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

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

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

An Algebraic Specification of HDLC Procedures and Its Verification. / Higashino, Teruo; Sugiyama, Yuji; Taniguchi, Kenichi; Kasami, Tadao; Mori, Masaaki.

In: IEEE Transactions on Software Engineering, Vol. SE-10, No. 6, 1984, p. 825-836.

Research output: Contribution to journalArticle

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, vol. SE-10, no. 6, pp. 825-836. https://doi.org/10.1109/TSE.1984.5010311
Higashino, Teruo ; Sugiyama, Yuji ; Taniguchi, Kenichi ; Kasami, Tadao ; Mori, Masaaki. / An Algebraic Specification of HDLC Procedures and Its Verification. In: IEEE Transactions on Software Engineering. 1984 ; Vol. SE-10, No. 6. pp. 825-836.
@article{e059820ac4b64085ab2ba6ce00699f98,
title = "An Algebraic Specification of HDLC Procedures and Its Verification",
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.",
keywords = "Algebraic specification, Church-Rosser property, HDLC procedures, term rewriting system, verification",
author = "Teruo Higashino and Yuji Sugiyama and Kenichi Taniguchi and Tadao Kasami and Masaaki Mori",
year = "1984",
doi = "10.1109/TSE.1984.5010311",
language = "English",
volume = "SE-10",
pages = "825--836",
journal = "IEEE Transactions on Software Engineering",
issn = "0098-5589",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
number = "6",

}

TY - JOUR

T1 - An Algebraic Specification of HDLC Procedures and Its Verification

AU - Higashino, Teruo

AU - Sugiyama, Yuji

AU - Taniguchi, Kenichi

AU - Kasami, Tadao

AU - Mori, Masaaki

PY - 1984

Y1 - 1984

N2 - 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.

AB - 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.

KW - Algebraic specification

KW - Church-Rosser property

KW - HDLC procedures

KW - term rewriting system

KW - verification

UR - http://www.scopus.com/inward/record.url?scp=0021521640&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0021521640&partnerID=8YFLogxK

U2 - 10.1109/TSE.1984.5010311

DO - 10.1109/TSE.1984.5010311

M3 - Article

VL - SE-10

SP - 825

EP - 836

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

SN - 0098-5589

IS - 6

ER -