一種基于微分代數(shù)動(dòng)態(tài)邏輯的CPS建模與驗(yàn)證方法.pdf

1、隨著CPS在工業(yè)控制、智能交通、智能醫(yī)療等領(lǐng)域的廣泛應(yīng)用，保證CPS系統(tǒng)的安全性、可靠性等問(wèn)題已經(jīng)成為CPS研究的至關(guān)重要的問(wèn)題。驗(yàn)證技術(shù)是一種保證系統(tǒng)安全可靠的有效手段，它是基于嚴(yán)格的數(shù)學(xué)理論的一種形式化方法。由于CPS是計(jì)算過(guò)程和物理過(guò)程的融合，它不同于傳統(tǒng)的系統(tǒng)，在CPS中始終交織著計(jì)算機(jī)離散計(jì)算和物理世界的連續(xù)動(dòng)態(tài)行為，這給CPS的建模與驗(yàn)證帶來(lái)了很大的困難。微分代數(shù)動(dòng)態(tài)邏輯可以用來(lái)同時(shí)描述離散變遷和連續(xù)的動(dòng)態(tài)行為特性，并且具有

2、相應(yīng)的推理規(guī)則用于微分代數(shù)動(dòng)態(tài)邏輯公式的推理驗(yàn)證。該驗(yàn)證技術(shù)是基于定理證明的，避免了狀態(tài)空間爆炸的問(wèn)題，適合于CPS屬性驗(yàn)證。但是微分代數(shù)動(dòng)態(tài)邏輯的操作模型微分代數(shù)程序過(guò)于抽象，所建模型不具有通用性，不便于系統(tǒng)不同領(lǐng)域?qū)＜抑g交流。
　　本文提出了一種基于HybridUML和微分代數(shù)動(dòng)態(tài)邏輯的CPS建模與驗(yàn)證方法。在這套方法中，首先使用HybridUML對(duì)CPS進(jìn)行建模，HybridUML擴(kuò)展了被軟件工程領(lǐng)域廣泛接受的建模語(yǔ)言--

3、UML，使其能夠同時(shí)描述計(jì)算過(guò)程和物理過(guò)程，適合于CPS建模。詳細(xì)描述了如何使用HybridUML中的agent來(lái)對(duì)CPS的結(jié)構(gòu)進(jìn)行刻畫以及如何使用mode來(lái)描述CPS的行為。其次在基于行為語(yǔ)義一致性的基礎(chǔ)上給出了HybridUML模型與微分代數(shù)程序之間語(yǔ)義的轉(zhuǎn)換規(guī)則，提出了HybridUML模型向微分代數(shù)程序的轉(zhuǎn)換方法，實(shí)現(xiàn)了HybridUML模型向微分代數(shù)程序的轉(zhuǎn)換。最后使用微分代數(shù)動(dòng)態(tài)邏輯對(duì)系統(tǒng)屬性進(jìn)行規(guī)約，并且依據(jù)微分代數(shù)動(dòng)態(tài)邏