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