工业控制系统广泛应用于航空航天、国防工程、电力、水利、交通运输、核电站和石油化工等安全攸关行业，是国家安全的重要组成部分。可编程逻辑控制器（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程序的检测验证，立足在不同应用领域上开展研究，呈现碎片化状态。由于不同的检测验证方法各有所长，所以集合各方法之所长、形成体系化优势，应用到安全攸关工业控制领域，是一种很好的技术途径。

目前，中国航天领域高速发展的多模式进入空间，跨越了陆地固定与机动发射、海上发射，以及空域和天域测量保障与安全控制等，控制系统是航天工业的重要核心组成部分，PLC程序控制的对象繁杂、构成复杂、平台多样和广域散布，涉及航天任务安全。近十多年来，在国家、军队和省部级等十余项重大科技攻关项目支持下，航天自主可控PLC研制项目组率先开展航天多域异构控制系统可信安全关键技术集智攻关与工程应用，在体系、系统、保障和产业上取得了成体系技术突破。这些技术成果也应用到了我国国防、航天、核电、风电、船舶、电子、铁路等领域。本书旨在总结项目组在PLC程序正确性和可信安全验证方面的研究工作，体系化构建集程序测试、模型检测、定理证明、可信验证和检测优化于一体的组合检测理论与方法，解决PLC程序运行可信性、安全与正确属性检测验证等问题，抛砖引玉，促进我国相关领域的发展。

本书共9章，第1章介绍PLC程序检测验证需求背景及其不同层次的检测验证研究现状；第2章研究构建了PLC程序组合检测体系架构，提出了组合检测方法学，阐述了相关机理，界定了研究边界；第3章按照IEC 61131-3标准提出PLC程序体系结构，形式化定义PLC程序指令的指称语义和指称语义函数，使多种多层次检测验证具有统一的语义和约束，支撑各方法优势互补；第4章在代码层，提出了一种基于组合机制的软件测试框架和测试方法，等效测试极限边界条件下的PLC程序，提高测试的覆盖性和PLC程序的可达性验证；第5章在模型层，设计了PLC程序对应的符号迁移系统的变元集合、谓词和迁移函数，以及基于组合策略的模型检测方法，验证PLC程序运行时的动态行为的正确性，降低验证规模；第6章在规约层，提出了一种基于定理证明技术的PLC程序正确性验证框架，验证PLC程序在一个扫描周期内程序的正确性质或静态性质；第7章在应用层，设计了发射场控制系统构成，开展了组合检测技术在航天发射摆杆控制系统案例上的检测应用；第8章在运行层，提出了一种控制系统可信运行与验证的策略，确保在计算资源有限的PLC上实现PLC程序运行状态可信计算验证；第9章在优化层，基于实际物理测试和组合检测的视角，以相关性驱动优化检测流程，缩短检测任务周期。

由于本书涉及的理论、技术、研究成果较多，在许多关键理论、技术或成果之处提供了较多的参考文献标注，以便读者深入研究。本书主要由肖力田负责编写完成；肖楠负责第4章组合测试方法和测试验证的研究，对研究现状和检测验证工具等文献资料进行分析；李孟源负责对发射场控制系统、PLC程序实现、发射场实际控制案例等进行研究，使本书内容能够结合航天发射场进行检测验证。

清华大学软件学院孙家广院士和顾明教授对本书的部分研究内容进行了指导；清华大学贺飞副教授、张荷花副研究员、万海副研究员、刘喻高级工程师，首都师范大学王瑞教授，美国波特兰州立大学宋晓宇教授，国防科技大学毛晓光教授、刘万伟教授，中国电子信息产业集团有限公司宋黎定首席专家、第六研究所丰大军正高级工程师，浙江中控研究院有限公司施一明总裁、王天林总工程师、刘国安高级工程师等对本书的研究工作给予了支持和帮助；出版社余敬春编审为本书的出版做了大量工作。北京特种工程设计研究院和管理层负责人，以及中国航天空间信息技术系列编审委员会对本书相关研究工作给予了全力支持，侯科文、张大伟、董强、袁启平、苏剑彬等对本书的出版给予了帮助。在此一并表示衷心的感谢！

由于作者水平有限，书中难免存在不足之处，敬请读者和专家批评指正。