注册

CODESYS电子期刊

CODESYS

科技周报

2018年6月
   第一期

所需要的9大类技术

聚焦工业安全

王飞跃团队深度剖析:马化腾要建立的              ,有什么来头?

                  对CODESYS IIOT进行讲解

工业4.0

-可编程逻辑控制器代码

安全缺陷分析

“智联网”

CODESYS全球技术大会

能力  VS. 执行力

NENG LI VS. ZHI XING LI

有个朋友跳槽到一家外企工作,刚去公司的时候,因为有很多聪明的想法深得顶头上司的照顾,有一次他跟上司说自己的想法时,上司竖起大拇指说:“真是个好主意,你一定要尽快形成策划方案”。
上司原本以为这位朋友说完后会立即去执行,但没想到他根本没做,只是一直停留在想的层面。
后来,上司要去开会,急匆匆的对朋友说:“上次说的那个方案做好了吗?我要用来跟对方谈合作。”朋友支吾着说:“对不起,我还没做呢,请再给我点时间。”
这下上司火了,因为时间差不多过去一个月了,他没有给朋友任何机会,而是直接把他开除了。为此朋友觉得委屈,他在微信上和我吐槽:“不过没做好方案而已,这外国人真难伺候”。
朋友说这话的时,我并没有说什么,也许他到现在还没有意识到执行力对一个人乃至一个企业到底有多重要。
很多时候,能力并不是最重要的,执行力才是。企业里表现好的员工可能不是能力最强的,但一定是执行力最强的,或许他们没有极强的能力,但是绝对会把眼前所有的事情都处理得井井有条。
与其一直停留在想的层面,不如努力地去做,至少这样不留遗憾。
生活中,有很多人就是这样,总说要开始减肥,可是几个月过去了没有丝毫进展,减肥成了一句口头禅;发誓要早睡早起努力读书,可刷完手机不经意间已经凌晨两点。
下定决心要攒钱,来实现自己微小的梦想,可每月花呗照样还款,总和别人谈及自己的梦想,却从来没有执行的动力。
你我以及身边的大多数年轻人就是这样,虽然心中有很多美好的想法,但从来不敢开始,因为惧怕失败,所以一直在逃避,可你知道吗,等待和犹豫才是这个世界上最无情的杀手。
如果想考研,那就马上努力学习,别一直停留在想的层面;如果想减肥,那就管住嘴迈开腿,千万别只是说说而已。
如果能力还不错,就更不要停留在想的层面了,因为这样只会害了你,让你离自己的梦想越来越远。

/ 03

其实,很多时候,我们并不是能力不行,而是缺乏执行力。想的太多是大多数年轻人的通病,遇到问题首先想到的是困难,而不是怎么解决困难,因为害怕,梦想就只能是梦想了。
凡事如果你去做,可能会成功但也可能会失败,但如果不去做,那么好像只能失败。有很多人遇到事情会犹豫不决,想等待一个绝佳的机会,但殊不知,在你犹豫的时候,具有超强执行力的人已经在做了。
时间久了,你会发现,就算当时你的起点比别人高很多,那么也会被他们甩在后面,造成这个原因的并不是你的能力,而是执行力。

悦读

This is the most delicious
steak in the world

/ 02

悦读:能力 VS. 执行力

·······················  02

CODESYS大事件

眼界:工控行业

第一届CODESYS全球技术大会对CODESYS IIOT进行讲解

可编程逻辑控制器代码安全缺陷分析综述

工业4.0所需要的9大类技术

王飞跃团队深度剖析:马化腾要建立的“智联网”,有什么来头?

···················  05

························  10

··················  14

··················  26

第一届CODESYS全球技术大会对CODESYS IIOT进行讲解

CODESYS大事件

2018年5月16日,第一届全球技术大会(CODESYS Technology Day)在CODESYS全球总部——德国肯普滕市隆重开幕。本次大会是CODESYS集团首届并且是年度最大的科技盛宴,与会人员涵盖德国、中国、美国、意大利等全球客户与合作伙伴共计600余人,共同见证了CODESYS前沿科技与工业4.0时代的完美结合,探讨了工业自动化的当下与未来。值得关注的是,本次会议除了对IIOT、Cloud Services、IT Security、Factory Management等做出精彩解析外,还提出“Industrial Automation in 2025”这一与“中国制造2025”相贴合的议题,体现出总部对中国市场的格外重视与青睐。会议同期,中国团队还将组织对CODESYS总部以及德国的斯图加特、慕尼黑,意大利的企业及大学的访问和考察。全面感受严谨的欧洲工业中渗透的文化智慧。

/ 04

/ 05

本次大会,各项目负责人向大家分享了CODESYS科技最新阶段性成果。

自动化工厂中如何实现控制器等硬件设备的监测和维护?如今仍是一个待探索的难题。全球技术大会上,演讲人向大家展示了通过CODESYS服务器技术来管理机器和设备应用程序以实现设备的交换、预测性维护、新单元的配置等最新成果。

CODESYS大事件

CODESYS大事件

Well Protected

在IIOT/工业4.0时代,工业网络安全尤为重要,尤其是网络的安全性引起越来越多的用户注意,软件与硬件相结合可在安全与灵活性之间获得最佳平衡。CODESYS对此进行了大量研究开发,并最终实现对设备用户端的开发者、使用者提供专业化身份验证机制,从设备端实现工厂设备和系统安全的有效保障。

Everything Under Control I/II

/ 06

/ 07

CODESYS大事件

CODESYS大事件

Perfect Data

CODESYS云服务究竟能做什么?大会中,我们展示了它为收集和处理自动化数据提供的几乎无限制存储,以及在所有主流平台使用多种格式/协议进行数据收集和传输。对于设备的预测性维护或异常检测,它也是轻而易举。

自动化工厂中如何实现控制器等硬件设备的监测和维护?如今仍是一个待探索的难题。全球技术大会上,演讲人向大家展示了通过CODESYS服务器技术来管理机器和设备应用程序以实现设备的交换、预测性维护、新单元的配置等最新成果。

Everything Under Control I/II

Always Up-To-Date

控制器数据随时更新可以保障客户使用最新的功能或修复已知的漏洞,CODESYS产品经理Samuel Greising先生向大家展示了如何在Office平台上快速执行CODESYS软件更新。

大会最后由德国CEO Manfred先生做总结发言,提出了CODESYS在2025年之内的关于构建专业的基于CODESYS云的数字化工厂软件解决方案。

/ 08

/ 09

如今,我们终于迎来第四波工业创新浪潮,这就是工业4.0,它以9大类科技技术为基础。在这次工业转型中,传感器、机器、工件和IT系统将在整条价值链上融合到一起。这种实体设备与互联网相互连接的制造系统能对数据进行收集分析,对错误进行预判、调整,从而适应不断变化的环境。在生产效率方面,在未来5-10年,越来越多的公司将采用工业4.0技术,除生产资料以外的可变成本将降低15-25%,工业部件制造企业将获得最大的生产效率提升(20-30%),例如汽车制造企业生产率将提高10-20%。工业4.0技术将大大提升制造效率,推动经济转型,改进劳动力就业结构,并最终改变公司乃至国家之间的竞争格局。

工业4.0所需要的9大类技术

眼界:工控行业

眼界:工控行业

工业4.0的9大类技术中的很多技术其实已经应用在制造业中,但工业4.0技术将这些技术整合到一起,成为完整的生产流程,这将改变供应商、制造商和消费者之间的关系,以及人与机器之间的关系。

对于制造领域,大数据分析还是新鲜事物,但它已经能帮助企业改进产品质量,节省能源并提高设备的性能。在工业4.0的环境下,对不同数据源(设备、系统和企业)进行收集和分析将成为未来企业进行实时决策的标准配备。
半导体制造商收集生产过程中的数据,这帮助它在生产流程的早期预判出故障的芯片,从而提高生产质量。

大数据和数据分析技术

很多生产行业已经广泛采用机器人进行生产,但今天的机器人技术变得更加强大。自动机器人不但更加灵活和智能,更可以在彼此之间进行沟通互动,甚至具备学习新技能的能力。这些新机器人不但在性能上远超目前的工业机器人,更在成本上大大降低。
机器人设备制造商提供生产的机器人就具备相互沟通的能力。这些机器人可以在一起合作,根据生产线上的工序调整自己的行动。这些机器人还搭载了先进的传感器和控制单元,能与人类进行紧密的合作。ABB公司推出双臂机器人YuMi,可以与工人肩并肩的工作,它们具备计算机视觉系统,不但可以识别零件,还能保证与人进行安全的互动。

自动机器人技术

在工程设计领域,不少公司都采用了3D模拟技术来设计产品的结

模拟技术

/ 10

/ 11

构和材料。未来,模拟技术将扩展到更广的范围。人们可以用实时数据来模仿物理世界,将新产品放入虚拟的生产环境中。在进行实际生产前,公司可以对这些新产品进行测试和优化,从而减少设备装配调试的时间并提高产品质量。
     西门子公司开发了一个虚拟机器系统,它可以通过真实数据对机器进行模仿。这个系统最多能减少设备装配调试时间达80%。

眼界:工控行业

眼界:工控行业

博世集团旗下的Rexroth公司推出一套自动生产系统。通过无线电编码,不同位置的工作站可以感知每件产品需要进行的生产步骤,并自动执行生产流程。

随着工业4.0时代的到来,原先相互隔绝的设备将相互连接,工业系统和生产线将连接成一体。到时,网络安全的重要性将大幅提高。安全可靠的网络通信以及身份辨别和接入管理系统将变得至关重要。
去年,欧洲几家大型工业设备制造商已经通过联手和并购的形式与网络安全公司进行了合作。

网络安全技术

很多企业已经开始使用职能和数据分析的云应用。未来更多的生产数据和功能将搭载在云端,为生产制造提供更多的数据相关服务。随着技术的进化,未来的监测和控制流程也可能会迁移到云上。

云计算技术

目前一些企业已经开始采用3D打印技术,但大多数都处于试验阶段或用于制造独立部件。未来3D打印技术将广泛应用到小批量生产和大规模定制领域。3D打印技术将大大降低企业的库存成本和物流成本。
飞机制造企业已经开始使用3D打印技术降低飞机的重量,节省稀有材料如钛的使用量。

增材制造(3D打印)技术

今天大部分公司的IT系统并未完全整合。公司、供应商和顾客常常是各自为战。在企业内部,工程设计、生产和职能部门也往往相互隔绝。即便是工程设计这一环节,也没有几家公司能做到设计——制造——自动化的三点一线。但随着工业4.0技术的发展,公司、部门和能力将成为更加紧密的整体,一条横跨公司的数据网络将让价值链真正实现自动化。
Dassault Systèmes和BoostAeroSpace为欧洲航天和国防工业搭建了名为AirDesign的合作平台。该平台搭建在私有云上,参与的合作伙伴可通过该平台进行复杂的合作以及数据交换。

水平和垂直系统整合技术

目前内置传感器和计算机的互联产品数量仍有限。然而,随着物联网时代的到来,以及连接标准的统一,越来越多的产品将相互连接。届时,身处不同地理位置的产品设备将能进行互动和沟通,并由中央处理器集中控制。物联网将实现决策的去中心化,互联设备能进行自动分析和决策,对环境变化进行实时反应。

物联网技术

现实增强系统可以在很多方面协助工人生产,例如通过手持设备挑

现实增强技术

/ 12

/ 13

选仓库中的配件或发送维修指令。这些系统目前还处在实验期,但未来这些技术将为工人提供实时信息,帮助他们进行实时决策,改善生产流程。
     比如,未来工人可以装备现实增强眼镜等设备,当他们检查一台设备时,计算机就将故障原因和维修指南发送到工人的眼镜上。
另一种应用是虚拟训练系统。西门子为Comos软件开发了一套发电站虚拟操作训练系统。操作人员佩戴现实增强眼镜,训练他们在紧急状况下的操作。

眼界:工控行业

眼界:工控行业

工业控制系统(Industrial control system,ICS)是国家基础设施的核心并广泛用于工业、交通、能源、水利、安防、食品以及大型制造等行业,工业控制系统的网络安全与国家安全息息相关。2010年“震网”(stuxnet)病毒造成了伊朗布什尔核电站重大损失,大量离心机报废,导致伊朗的核计划推迟,也促使工业控制系统安全逐渐成为网络安全领域的研究热点。随着工业控制系统由封闭走向互联,大量的控制器配备了以太网通信组件,使得攻击者可以直接访问PLC硬件及其编程软件。但PLC逻辑控制层缺少认证和监测等保护措施,PLC代码的安全缺陷成为工业控制系统的重要安全威胁之一。

与传统的编程语言一样,PLC存在代码安全缺陷,而这些代码安全缺陷为攻击者攻击工业控制系统留下了后门。
2013年South Carolina大学的Sidney对PLC代码设计安全缺陷进行了深入的研究,并把PLC代码设计级缺陷主要分为基于硬件缺陷和基于软件缺陷两种。攻击者可以利用PLC代码缺陷破坏代码逻辑,进行中间代码插桩,实现任意代码执行等。
2014年北京科技大学李伟泽等提出和分析了一种针对SCADA系统的新型的网络物理攻击——伪逻辑攻击。
2015年在blackhat-US会议上Klick等在西门子S7-300中注入了一种新型的后门,通过注入工具实现了在S7-300上进行SNMP扫描及SOCK5代理功能。作者利用PLC程序中存在跳转指令的安全缺陷,成功在主程序OB1前嵌入恶意指令从而可控制PLC的启停以及输出寄存器。
2016年11月在blackhat欧洲会议上Ali Abbasi等实现了对PLC输入/输出接口的新攻击,该攻击通过篡改输出输入引脚改变系统的运行逻辑。

2.工控代码利用相关研究

可编程逻辑控制器代码安全是确保工业控制系统安全运行的核心,本文围绕着可编程逻辑控制器的代码安全缺陷进行分析,首先阐述了工控代码安全的相关研究。接着,从可编程逻辑控制器代码逻辑缺陷、安全需求规约两个方面对工控代码缺陷进行分类,分析了针对梯形图语言的3种代码逻辑缺陷产生的机理,并结合梯形逻辑图,利用PLC代码逻辑缺陷,实现拒绝服务攻击、中间人攻击等。最后,本文提出了PLC代码形式化验证中面临的困难,并从中间语言翻译、模型构建和模型检测三方面综述了PLC代码形式化验证的相关研究。

1.引言

可编程逻辑控制器代码安全缺陷分析综述

/ 14

/ 15

眼界:工控行业

眼界:工控行业

PLC代码逻辑缺陷具有隐蔽性强的特性,难以发现,可以潜伏多年,传统的安全防御思路无法解决这方面问题。在工业控制系统中,一次开关动作不执行,工艺执行流程的改变以及特定的输出响应故障都可能造成毁灭性的破坏。
本文以梯形图语言为例分析PLC代码逻辑缺陷,梯形图语言形象直观,与继电器的控制电路的表达方式极为相似。梯形图由触点、线圈等图形符号结合数字指令、算术运算指令、控制指令等指令符号构成,PLC代码逻辑缺陷也是由这些元素和组件位置放置不恰当、链接和范围不正确引起的。表1给出了PLC代码逻辑缺陷分类及其相关描述。

不同于传统的IT系统,工业控制系统有其特殊的编程语言,根据国际电工委员会制定的工业控制编程语言标准(IEC61131-3),PLC的编程语言包括以下五种:梯形图语言(LadderLogicP r o g r ammi n g L a n g u a g e , L D)、指令表语言(In s t r u c t i o n L i s t , IL)、功能模块图语言(Function Block Diagram,FBD)、顺序功能流程图语言(Sequential function chart,SFC)及结构化文本语言(Structured text,ST)。本文中的代码缺陷研究也是基于上述编程语言展开的。
工业控制系统的入侵与传统互联网入侵虽然手段上大同小异,但工业控制系统的部署与其物理工艺流程紧耦合,因此利用工艺流程中的代码逻辑缺陷成为针对工业控制系统的有效打击手段之一,如陷阱门、逻辑炸弹、特洛伊木马、蠕虫、Zombie等,且这类新的恶意代码具有更强的传播能力和破坏性。本文主要研究基于软件的PLC代码缺陷,并从代码逻辑缺陷和违反安全需求规约两个方面对PLC代码缺陷进行分类研究。

3.PLC代码缺陷分类

3.1 PLC代码逻辑缺陷

/ 16

/ 17

2017年3月,来自印度海德拉巴和新加坡的学者,演示了针对工业控制系统的PLC梯形图逻辑炸弹(Ladder Logic Bombs,LLB)。该逻辑炸弹是用梯形图语言编写的恶意软件,这种恶意软件可被攻击者注入到PLC现有控制逻辑中,通过改变控制动作或者等待特定的触发信号来激活恶意行为,以实现传感器数据篡改,系统敏感信息获取以及PLC拒绝服务攻击等。

眼界:工控行业

眼界:工控行业

PLC逻辑代码中的数字指令包含比较指令,该比较指令如果编码不正确可能会导致安全隐患,使得恶意用户可以通过比较指令将不正确的数据插入到进程中。这些数据可能会导致进程序列发生变化,或者导致进程完全中止。
如图2所示,假设常开触点I0.1可以触发高压锅炉的初始化,常开触点后连接一个比较函数,O4.1控制高压锅炉的关闭进程。直到A的值大于等于B的值时,O4.1被激活,锅炉停止加热。如果比较元素B不参考符号表中的数值而是使用定值进行硬编码,B中的数据是不受保护的,我们通过提高B的温度值,使得高压锅炉不断加热直到设备损坏甚至发生爆炸。

2)比较函数硬编码缺陷

PLC编程中的计时器可通过设置预设时间触发计时器。定时器完成位元件的不正确放置可能导致涉及定时器完成位的过程和定时器本身进入竞争条件。当定时器完成位成为激活其自身触发机制的必需元素时,发生这种竞争条件使得定时器陷入死循环并使定时器复位。
如图1所示,把计时器的预设值设为0,使得定时器触发位和定时器同时打开,造成计时器持续振荡,使得输出O4.1无法被触发,致使程序流程顺序错误或进程无法关闭等故障,实现拒绝服务攻击。

(1)计时器条件竞争缺陷

图二:比较函数缺陷梯形图

图一:计时器条件竞争缺陷梯形图

/ 18

/ 03

/ 19

 通过利用表1中列举的PLC代码逻辑缺陷,可实现拒绝服务攻击,中间人攻击、改变控制器正常的工作流程等,对工业控制系统造成难以估量的损失。下面给出几个PLC代码缺陷分析和利用。

眼界:工控行业

眼界:工控行业

除了PLC代码的逻辑缺陷外,PLC代码在物理现场的安全需求属性也将决定PLC缺陷利用的成功与否。不同的工控行业安全约束条件也不尽相同,PLC的代码安全还要结合特定行业的物理现场安全需求属性,对时序逻辑、设备状态、变量阈值等进行约束。例如电梯控制系统中按照加速、匀速、减速的顺序升降,交通信号灯控制系统中东西方向和南北方向的交通信号灯在同一时刻不相同,供暖的控制系统中锅炉必须控制在安全的额定温度下运行。Pavlovic等[11]对PLC的时序、状态等安全需求进行了约束。本文将安全需求总结为以下几点,如表2所示。

3.2 PLC代码安全需求规约

跳转和链接缺陷是由一些可影响程序执行顺序的跳转指令和逻辑块指令的错误的跳转到某个程序段而引起。这种类型的代码缺陷类似于中间人攻击,攻击者可以利用错误的跳转指令跳转到一个非预期的位置,并且把在非预期的位置插入恶意的程序段,再返回到跳转之前的位置。
图3给出了基于跳转和链接缺陷的代码利用方法,我们可以利用跳转到子程序JSR函数从File1跳转到恶意代码文件File3中,引入恶意的子程序再返回到JSR跳转之前位置,完成恶意代码的插入,实现中间人攻击。

3)跳转和链接缺陷

PLC代码采用“顺序扫描,不断循环”的工作方式,典型的PLC的工作过程包括三个不同阶段:把输入数据读入存储器、处理存储器中的数据和更新输出数据。PLC程序仅包含有限的状态集合和有限的变量,且程序内部不包含循环,安全需求依赖于输出变量等,所以在一定程度

4.PLC代码形式化分析与验证

图三:跳转和链接缺陷图

/ 20

/ 21

上形式化验证技术适用于PLC程序安全分析和恶意代码检测。
     形式化分析分为定理证明和模型检测两种方法,定理证明过程过于复杂和冗繁,实际中利用定理证明来验证PLC程序正确性的研究并未得到认可。模型检测是一种广泛使用的形式化方法,他更适合用于PLC代码的验证,相比于传统的计算机程序,对低级的PLC程序建模会更容易,因为他的状态转换系统相对简单。

眼界:工控行业

眼界:工控行业

PLC代码形式化验证旨在检测出PLC代码缺陷,防止恶意代码的入侵。目前通过形式化验证方式发现PLC代码缺陷的研究主要集中于对PLC代码形式化模型构建、PLC代码缺陷及安全需求规约描述以及PLC代码模型检测技术的研究,如图4所示。

图四:PLC控制代码检测的技术路线

PLC编程属于低级编程语言且编程语言众多,语法语义晦涩,采用分层寻址,地址寻址复杂,存在隐式的类型数据,建模难度大,语言属性易丢失。 
工业控制系统的实时性要求很高,因此对时间进行建模极为重要,时间建模的对象应包括定时器的累积时间、单条指令的运行时间和执行周期时间,由于定时器是跨循环周期的全局变量,建模时将时间考虑在内会极大地提高建模的难度并增加检测的时间,但不考虑时间就无法检测出与时间相关的安全规约。
工控系统与物理环境关系密切,工业控制器的输入一般可以认为是物理环境的输出,输出一般可以认为是物理环境的输入,构成一个闭环回路,不考虑物理环境就无法精确地模拟出工业控制器的行为。
PLC代码包含的变量多,状态空间大,对PLC代码进行建模分析是建立在状态转化基础上的,如果直接进行模型检测会造成状态空间爆炸的问题。

4.1 PLC形式化分析中面临的困难

4.2 PLC代码形式化分析

4.2.1 中间语言翻译

由于工业控制器支持多种标准编程语言,且语法语义上都有较大差异,现有的模型检测技术大都基于特定的编程语言,为了降低建模的复杂性,我们需要把PLC编程语言转化成模型检测器可以处理的中间语言。
Darvas等提出了将PLC程序的SCL语言转化为基于NuSMV的中间模型方法,它是一种接近于自动机模型的中间模型。McLaughlin等给出了将PLC的指令表IL语言代码翻译为基于Vine的中间语言ILIL的方法。Zonouz等通

/ 22

/ 23

过反编译的方法将MC7code转化为中间语言ILIL,该中间语言ILIL同样使用Bi-tBlaze二进制分析工具Vine插件来描述。

眼界:工控行业

眼界:工控行业

目前研究中用到的模型检测工具有很多,如SMV、UPPAAL、SPIN等。Yoo等使用Verilog模型和CadenceSMV模型对核电站控制系统的PLC代码进行模型检查。McLaughlin等开发了一个TSV(Trusted Safety Verifier)工具,该工具是利用TEG(Temporal Execution Graph)图来进行模型检测,在原始的IL代码对输出变量赋值再转换到ILII中间语言,依据被给的安全需求,TSV使用生成的TEG图来决定具体的原子命题值。Zonouz等同样利用TEG图的方法进行模型检测,先对线性时序逻辑规范公式进行取反接着得到TEG-UR图模型P,然后在模型M中搜寻满足的路径,最后,如果在第三步中不存在任何路径,则可认为原始代码满足安全需求,能够安全地执行。如果存在路径,则可以通过违反约束的路径条件得到相应的反例。
实际开发的PLC程序包含的多个变量和状态空间,执行路径较复杂。会遇到状态空间爆炸的问题。解决状态空间爆炸问题最有效的方法是符号执行McLa-ughlin等提出一种合并具有相同输出的输入来避免等价状态生成的状态聚合方法。Guo等提出了一种用于自动测试PLC编程语言符号执行工具SymPLC。 SymPLC将PLC源代码作为输入,并在应用符号执行之前将其转换为C语言,以系统的生成测试输入来覆盖每个周期任务中的所有路径。为此,他们提出了一些PLC特定缩减技术,用于识别和消除冗余。

在工业控制系统中,一个微小的代码缺陷可能影响到整个工业流程遭受破坏甚至威胁到生命财产安全。本文围绕着工业控制系统控制代码安全展开研究,从PLC代码逻辑缺陷、代码安全需求规约两个方面对工控代码缺陷进行分类,并结合了现实中常见的梯形图逻辑缺陷构造了代码利用场景,基于这些代码逻辑缺陷实现了对工业控制系统的拒绝服务攻击,中间人攻击等。PLC代码形式化验证是发现PLC代码缺陷的一种重要且有效的方法,文章最后围绕着如何实现,简要从中间语言翻译,时间模型构建和模型检测技术三个方面阐述了PLC代码形式化验证的技术路线及研究进展。

5.结语

工业控制系统的实时性要求很高,因此时间是很重要的建模对象。延时寄存器(O n - D e l a y Timer,TON)用于确保PLC中实时性属性,TON指令为PLC的输入信号提供延迟机制。对TON计时器建模会极大地提高建模的难度并增加检测的时间,但不考虑时间就无法检测出与时间相关的安全规约。因此对TON计时器的形式化验证成为PLC代码形式化验证的瓶颈之一。
近年来也有一些对TON计时器的建模研究,Masder等最早开始这方面的研究,他们将IL程序转换为时间自动机模型并使用自动机和Prometa模型两种方式对计时器建模。Willems[21]使用时间自动机对TON模型建模计来解决关于TON的问题。Wan等在定理证明器Coq中针对梯形图语言对TON计时器进行形式化验证,但没有给出通用模块的PLC程序形式化描述。Sidi在定理证明器Coq中针对指令表语言对TON计时器进行形式化验证。

4.2.2 时间模型构建

模型检测是一种广泛使用的自动化验证技术,选择合适的模型来验证系统,并且通过系统地探测建模来检查所要验证的所需属性。由于模型检测可以自动执行,并能在系统不满足性质时提供反例路径,因此在工业界比演绎证明更受推崇。模型检测在PLC系统安全的验证方面特别有用,因为与传统的计算机编程相比,可以更容易地将低级PLC代码建模为状态转换系统。

4.2.3 模型检测技术

/ 24

/ 25

在5月23日举行的2018腾讯“云+未来”峰会上,马化腾表示,希望腾讯在云时代通过“连接”,促成“三张网”的构建:人联网,物联网和智联网。以第三张网——智联网为依托,马化腾提出了“超级大脑”的概念,并希望借助超级大脑的概念来发展智联网。
 说到智联网这一新兴概念,可能许多人会比较陌生。但学界将其作为课题进行专项研究已有一段时间,作为国内最早研究智联网的团队之一,中国科学院自动化所王飞跃教授及其团队在2017年12月期的《自动化学报》曾经探讨了智联网的概念、问题和平台[1],2018年又尝试将区块链与智联网相融合[2],探讨了未来由两者所驱动的CPSS社会将是一种怎样的形态。

王飞跃团队深度剖析:马化腾要建立的“智联网”,有什么来头?

眼界:工控行业

眼界:工控行业

当代西方最有影响的科学哲学家卡尔·波普尔认为,现实是由三个世界组成的:物理、心理和人工世界。而人类一直在围绕这三个世界建立“网”(Grids),第一张网Grids 1.0,就是交通网;接着Grids 2.0,能源网;Grids 3.0,信息网或互联网;Grids 4.0,物联网;现在即将开始第五张网的建设:Grids 5.0,即智联网(Internet of minds,IoM)。围绕上述五张网,人类社会已经进行了一系列的工业革命。第一次工业革命的核心是蒸汽机,第二次工业革命的核心是电动机,第三次工业革命的核心是计算机技术,第四次工业革命的核心是网络,特别是物联网技术。王飞跃教授认为,人类已开始步入稳定的第五次工业革命,即工业5.0之初始阶段,接下来就是虚实平行的智能机所推动的智能时代。

智联网:未来智能社会的基础设施

/ 26

/ 27

   由于我们即将面临第五次工业革命,这就必须开拓思路和重新审视并建立我们的智能技术基础设施:智联网。在智能时代,智联网必须在卡尔o波普尔的三个世界中整合Grid 1.0到Grid 5.0的特性和功能,形成一个合一的网。而这样的网和技术已经出现端倪,如社会交通(Uber,MoBike),社会能源(从智能电网、能源互联网再到社会能源),社会计算,社会制造,社会智能。而这些最新出现的智能技术和系统,必将促生智能生态系统,共享服务,共享经济,最终形成智能社会。我们相信,新时代即将到来的社会网格,是由智联网提供的,它为我们社会的所有智能提供了连接,并最终成为未来智能社会的基础设施。

眼界:工控行业

眼界:工控行业

智联网的基本概念和框架

 根据王飞跃、张俊《智联网:概念、问题和平台》中的定义,智联网,即以互联网、物联网技术为前序基础科技,在此之上以知识自动化系统为核心系统,以知识计算为核心技术,以获取知识、表达知识、交换知识、关联知识为关键任务,进而建立包含人机物在内的智能实体之间语义层次的联结、实现各智能体所拥有的知识之间的互联互通;智联网的最终目的是支撑和完成需要大规模社会化协作的、特别是在复杂系统中需要的知识功能和知识服务。
智联网并非空中楼阁,智联网是建立在互联网(数据信息互联)和物联网(感知控制互联)基础上的,目标是“知识智能互联”的系统。智联网的目标是达成智能体群体之间的“协同知识自动化”和“协同认知智能”,即以某种协同的方式进行从原始经验数据的主动采集、获取知识、交换知识、关联知识,到知识功能,因此智联网的实质是一种全新的、直接面向智能的复杂协同知识自动化系统。

 什么是智联网?

在智能时代新革命中,最显著的特征,就是智能科技作为人类和社会智能的直接延伸而出现。此时,复杂系统,导致人们更需要借助知识自动化所衍生出的机器智能来弥补其自身智能上的不足,进而才能去完成各种层出不穷的时变性、不定性、多样性、复杂性。而整个社会正在涌现海量的、各种层次上的大数据和智能体。尽管这些智能体在数据和信息的层面上实现了互相连通,但是由于缺乏智能联结机制,它们在知识层面上并未做到直接连通。智联网,正是实现借助机器智能的联结来

为什么需要智联网?

/ 28

/ 29

协同人类社会中各种纷杂智能体的核心科技。而只有在实现社会化的智能体知识互联之后,人工智能技术才能够形成真正的社会化生态系统。
     如果说互联网的实质是实现“虚连”或“被动联结”,物联网的实质是“实连”或“在线联结”,则智联网的实质是“真联”或“主动联结”。智联网是新智能时代的核心科技,毫无疑问,只有在智联网建成之后才可以宣告智能时代的全面来临。

眼界:工控行业

眼界:工控行业

     随着信息和物理系统被进一步融合贯通,形成了高级、复杂的信息物理系统(CPS)。CPS理念被广泛应用于交通、能源、国防、制造、医疗、电力、农业等方面。显然,作为CPS系统的设计者、制造者、管理者和使用者,人与CPS系统是紧密结合在一起的,需要人参与其中才能使系统更高效、安全、可靠地运行。在这其中,人与信息物理系统之间的运行模式有共融、协同、主导、辅助、监管等,催生了信息物理社会系统(CPSS)的诞生和发展。

智联网为操作CPSS提供了一个全新的机会。CPSS被认为是一种社会技术系统,它由智能实体组成,可以是机器、技术系统、人类、社会组织等,智联网和它的基础物联网和互联网基础设施,在物理空间中提供了这样的机制,并提供了一种方法,在网络空间中构建一个人工智能的虚拟系统。因此,智联网支持对这三个世界的探索,同时为ACP管理和控制复杂的社会技术系统提供了一个处理程序。智能技术的最新发展,如高性能计算、高吐量通信、大数据分析,已经为基于智联网的CPSS的远景开发提供了基础。

智联网的出现是新IT(Intelligent Technology)发展的自然结果,它的社会基础是老“IT”工业技术(Industrial Technology)、旧“IT”信息技术(Information Technology)和智能技术的统一。智联网利用互联网和物联网作为其基础技术,将知识自动化作为其核心的系统形式,并将知识计算作为其核心技术。智联网的主要任务包括知识获取、知识表示、知识交流和知识关联,旨在构建智能社会实体之间的语义连接。在智能的意义上,智联网旨在实现“合作认知智能”或“合作知识自动化”,即以合作的方式实现知识获取、交流、表示、关联等基本知识功能,并将推理、策略、决策、调度、管理与控制等协同高层次应用自动化。最终,智联网为复杂和大规模的社会化合作提供了知识功能和服务,大大提高了运作效率,并使新的社会合作成为可能,只有人与人之间的互动是不可能的。
智联网意味着向社会化的知识连通、智能整合的跃进;意味着从相对独立的简单知识系统,向着基于知识联结的、整合为一的复杂知识系统的跃进;意味着从以“牛顿定律”为代表的精确物质系统,向以“默顿定律”为代表的自由意志系统的跃进。因此,可以预见,智联网的实现标志着新智能时代全面到来,将是未来智能技术核心之一,具有极其广阔的革命性应用前景

智联网:一种新的智能合作范式

信息物理社会系统:平行智能的智能基础

/ 30

/ 33

眼界:工控行业

眼界:工控行业

区块链和平行区块链技术是一种全网共识、共同维护且保有所有历史交易数据的分布式数据库。其所采用的时间戳、非对称加密、分布式共识、可灵活编程等技术使其具备了去中心化、时间可追溯性、自治性、开放性以及信息不可篡改等特性。区块链技术的基本构架大致可以分为六层,即涵括所有基层信息数据和加密技术等的数据层、连接所有节点完成数据传播以及验证的网络层、涵括各种共识算法与机制的共识层、制定奖励与惩处的激励层、封装算法和智能合约的合约层、以及具体化区块链应用场景的应用层。
区块链的智能合约技术可以真正做到在无外部监督的情况下,以极小的运营成本支撑大型智能实体网络的运行,即“分布式自治组织”(Distributed autonomous organization,DAO)。DAO是区块链的一种特殊应用,它是由多套智能合同配置和操作的。DAO=分布式与去中心化(Distributed,Decentralized)+自主性与自动化(Autonomous,Automated)+组织化与有序性(Organized,Ordered)。下图为信息物理社会系统(CPSS)中的DAO模型。

智联网支撑平台与架构示意图

/ 32

中科院王飞跃教授及其团队在“Blockchainized Internet of Minds: A New Opportunity for Cyber-Physical-Social-Systems”的论文中,提出基于区块链技术的智联网概念。区块链和平行区块链技术是一种全网共识、共同维护且保有所有历史交易数据的分布式数据库。其所采用的时间戳、非对称加密、分布式共识、可灵活编程等技术使其具备了去中心化、时间可追溯性、自治性、开放性以及信息不可篡改等特性。

与智联网核心问题同等重要的,是智联网的支撑平台技术,即在何种平台上,智联网能够得以研究、开发、实施、运行、管理与控制。

 智联网的支撑平台技术

DAO运用智能合约执行一系列公开、公平、公道的系统运行规则,在无人管理和监督的情况下实现自主运行和自主进化。基于区块链的DAO为物联网的运营提供了理想的平台,从而实现按照一定组织规则来自动组织智能体和开展协同知识自动化。更进一步,通过出售或收购DAO的股权,提供或者购买DAO的知识服务,开放智联网DAO知识服务API等种种知识消费商业和技术创新,智联网可以成为一种社会化的技术生态系统。
区块链已经在能源、交通、计算、管理等多个领域崭露头角,其未来应用前景更是不可限量,区块链加人工智能必将把人类社会带入一个知识自动化的智能社会。

眼界:工控行业

眼界:工控行业

虽然物联网能够很容易地通过自动化系统访问传感、通信和控制,但智联网支持连接和协作的智能和知识。智联网提供了建立、开发和操作CPSS的物理、社会和网络空间的范例,并创建了相应的虚拟人工系统。利用智联网作为辅助技术,利用ACP方法,管理和控制社会技术CPSS变得可行。区块链化的智联网为创造一个真正自主的、可靠的、安全的全社会生态系统提供了革命性的能力,我们预见到这是重新塑造我们的社会的一个新的历史机遇,并将新的IT融入到CPSS中。

/ 34

/ 35

Copyright © 2024 陕西妙网网络科技有限责任公司 All Rights Reserved

增值电信业务经营许可证:陕B2-20210327 | 陕ICP备13005001号 陕公网安备 61102302611033号