时态次序说明语言-LOTOS

本文介绍ISO最新开发的一种形式描述技术——LOTOS语言,这种语言以数学方法描述进程外观行为的时态次序,它定义了以事件为运算对象对行为表达式进行运算的一整套规则和相应的形式证明规则,从而为协议的正确说明与验证打下了基础。本文介紹事件和进程的描述方法,以及行为表达式的证明方法。读者可以发现,LOTOS有更广泛的应用。