论文部分内容阅读
结合混合系统的研究对余度管理系统进行了形式化的分析和验证。采用的手段是时段演算技术及其扩展。首先进行形式化的需求分析，需求及其假设用时段演算表示，其次严格化地描述算法和参数的选取。在验证过程中，首先应用程序逻辑验证算法，算法的不变量以时段演算表示，最后在时段演算中验证整个系统的行为满足给定的需求。