Reduced incremental ECFSM-based protocol verification

Chung-Ming Huang, Huei Yang Lai, Duen Tay Huang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The Extended Communication Finite State Machine (ECFSM) model, which belongs to the state transition model, has been used to formally specify protocols with context variables and predicates. Global state reachability analysis is one of the most straightforward ways to verify communication protocols specified in the state transition model. Many CFSM-based global state reduction techniques have been proposed to reduce the complexity of global state reachability analysis. However, these reduction techniques cannot be directly applied to ISO's Estelle and CCITT's SDL, which are ECFSM-based Formal Description Techniques (FDTs), -based protocol verification systems. Based on Itoh and Ichikawa's CFSM-based, Chu and Liu's ECFSM-based reduction techniques, and Huang et al.'s CFSM-based incremental verification technique, this paper proposes a protocol verification technique for ECFSM-based n-entity protocols. In this way, the integrated reduced incremental verification technique can be directly applied to Estelle or SDL-based protocol verification systems.

Original languageEnglish
Title of host publicationProceedings - IEEE Computer Society's International Computer Software & Applications Conference
Editors Anon
PublisherPubl by IEEE
Pages166-172
Number of pages7
ISBN (Print)0818644400
Publication statusPublished - 1993
EventProceedings of the 17th Annual International Computer Software & Applications Conference - COMPSAC 93 - Phoenix, AZ, USA
Duration: 1993 Nov 11993 Nov 5

Other

OtherProceedings of the 17th Annual International Computer Software & Applications Conference - COMPSAC 93
CityPhoenix, AZ, USA
Period93-11-0193-11-05

Fingerprint

Finite automata
Network protocols
Communication

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Huang, C-M., Lai, H. Y., & Huang, D. T. (1993). Reduced incremental ECFSM-based protocol verification. In Anon (Ed.), Proceedings - IEEE Computer Society's International Computer Software & Applications Conference (pp. 166-172). Publ by IEEE.
Huang, Chung-Ming ; Lai, Huei Yang ; Huang, Duen Tay. / Reduced incremental ECFSM-based protocol verification. Proceedings - IEEE Computer Society's International Computer Software & Applications Conference. editor / Anon. Publ by IEEE, 1993. pp. 166-172
@inproceedings{fe00da07ed0344f49c29d8e5c75badb0,
title = "Reduced incremental ECFSM-based protocol verification",
abstract = "The Extended Communication Finite State Machine (ECFSM) model, which belongs to the state transition model, has been used to formally specify protocols with context variables and predicates. Global state reachability analysis is one of the most straightforward ways to verify communication protocols specified in the state transition model. Many CFSM-based global state reduction techniques have been proposed to reduce the complexity of global state reachability analysis. However, these reduction techniques cannot be directly applied to ISO's Estelle and CCITT's SDL, which are ECFSM-based Formal Description Techniques (FDTs), -based protocol verification systems. Based on Itoh and Ichikawa's CFSM-based, Chu and Liu's ECFSM-based reduction techniques, and Huang et al.'s CFSM-based incremental verification technique, this paper proposes a protocol verification technique for ECFSM-based n-entity protocols. In this way, the integrated reduced incremental verification technique can be directly applied to Estelle or SDL-based protocol verification systems.",
author = "Chung-Ming Huang and Lai, {Huei Yang} and Huang, {Duen Tay}",
year = "1993",
language = "English",
isbn = "0818644400",
pages = "166--172",
editor = "Anon",
booktitle = "Proceedings - IEEE Computer Society's International Computer Software & Applications Conference",
publisher = "Publ by IEEE",

}

Huang, C-M, Lai, HY & Huang, DT 1993, Reduced incremental ECFSM-based protocol verification. in Anon (ed.), Proceedings - IEEE Computer Society's International Computer Software & Applications Conference. Publ by IEEE, pp. 166-172, Proceedings of the 17th Annual International Computer Software & Applications Conference - COMPSAC 93, Phoenix, AZ, USA, 93-11-01.

Reduced incremental ECFSM-based protocol verification. / Huang, Chung-Ming; Lai, Huei Yang; Huang, Duen Tay.

Proceedings - IEEE Computer Society's International Computer Software & Applications Conference. ed. / Anon. Publ by IEEE, 1993. p. 166-172.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Reduced incremental ECFSM-based protocol verification

AU - Huang, Chung-Ming

AU - Lai, Huei Yang

AU - Huang, Duen Tay

PY - 1993

Y1 - 1993

N2 - The Extended Communication Finite State Machine (ECFSM) model, which belongs to the state transition model, has been used to formally specify protocols with context variables and predicates. Global state reachability analysis is one of the most straightforward ways to verify communication protocols specified in the state transition model. Many CFSM-based global state reduction techniques have been proposed to reduce the complexity of global state reachability analysis. However, these reduction techniques cannot be directly applied to ISO's Estelle and CCITT's SDL, which are ECFSM-based Formal Description Techniques (FDTs), -based protocol verification systems. Based on Itoh and Ichikawa's CFSM-based, Chu and Liu's ECFSM-based reduction techniques, and Huang et al.'s CFSM-based incremental verification technique, this paper proposes a protocol verification technique for ECFSM-based n-entity protocols. In this way, the integrated reduced incremental verification technique can be directly applied to Estelle or SDL-based protocol verification systems.

AB - The Extended Communication Finite State Machine (ECFSM) model, which belongs to the state transition model, has been used to formally specify protocols with context variables and predicates. Global state reachability analysis is one of the most straightforward ways to verify communication protocols specified in the state transition model. Many CFSM-based global state reduction techniques have been proposed to reduce the complexity of global state reachability analysis. However, these reduction techniques cannot be directly applied to ISO's Estelle and CCITT's SDL, which are ECFSM-based Formal Description Techniques (FDTs), -based protocol verification systems. Based on Itoh and Ichikawa's CFSM-based, Chu and Liu's ECFSM-based reduction techniques, and Huang et al.'s CFSM-based incremental verification technique, this paper proposes a protocol verification technique for ECFSM-based n-entity protocols. In this way, the integrated reduced incremental verification technique can be directly applied to Estelle or SDL-based protocol verification systems.

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

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

M3 - Conference contribution

SN - 0818644400

SP - 166

EP - 172

BT - Proceedings - IEEE Computer Society's International Computer Software & Applications Conference

A2 - Anon, null

PB - Publ by IEEE

ER -

Huang C-M, Lai HY, Huang DT. Reduced incremental ECFSM-based protocol verification. In Anon, editor, Proceedings - IEEE Computer Society's International Computer Software & Applications Conference. Publ by IEEE. 1993. p. 166-172