Formal Description of Protocols with RAISE Specification Language Based on Temporal Logic
Xiang Gu, Qiu Jianlin · Jisuanji gongcheng · 2011
This paper researches how to use RAISE Specification Language(RSL) to describe operators of Temporal Logic(TL),such as always operator,sometimes operator,until operator and complex operators of TL,and presents the method of formal description with RSL based on TL model.Formal description of AB(Alternating Bit) protocol with RSL based on TL model is given as an example.The result proves that the description model helps realizing automatic implementation of protocols verification and testing.