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.
Year
DOI
Venue
1984
10.1109/TSE.1984.5010311
IEEE Trans. Software Eng.
Keywords
Field
DocType
hdlc procedures,various property,algebraic specification,state transition function,high-level data link control,hdlc procedure,verification example,state transition,algebraic specification method,elementary notion,abstract state,information transfer,arithmetic,high level data link control,formal specifications,data mining,protocols,reactive power,kernel,probability density function,verification,algebra
Kernel (linear algebra),Algebraic specification,Programming language,Data Link Control,Information transfer,Computer science,Axiom,Formal specification,Theoretical computer science,Language Of Temporal Ordering Specification,Probability density function
Journal
Volume
Issue
ISSN
10
6
0098-5589
Citations 
PageRank 
References 
11
2.12
18
Authors
5
Name
Order
Citations
PageRank
Teruo Higashino11086119.60
Masaaki Mori2174.08
Yuji Sugiyama3112.12
kenichi taniguchi425635.56
Tadao Kasami5751131.11