安全關(guān)鍵應(yīng)用需求的不斷發(fā)展,對嵌入式實時系統(tǒng)的性能提出了更高的要求,面向中小型簡單系統(tǒng)的傳統(tǒng)分析及評價方法(測試、仿真)不再適用于大型復(fù)雜的先進嵌入式實時系統(tǒng),必須采用更為有效的方法———形式化方法來實現(xiàn)安全關(guān)鍵領(lǐng)域?qū)崟r系統(tǒng)的分析和驗證,以確保系統(tǒng)滿足所需的要求.
　　不同于大多數(shù)嵌入式系統(tǒng)的書籍僅著重于嵌入式技術(shù)的應(yīng)用,也不同于一些實時系統(tǒng)的文獻僅著重于模型、體系架構(gòu)或者系統(tǒng)的實現(xiàn),本書對不同實時系統(tǒng)的分析和驗證方法進行了論述,對不同結(jié)果進行了系統(tǒng)討論或分析,盡可能展現(xiàn)業(yè)界最有意義的發(fā)展趨勢,并結(jié)合大量工程實例,給予更多教學(xué)指導(dǎo),從而幫助讀者在實際中加以利用.
　　原書作者AlbertM．K．Cheng教授是國際上實時系統(tǒng)領(lǐng)域的著名學(xué)者,是IEEETransactionsonComputers期刊的副編輯、IEEE 高級會員、INSTICC 榮譽會員和IOP會員,研究方向涵蓋實時系統(tǒng)、安全關(guān)鍵系統(tǒng)、CPS物理信息融合系統(tǒng)和形式化驗證方法,在國際期刊和會議上發(fā)表了180余篇論文,承擔了多項美國自然科學(xué)基金項目,與美國著名公司W(wǎng)indRiver有著長期深度的合作,其實時系統(tǒng)方面的研究成果被廣泛應(yīng)用于工程領(lǐng)域.本書原著是其多年來在嵌入式實時系統(tǒng)領(lǐng)域進行研究和教學(xué)工作的產(chǎn)物,在嵌入式實時系統(tǒng)的分析和驗證方法方面具有很強的系統(tǒng)性,書中討論了現(xiàn)有技術(shù)和工具在各種工業(yè)領(lǐng)域的應(yīng)用,所結(jié)合的工程項目(來源于NASA航天、航空、火車、汽車等安全關(guān)鍵應(yīng)用領(lǐng)域)具有很強的實用性.此書出版后被國際多所大學(xué)的教授采納為相關(guān)專業(yè)本科生和研究生課程教材,這些教授包括ProfDinoMandrioli(PolitecnicodiMilano,Italy),ProfPedroMejiaGAlvarez(InstitutoTecGnologicoNacional,Mexico),ProfSudarshanK Dhall(UniversityofOklahoma,Norman,USA),ProfBernardoA LeondelaBarra (UniversityofTechnology,Sydney(UTS),Australia),ProfBinoyRavindran(VirginiaTech,USA),andProfFarokhBastani(UniversityofTexas,Dallas,USA),ProfAloisFerscha(UniversiGtyofLinz,Austria),ProfMiguelCeballos(UniversidadAutonomadeQueretaro,Mexico)和ProfHughAnderson(NationalUniversityofSingapore).
　　本書圍繞嵌入式實時系統(tǒng)的調(diào)度、分析和驗證,分為12章.第1章介紹了實時系統(tǒng),定義了時間概念及其測量方法;第2章采用符號邏輯和自動機理論方法論述了非實時系統(tǒng)的分析和驗證;第3章討論了實時調(diào)度方法和調(diào)度性分析;第4章論述了有限狀態(tài)系統(tǒng)的模型檢測;第5章討論了以Statecharts、Statemate為代表的可視化形式化方法;第6章討論了實時邏輯RealGTimeLogic(RTL)、圖論分析和ModeGchart;第7章討論了時間自動機方法;第8章討論了時間無關(guān)(untimed)Petri網(wǎng)和時間/定時Petri網(wǎng);第9章討論了進程代數(shù)(processGalgebraic)方法;第10章討論了基于命題邏輯規(guī)則系統(tǒng)的設(shè)計與時間分析;第11章討論了基于謂詞邏輯規(guī)則系統(tǒng)的時間分析;第12章討論了基于規(guī)則系統(tǒng)的優(yōu)化.每章在組織上都具有共同之處,包括設(shè)計、分析和驗證工具,歷史回顧和相關(guān)文獻,總結(jié)和習(xí)題.
　　周強博士負責本書的前言、第1、3、11、12章及整體翻譯工作,李峭博士主譯了第7~10章,楊昕欣博士主譯了第2、4~6章.此外,參與本書翻譯工作的還有楊子坤、吳瑩、楊駿峰、劉學(xué)斌、張安逸、孫永磊、姜宇、張娜、于正泉等.
　　每當看到優(yōu)秀的原版書籍并認為可以給國內(nèi)相關(guān)領(lǐng)域作借鑒時,總希望國內(nèi)業(yè)界同仁也能一睹原作芳容.在休斯頓訪學(xué)期間我接觸了原書作者AlbertM．K．Cheng教授,并與其探討了專業(yè)領(lǐng)域的一些問題,在譯書過程中更得到教授本人的幫助,也得到其他很多人的幫助.希望此譯書能有益于國內(nèi)嵌入式實時系統(tǒng)領(lǐng)域的發(fā)展.限于譯者的水平和經(jīng)驗,譯文中難免存在不當之處,懇請讀者提出寶貴意見.本書出版受到北京自然科學(xué)基金“基于交換式互連的響應(yīng)式衛(wèi)星綜合電子系統(tǒng)體系架構(gòu)研究”(4133089)、國家自然科學(xué)基金“分布交換式互連系統(tǒng)的有界活性在線測試方法研究”(61073012)、中央高�；�本科研業(yè)務(wù)費專項資金YMF 12 LZGF057、YWF 14 DZXY 018/023和YWF 15 GJSYS 055和國家留學(xué)基金(201303070189)的資助.
　　譯　者
　　2015年8月