基于TLA+的AFDX冗余管理算法的改进

为了在航空应用中得到更加安全可靠的通讯系统,就目前普遍应用的标准以太网可能会出现的问题,提出了用行为时序逻辑TLA对AFDX冗余管理算法进行形式化分析。在适当的环境中,根据安全性、活性、可用性3个性质,得到两个冗余管理的推论,根据这些性质和推论,提出了3个冗余管理算法,并用TLA+语言进行详细的描述。通过模型检测,表明出RMA13为最优算法。

中值定理的推广

将微分中值定理推广到存在单侧导数函数的场合,将积分中值定理推广到被积函数存在单侧极限或单调的场合.

类BAN逻辑缺陷的进一步分析

类BAN逻辑是一种用于分析密码协议安全性的逻辑。文章分析了各种类BAN逻辑的缺陷,并对其进行了详细的分类描述,最后指出进一步发展类BAN逻辑需要解决的问题。

因材施“建”传薪火

练功房里,师生们利用课余时间环排练红色音乐舞蹈剧;同学们手绘的百米“红墙”,将大别山地区的革命历史画卷在校园呈现;柳园宿舍“一站式”学生社区内,学生党员们正在开展主题党日活动……在黄冈师范学院,从教学区到生活区,党建元素处处可感,时时滋润师生心田.