CAJ | 학술논문

计算机通信协议的开发难度随着复杂程度的增加而日益增大,潜在错误也越来越多,其中对协议规格说明理解的偏差是重要原因之一.因此需要对规格说明进行验证和确认,并对协议的实现进行一致性测试.一致性测试就是测试协议的实现是否与相关国际标准中的规格说明相一致.协议的规格说明主要是以自然语言描述的,对其进行形式化是为了精确描述协议,因而可减少这类错误的出现.Z语言是基于一阶谓词逻辑和集合论的形式规格说明语言,采用了严格的数学理论,可产生简明、精确、无歧义且可证明的规格说明.本文以TCP协议为例详细介绍了如何使用Z语言对协议进行形式化,为协议一致性测试打下基础.
계산궤통신협의적개발난도수착복잡정도적증가이일익증대,잠재착오야월래월다,기중대협의규격설명리해적편차시중요원인지일.인차수요대규격설명진행험증화학인,병대협의적실현진행일치성측시.일치성측시취시측시협의적실현시부여상관국제표준중적규격설명상일치.협의적규격설명주요시이자연어언묘술적,대기진행형식화시위료정학묘술협의,인이가감소저류착오적출현.Z어언시기우일계위사라집화집합론적형식규격설명어언,채용료엄격적수학이론,가산생간명、정학、무기의차가증명적규격설명.본문이TCP협의위례상세개소료여하사용Z어언대협의진행형식화,위협의일치성측시타하기출.