论文部分内容阅读
混成系统主要包括离散状态跳转和连续行为演化的混杂叠加，对于很多实际系统，必须考虑系统自身或环境等带来的不确定性和干扰问题，同时还要保证系统的性能需求。很显然针对此类问题，需要有一种将随机行为与经典的混成系统相结合的形式化建模方法，并能在此基础上进行分析验证。 混成CSP(HCSP)是刻画混成系统的形式化建模语言，它是对CSP的扩展，主要引入了中断机制、表示连续行为的常微分方程等，但其缺乏对随机行为的刻画。本文主要扩展了混成CSP，具体地是在原有的基础上引入概率和随机机制:通信和进程等的选择执行不再是确定的，而是满足某个概率分布，同时把常微分方程替代成随机微分方程等。我们先定义随机混成CSP的语法，然后定义相应的操作语义，为了定义和验证随机混成CSP的进程性质，扩展了混成霍尔逻辑(HHL)，建立随机混成霍尔逻辑，并证明其可靠性。