CODESYS

2018年6月

?? 第一期

所需要的9大類技術

工業4.0

-可編程邏輯控制器代碼

安全缺陷分析

“智聯網”

CODESYS全球技術大會

能力 ?VS. 執行力

上司原本以為這位朋友說完后會立即去執行，但沒想到他根本沒做，只是一直停留在想的層面。

后來，上司要去開會，急匆匆的對朋友說：“上次說的那個方案做好了嗎？我要用來跟對方談合作。”朋友支吾著說：“對不起，我還沒做呢，請再給我點時間。”

這下上司火了，因為時間差不多過去一個月了，他沒有給朋友任何機會，而是直接把他開除了。為此朋友覺得委屈，他在微信上和我吐槽：“不過沒做好方案而已，這外國人真難伺候”。

朋友說這話的時，我并沒有說什么，也許他到現在還沒有意識到執行力對一個人乃至一個企業到底有多重要。

很多時候，能力并不是最重要的，執行力才是。企業里表現好的員工可能不是能力最強的，但一定是執行力最強的，或許他們沒有極強的能力，但是絕對會把眼前所有的事情都處理得井井有條。

與其一直停留在想的層面，不如努力地去做，至少這樣不留遺憾。

生活中，有很多人就是這樣，總說要開始減肥，可是幾個月過去了沒有絲毫進展，減肥成了一句口頭禪；發誓要早睡早起努力讀書，可刷完手機不經意間已經凌晨兩點。

下定決心要攢錢，來實現自己微小的夢想，可每月花唄照樣還款，總和別人談及自己的夢想，卻從來沒有執行的動力。

你我以及身邊的大多數年輕人就是這樣，雖然心中有很多美好的想法，但從來不敢開始，因為懼怕失敗，所以一直在逃避，可你知道嗎，等待和猶豫才是這個世界上最無情的殺手。

如果想考研，那就馬上努力學習，別一直停留在想的層面；如果想減肥，那就管住嘴邁開腿，千萬別只是說說而已。

如果能力還不錯，就更不要停留在想的層面了，因為這樣只會害了你，讓你離自己的夢想越來越遠。

/ 03

凡事如果你去做，可能會成功但也可能會失敗，但如果不去做，那么好像只能失敗。有很多人遇到事情會猶豫不決，想等待一個絕佳的機會，但殊不知，在你猶豫的時候，具有超強執行力的人已經在做了。

時間久了，你會發現，就算當時你的起點比別人高很多，那么也會被他們甩在后面，造成這個原因的并不是你的能力，而是執行力。

悅讀

This is the most delicious

steak in the world

/ 02

悅讀：能力 VS. 執行力

CODESYS大事件

眼界：工控行業

第一屆CODESYS全球技術大會對CODESYS IIOT進行講解

可編程邏輯控制器代碼安全缺陷分析綜述

工業4.0所需要的9大類技術

王飛躍團隊深度剖析：馬化騰要建立的“智聯網”，有什么來頭？

第一屆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

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控制代碼檢測的技術路線

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

與智聯網核心問題同等重要的，是智聯網的支撐平臺技術，即在何種平臺上，智聯網能夠得以研究、開發、實施、運行、管理與控制。

?智聯網的支撐平臺技術

DAO運用智能合約執行一系列公開、公平、公道的系統運行規則，在無人管理和監督的情況下實現自主運行和自主進化。基于區塊鏈的DAO為物聯網的運營提供了理想的平臺，從而實現按照一定組織規則來自動組織智能體和開展協同知識自動化。更進一步，通過出售或收購DAO的股權，提供或者購買DAO的知識服務，開放智聯網DAO知識服務API等種種知識消費商業和技術創新，智聯網可以成為一種社會化的技術生態系統。

區塊鏈已經在能源、交通、計算、管理等多個領域嶄露頭角，其未來應用前景更是不可限量，區塊鏈加人工智能必將把人類社會帶入一個知識自動化的智能社會。

眼界：工控行業

眼界：工控行業

雖然物聯網能夠很容易地通過自動化系統訪問傳感、通信和控制，但智聯網支持連接和協作的智能和知識。智聯網提供了建立、開發和操作CPSS的物理、社會和網絡空間的范例，并創建了相應的虛擬人工系統。利用智聯網作為輔助技術，利用ACP方法，管理和控制社會技術CPSS變得可行。區塊鏈化的智聯網為創造一個真正自主的、可靠的、安全的全社會生態系統提供了革命性的能力，我們預見到這是重新塑造我們的社會的一個新的歷史機遇，并將新的IT融入到CPSS中。

/ 34

/ 35