-
>
湖南省志(1978-2002)?铁路志
-
>
公路车宝典(ZINN的公路车维修与保养秘籍)
-
>
晶体管电路设计(下)
-
>
基于个性化设计策略的智能交通系统关键技术
-
>
德国克虏伯与晚清火:贸易与仿制模式下的技术转移
-
>
花样百出:贵州少数民族图案填色
-
>
识木:全球220种木材图鉴
PLC程序组合检测理论与方法 版权信息
- ISBN:9787302617587
- 条形码:9787302617587 ; 978-7-302-61758-7
- 装帧:一般胶版纸
- 册数:暂无
- 重量:暂无
- 所属分类:>
PLC程序组合检测理论与方法 本书特色
工业控制系统广泛应用于航空航天、国防工程、电力、水利、交通运输、核电站和石油化工等安全攸关行业,是国家安全的重要组成部分。可编程逻辑控制器(Programming Logic Controler,PLC)是一种嵌入式系统和自动控制系统的核心部件,其复杂性及规模也愈加庞大,PLC运行所依赖的PLC程序正确性、可信性保障变得愈加紧迫。国际上,虽经测试的软件由于软件可信性问题所导致的重大灾难、事故和严重损失屡见不鲜,如何保证PLC程序正确性得到可信验证已经成为工业控制领域的重大现实问题。本书旨在总结在PLC程序正确性和可信安全验证方面的研究工作,体系化构建集程序测试、模型检测、定理证明、可信验证和检测优化为一体的组合检测理论与方法,解决PLC程序运行可信性、安全与正确属性检测验证等问题。
PLC程序组合检测理论与方法 内容简介
本书针对控制系统PLC程序的正确性和可信性检测验证问题,介绍了以形式化理论方法综合运用形成组合检测验证体系,从多个层次检测验证PLC程序动态、静态和运行的正确性
PLC程序组合检测理论与方法 目录
1.1 研究背景
1.1.1 PLC运行环境
1.1.2 PLC程序验证需求
1.2 程序正确性检测的现状
1.2.1 代码层次的测试技术
1.2.2 模型层次的模型检测技术
1.2.3 规约层次的定理证明技术
1.2.4 运行层次的状态检测技术
1.3 程序检测流程优化技术研究现状
1.3.1 工作流程计划相关研究
1.3.2 软件检测计划优化技术
1.3.3 PLC程序检测计划技术
1.4 本书主要内容
第2章 PLC程序组合检测体系架构
2.1 PLC工作模式以及系统模型
2.2 PLC程序组合检测体系
2.2.1 PLC组合检测体系构成
2.2.2 PLC程序组合检测方法学
2.3 PLC程序组合检测机理
2.3.1 PLC程序组合检测流程
2.3.2 PLC程序模块组合机制
2.4 PLC程序组合检测研究内容
2.5 本章小结
第3章 PLC程序指称语义
3.1 PLC主要编程指令简介
3.1.1 IEC 61131-3
3.1.2 PLC主要硬件单元
3.1.3 PLC主要编程指令集
3.2 PLC程序体系结构的定义
3.3 PLC程序的指称语义定义
3.3.1 PLC程序语句块的划分与定义
3.3.2 PLC程序基本语句块的指称语义函数
3.4 本章小结
第4章 PLC程序的组合测试
4.1 软件测试技术概述
4.2 PLC嵌入式软件测试技术的适应性研究分析
4.3 基于组合的PLC测试技术
4.3.1 PLC程序组合测试框架
4.3.2 PLC代码块的TA代码
4.4 本章小结
第5章 PLC程序的组合模型检测
5.1 组合模型检测的主要思路
5.2 线性时序逻辑语法、语义
5.3 线性时序逻辑的模型检测问题
5.4 模型检测工具
5.4.1 模型检测工具分类
5.4.2 面向属性验证的工具
5.4.3 面向系统分析和建模的工具
5.4.4 面向源程序验证的工具
5.4.5 模型检测验证工具选择
5.5 PLC程序的符号迁移系统表示
5.6 PLC程序的组合模型检测
5.6.1 通用的组合检测规则
5.6.2 PLC程序特有的组合规则
5.7 组合模型检测的正确性
5.7.1 通用的组合检测规则
5.7.2 PLC程序特有的组合检测规则
5.8 检测策略的案例分析
5.9 本章小结
第6章 PLC程序的组合证明
6.1 定理证明工具
6.1.1 COQ定理证明器
6.1.2 Automath定理证明器
6.1.3 Nqthm和ACL2定理证明器
6.1.4 Isabelle/HOL定理证明器
6.1.5 PVS定理证明器
6.1.6 Nuprl和LEGO证明开发系统
6.1.7 Mizar项目
6.2 直觉主义逻辑及其一阶逻辑定义
6.3 交互式定理证明工具COQ
6.4 基于COQ的PLC程序建模
6.5 基于COQ的PLC程序性质证明
6.6 本章小结
第7章 PLC程序组合检测实际应用
7.1 发射场系统任务与组成
7.1.1 传统发射场系统
7.1.2 先进航天发射场系统
7.2 发射场控制系统
7.2.1 发射场智能系统构成
7.2.2 发射场控制系统组成
7.3 案例概述
7.4 航天发射摆杆控制系统
7.5 航天发射摆杆控制系统PLC输出驱动模块
7.5.1 发射摆杆控制功能
7.5.2 正确性验证性质
7.6 PLC输出驱动模块的组合测试
7.6.1 实际测试
7.6.2 组合测试
7.7 PLC输出驱动模块的组合模型检测
7.8 PLC输出驱动模块的组合证明
7.9 PLC输出驱动模块的组合检测结果分析比较
7.10 本章小结
第8章 PLC程序运行状态检测
8.1 控制系统远程智能支持体系架构
8.1.1 现场级
8.1.2 过程级
8.1.3 远程级
8.1.4 控制任务中智能支持流程
8.2 远程智能支持构建关键要素
8.2.1 PLC程序运行状态检测验证
8.2.2 控制系统智能故障诊断
8.2.3 智能远程支持
8.2.4 远程智能支持平台构建
8.3 可信标签和检测验证协议
8.3.1 可信标签构建
8.3.2 可信标签签名算法分析
8.3.3 PLC程序状态迁移串行可信标签检测验证协议
8.3.4 PLC程序状态迁移并行可信标签检测验证协议
8.3.5 协议原型系统部署试验验证
8.4 PLC程序状态迁移可信标签检测验证协议的安全性分析
8.4.1 外部独立攻击的安全性分析
8.4.2 联合攻击的安全性分析
8.5 本章小结
第9章 相关性驱动检测流程优化
9.1 过程模型的选择
9.1.1 以流程对象为主的过程模型
9.1.2 测试计划的过程模型
9.2 PLC程序检测过程模型的定义
9.3 检测流程中检测项相关性
9.4 检测流程模型优化框架
9.4.1 强相关性检测项的转换
9.4.2 强相关性检测项的同步检测
9.4.3 强相关性检测项的异步检测
9.5 相关性驱动的组合检测流程优化可行性
9.6 本章小结
参考文献
PLC程序组合检测理论与方法 作者简介
肖力田,清华大学计算机科学与技术学科工学博士,北京特种工程设计研究院首席专家兼发射场建设责任总师、研究员;多个中央与国家专家委员会委员。 作为我国测试发射与控制技术领域专家,长期从事发射场总体论证、规划、发展战略和试验技术等研究工作,是我国新型发射场建设的体系设计者和重要开拓者之一。先后担任项目负责人、总师和第一技术责任人,出色主持完成了一系列国家重大工程研究设计与建设任务;担任指挥部成员和测试发射总体技术专家,遂行保障了200余次重大发射任务,为我国运载火箭发射与试验领域建设跨越式发展做出了卓越贡献。 先后获国家科技进步特等奖1项、二等奖1项,国家勘察设计金奖1项等;军队及省部级科技进步奖等44项(一等奖4项、二等奖10项);发明专利与软件著作权47项,发表学术论文120余篇(SCI、EI检索46篇)、著作5部,编制发射场类国军标3项。享受国务院政府特殊津贴;荣获中国航天基金奖、全国工程勘察设计行业信息化突出贡献人物奖,荣立个人二等功1次;国防科学技术工业委员会授予“十大标兵”称号与英模等荣誉。
- >
我与地坛
我与地坛
¥20.2¥28.0 - >
人文阅读与收藏·良友文学丛书:一天的工作
人文阅读与收藏·良友文学丛书:一天的工作
¥16.5¥45.8 - >
经典常谈
经典常谈
¥19.5¥39.8 - >
月亮虎
月亮虎
¥20.2¥48.0 - >
名家带你读鲁迅:故事新编
名家带你读鲁迅:故事新编
¥12.6¥26.0 - >
李白与唐代文化
李白与唐代文化
¥12.5¥29.8 - >
烟与镜
烟与镜
¥17.3¥48.0 - >
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
¥9.7¥14.0
-
迷蒙星空-探天之路
¥14.5¥39 -
飞天起航
¥13.9¥35 -
航空工业出版社遥控模型飞机系列遥控像真模型飞机入门
¥20.2¥48 -
航天器自主导航技术
¥39.1¥112 -
国家出版基金 中国航天的历史使命
¥22.8¥68 -
航空超高强度钢的发展
¥25.9¥58