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