【摘 要】
：
目前验证前向可修正属性的＂展开方法＂是不完备的,即当＂展开定理＂的局部条件不满足时,不能判断出系统不满足前向可修正属性。为此,提出一种基于状态转换系统的前向可修正属性验证
【机 构】
：
江苏大学计算机科学与通信工程学院,镇江市地方税务局
【基金项目】
：
国家自然科学基金（60773049）, 江苏大学高级人才科研启动基金（07JDG014）, 江苏省高校自然科学基金（08KJD520015）, 教育部博士点基金（20093227110005）资助
论文部分内容阅读
目前验证前向可修正属性的＂展开方法＂是不完备的,即当＂展开定理＂的局部条件不满足时,不能判断出系统不满足前向可修正属性。为此,提出一种基于状态转换系统的前向可修正属性验证方法,该方法将前向可修正属性的验证归约为可达性问题,进而可借助可达性检测技术完成属性的验证。该方法是完备的,且当属性不成立时,可以给出使属性失效的反例,反例的给出对非法信息流的消除和控制具有直接的帮助。最后,通过磁臂隐通道的例子说明了方法的有效性和实用性。
其他文献
为了精确辨识湿敏电容器的温度补偿模型,减小系统测量误差,分析了湿敏电容器的温度补偿原理,提出了一种基于改进的遗传算法（GA）和支持向量机（SVM）相结合的补偿算法。基于湿敏电容
针对经典时间同步算法应用于无线传感器网络时主要是提高同步精度而忽略网络能耗的问题,提出了一种基于分簇的高能效无线传感器网络时间同步算法。该算法基于分簇的网络拓扑
原有基于模幂运算故障的RSA-CRT故障攻击算法,因添加了错误检验操作而失效。为寻找新的故障攻击方法,以BOS防御算法为攻击分析对象,针对在检错步骤产生故障的情况进行分析,建