论文部分内容阅读
针对组件系统的可信验证问题,提出了一种基于B抽象机精化机制的组件间连接的形式化验证方法.以基于组件的实时响应系统——锅炉控制系统为实例进行了分析,设计了该系统的组件模型,给出了在模型中引入了相关可信行为约束的方法.通过B工具Atelier B对模型进行了检测,验证了模型的正确性.
一个实时系统的组件模型及其可信性验证
【摘 要】
：
针对组件系统的可信验证问题,提出了一种基于B抽象机精化机制的组件间连接的形式化验证方法.以基于组件的实时响应系统——锅炉控制系统为实例进行了分析,设计了该系统的组件
【机 构】
：
北京工业大学 计算机学院,北京 100124
【出 处】
：
2010年第四届中国可信计算与信息安全学术会议
【发表日期】
：
2010年期
其他文献
灭蚊达标是创建国家卫生城的硬指标之一，同时直接关系到人民群众的身体健康、城市声誉及投资环境，推广应用蚊类的环境综合治理，并把城市的开发建设与综合治理蚊虫滋生地有机地结
群密钥协商作为一种基本的密码学任务,其目标在于允许多个用户在公开的网络环境中建立一个共享密钥.目前,群密钥协商协议已成为多方密码学的研究热点.本文介绍了群密钥协商协
认证协议是网络安全的基础.Rubin逻辑具有传统BAN类逻辑所没有的优点.使用Rubin逻辑对Andrew安全RPC协议及2个改进协议进行了分析,发现它们都存在安全缺陷.根据分析结果提出
对第一个在标准模型下可证安全的无证书签名方案和它的一个改进方案进行密码学分析,提出了一种新的密码生成中心(KGC)攻击,即通用恶意KGC攻击.在这种攻击下,恶意KGC在系统参
为了在提高系统的安全性,阻止非法信息流扩散,保证系统的可用性,提出一种基于多信任域的访问控制模型,该模型通过分析组成应用的资源间调用关系,将系统资源映射到相应的信任
１９９８年１２月８～２４日，在灌云县宁海乡突发３７例甲型副伤寒病人，死亡１例，经省、市、县三级卫生防疫专业人员调查，证实为经水传播的甲型副伤寒暴发疫情，现将调查情况报告如下。１ 疫情概况本次暴发共发