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