混成系统(Hybrid Systems)是指系统行为既包含离散跳转、又包含连续演化的复杂系统,很多嵌入式系统、实时系统和信息物理融合系统都是混成系统。由于混成系统常用于安全攸关领域,其设计和验证一直是学术界和工业界共同关注的重要问题。在现实应用场景中,往往需要多个子系统之间进行交互与协同,以实现单个子系统无法实现的复杂目标,现有的设计方法难以兼顾高效和安全两方面的需求;另一方面,现实应用场景中还存在着大量的不确定因素,使得混成系统进一步演变成为随机混成系统,现有的验证方法尚不能应对无限时间概率验证问题的挑战。本文针对混成系统的交互与协同设计问题和无限时间概率验证问题,从连续系统多主体协同的设计、切换系统多主体协同的设计、随机系统的无限时间概率验证等三个方面展开研究,主要工作如下:●针对离散时间连续系统的多主体协同的设计问题,提出了基于可达集技术的分层模型预测协同方法。该工作经过分析指出了一方面集中式协同效率低下;另一方面分布式协同安全性难以保证,其根本原因在于各个系统之间的耦合关系难以安全解耦。基于这一思路,本文提出了一种分层模型预测协同的方法,主要利用了可达集对于多主体系统进行解耦。在准备阶段,首先计算出每个主体的协同周期可达集模板。在具体控制时,每个协同时刻,中央协调器基于可达集模板和每个主体系统的当前状态快速得到每个主体的可达集,并基于模型预测的思想计算出每个主体下个协同时刻的目标状态,然后发送给每个主体。每个主体在得到目标状态后,根据自身行为方程,计算出下个协同周期内的具体控制方案。实验显示,该方法克服了集中式协同和分布式协同各自的缺点,在保证安全性的同时有效提升了控制效率。●针对离散时间切换系统的多主体协同的设计问题,扩展了基于可达集技术的分层模型预测协同方法。该工作将分层模型预测控制扩展到了更为常见的切换系统协同控制中。切换系统属于混成系统,而混成系统的可达性具有不可判定、可达集非凸、可达集很难模板化等特点。该工作主要证明了在所研究的场景中,切换系统的可达集可判定且为凸集,并给出了模板的可计算方法,从而在切换系统的多主体协同问题上给出了基于分层模型预测协同的解决方案。实验显示,该方法相对于集中式协同,对于主体数量不敏感,且对于主体模式数量也不敏感。●针对随机连续时间混成系统的无限时间安全验证问题,提出了基于概率栅栏函数的技术。基于初始状态随机的混成系统的无限时间安全验证需求,在经典栅栏函数的基础上,提出了运用概率栅栏函数验证安全性的指导思路,并给出了概率栅栏函数的计算方法。首先对于不同初始状态分布,给出定制化的初始状态集合模板。然后利用栅栏函数思想将安全问题编码为优化双线性矩阵不等式问题。最后利用现有的双线性矩阵不等式求解器进行优化求解出概率最大的初始集合,从而得到随机混成系统的安全概率下界。实验显示,该方法在安全概率的结果上和随机测试相近,但在效率上大幅优于随机测试。