论文部分内容阅读
如今,无处不在的反应式系统(Reactive System)已经广泛深入了人们的生活,典型的反应式系统有操作系统、网络协议、飞机航线控制系统甚至核反应堆控制系统等。为了精确地描述和定义该类系统,学者们提出了进程代数作为其原型描述语言。其中,Milner在1980年提出的CCS(Calculus of CommunicaringSystems)就是一种典型的进程代数。传值CCS作为纯CCS的完整版本,具有更强的表达能力但仍然非常简洁。传值CCS在CCS的基础上引入了传递信息的操作,它可以在信道上发送和接受值,以便更好地描述和验证反应式系统。 传统的传值CCS的理论中包含了一个默认却关键的假设:其信道没有任何噪音,即假设接收方所接收的值,一定正是发送方所发送的值。然而在实际的反应式系统中,信道上的噪音是难以避免的,于是Ying、Cao等学者都分别开始考虑噪音对系统的影响。为了更好地对这些带有噪音信道的反应式系统进行建模和验证系统性质,本文提出了噪音环境下的传值CCS(VCCSN),通过定义在所有值上的一个概率分布来刻画系统中的噪音。 本文主要做了以下几方面的工作: 1.为了研究噪音环境下的传值通信系统演算,我们扩展了传值CCS的操作语义,提出了噪音环境下VCCSN的操作语义。 2.研究了VCCSN中的Barbed等价、Barbed同余、强互模拟和全互模拟,并且证明了强互模拟和Barbed等价的一致性以及全互模拟和Barbed同余的一致性。 3.在变迁语义的基础上,针对VCCSN定义了一个概率模态逻辑系统,用于规范反应式系统的性质,并且验证了该逻辑系统和互模拟概念之间的联系,即两个进程是强互模拟的当且仅当它们满足相同的概率模态公式。 4.作为VCCSN的一个应用,我们用VCCSN对一个通信协议进行建模,并且说明该协议能够在有噪音的信道上进行可靠的传输。