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 Higashino | 1 | 1086 | 119.60 |
Masaaki Mori | 2 | 17 | 4.08 |
Yuji Sugiyama | 3 | 11 | 2.12 |
kenichi taniguchi | 4 | 256 | 35.56 |
Tadao Kasami | 5 | 751 | 131.11 |