本書聚焦于高可靠動(dòng)態(tài)系統(tǒng)的形式化設(shè)計(jì)與驗(yàn)證研究，提出了一種形式化描述與驗(yàn)證方法，主要對(duì)利用可執(zhí)行時(shí)序邏輯語言XYZ/RE來精確描述系統(tǒng)、XYZ/RE到時(shí)間自動(dòng)機(jī)的映射規(guī)則的建立、嵌入式動(dòng)態(tài)系統(tǒng)的建模等進(jìn)行了詳細(xì)介紹，并對(duì)借助基于時(shí)間自動(dòng)機(jī)的驗(yàn)證工具UPPAAL對(duì)系統(tǒng)進(jìn)行形式化驗(yàn)證，以提高系統(tǒng)的正確性、可靠性、可信度等進(jìn)行了講解。此外，本書結(jié)合智能制造、智能家居等典型場景開展實(shí)證，并提出在進(jìn)行工業(yè)控制動(dòng)態(tài)系統(tǒng)設(shè)計(jì)時(shí)可融入先進(jìn)測試技術(shù)的理念，同時(shí)介紹了動(dòng)態(tài)系統(tǒng)的質(zhì)量保證方法。