【摘 要】
：
提出使用事件自动机对C程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法.事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性.事
【机 构】
：
南京航空航天大学计算机科学与技术学院
【基金项目】
：
国家自然科学基金(61272083,61100034)
论文部分内容阅读
提出使用事件自动机对C程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法.事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性.事件自动机将属性规约与C程序本身隔离,不会改变程序的结构.在事件自动机的基础上,提出了自动机可达树的概念.结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法.最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法.实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约.
其他文献
政党制度的主体是政党,主体构成通常是区分不同政党制度的重要标识。政党的政治角色及其功能发挥是制约政党制度效能的重要因素。主体的多元性是我国多党合作制度的结构特征,
党的十八大提出,坚持走中国特色新型工业化、信息化、城镇化、农业现代化道路。在国家"十三五"规划中也强调新型城镇化是国家未来五年的工作重点。新型城镇化是我们党和国家
为了开发可用于运输鸡笼消毒的新型消毒剂,研究模拟了环保型消毒剂微酸性电解水在鸡粪干扰下对运输鸡笼的灭菌效果,并探索了消毒时间(10~40 s)、清洗时间(5~20 s)及有效氯浓
音乐是儿童生活的灵魂,音乐教育是幼儿园教育不可缺少的内容,本文以音乐教育的观点进一步阐述音乐对幼儿健康发展的作用,以促进幼儿身心健康成长,开发幼儿的智能,培养幼儿的
重视饮水系统卫生质量安全是预防鸡群发病的一个重要环节。规模化鸡场饮水管道全封闭、内部清洁困难,而为提高饲料转化率和抗应激能力,普遍通过饮水系统添加多维等产品,加速