本书针对控制系统PLC程序的正确性和可信性检测验证问题，介绍了以形式化理论方法综合运用形成组合检测验证体系，从多个层次检测验证PLC程序动态、静态和运行的正确性

肖力田，清华大学计算机科学与技术博士，北京特种工程设计研究院首席专家兼航天发射场建设责任总师、研究员；多个中央与国家专家咨询委员会委员。作为我国航天测试发射与控制技术领域专家，长期从事航天发射场总体论证、规划、发展战略和试验技术等研究工作，是我国新型航天发射场建设的体系设计者和重要开拓者之一。先后担任项目负责人、总师和第一技术责任人，出色主持完成了一系列国家重大工程研究设计与建设任务；担任指挥部成员和测试发射总体技术专家，遂行保障了200余次重大发射任务，为我国航天发射领域建设跨越式发展做出了卓越贡献。先后获国家科技进步特等奖1项、二等奖1项，国家勘察设计金奖1项等；军队及省部级科技进步奖等44项（一等奖4项、二等奖10项）；发明专利与软件著作权47项，发表学术论文120余篇、著作5部，编制航天发射场类国军标3项。享受国务院政府特殊津贴；荣获中国航天基金会奖、信息化突出贡献人物奖，荣立个人二等功1次；原国防科学技术工业委员会授予“十大标兵”称号与英模等荣誉。

工业控制系统广泛应用于航空航天、国防工程、电力、水利、交通运输、核电站和石油化工等安全攸关行业，是国家安全的重要组成部分。可编程逻辑控制器（programming logic controller，PLC）是一种嵌入式系统和自动控制系统的核心部件，其复杂性及规模也愈加庞大，PLC运行所依赖的PLC程序正确性、可信性保障变得愈加紧迫。国际上，由于软件可信性验证存在问题，经过测试的软件导致的重大灾难、事故和严重损失屡见不鲜，因此如何保证PLC程序正确性得到可信验证已经成为工业控制领域的重大现实问题。 国内外为软件正确性、可信性的检测验证投入了大量人力、物力，如美国国防部先进研究项目局（Defence Advanced Research Projects Agency，DARPA）、美国国家科学基金会（National Science Foundation，NSF）、美国国家航空航天局（National Aeronautics and Space Administration，NASA）、美国联邦航空管理局（Federal Aviation Administration，FAA）、美国国防部（Department of Defence，DoD）、欧洲航天局（European Space Agency，ESA）、欧盟等，都先后支持了很多项目研究，这些研究大多关注常用编程语言编制的软件，取得了很好的效果。但是针对控制系统PLC程序的检测验证，立足在不同应用领域上开展研究，呈现碎片化状态。由于不同的检测验证方法各有所长，所以集合各方法之所长、形成体系化优势，应用到安全攸关工业控制...