[發明專利]一種基于UPPAAL模型的汽車軟件源代碼仿真測試方法

有效

• 申請號: 201210382231.4
• 申請日: 2012-10-11
• 公開（公告）號: CN102866952A
• 公開（公告）日: 2013-01-09
• 發明（設計）人: 閆旭琴;劉曉建;王知學;成巍
• 申請（專利權）人: 山東省科學院自動化研究所
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 濟南圣達知識產權代理有限公司 37221
• 代理人: 張勇

技術領域

本發明涉及一種軟件工程領域，尤其涉及一種基于UPPAAL模型的汽車軟件源代碼仿真測試方法。

背景技術

隨著汽車智能化程度的不斷提高，更多的控制功能趨于使用軟件來實現，導致汽車軟件的規模和復雜度不斷增長。Manfred?Broy在文獻[M.Broy，I.H.Kruger,A.Pretschner,C.Salzmann.Engineering?Automotive?Software.Proceedings?of?the?IEEE,95(2):356-373,2007.]中預測，“未來五年內上市的下一代高檔轎車上，軟件的總量將達到1GB,軟件將成為汽車價值的主要貢獻者，同時軟件開發的比重和成本也將不斷提高”。隨著汽車上軟件比重的不斷提高，汽車軟件開發面臨著越來越多的挑戰，這些挑戰主要來自如下幾個方面：（1）汽車系統是一種嵌入式實時性系統，具有嚴格的時間約束性，這種時間約束性與軟件系統的可控的物理工作過程密切相關，汽車系統的安全性主要依靠軟件系統的可控的物理工作過程的正確性；（2）汽車系統是一種復雜而龐大的嵌入式計算機系統，包括數以萬計的、與需求相關的功能條目；（3）汽車系統是一種分布式計算機系統，包括大量的用于諸如ECU、激勵器等組件間交互信息的信號；（4）電子產品和汽車電子系統功能的復雜性日益增加。面對這些挑戰，需要新的方法、模型和工具來確保汽車系統的安全性和可靠性。

對于汽車系統這樣一種安全關鍵系統而言，設計者必須深刻理解系統的可控的物理工作過程，當系統的可控的物理工作過程是正確的，就能確保系統處于安全狀態。Anders?P.Ravn、Hans?Rischel和Kirsten?Mark?Hansen在文獻[A.P.Ravn,H.Rischel,K.M.Hansen.Specifying?and?Verifying?Requirements?of?Real-Time?Systems.IEEE?Transactions?on?Software?Engineering,19(1):41-55,1993.]中指出“設計嵌入式計算機系統的工程師必須深刻理解系統可控的物理工作過程這一特性，當這個系統是安全關鍵性系統時，這種洞察力被明確并形成設計基礎就顯得尤為重要”，這一問題已經引起了學術界的廣泛認識。近些年來出現了一些基于模型的實時系統分析工具，如SaveCCM（SaveComp?Component?Model）[M.J.Carlson,J.H.Hansson,M.Nolin,T.Nolte,and?P.Pettersson.The?SaveCCM?Language?Reference?Manual.MRTC?report?ISSN?1404-3041?ISRN?MDHMRTC-207/2007-1-SE,Real-Time?Research?Centre,University，January，2007.]、KRONOS[C.Daws,A.Olivero,S.Tripakis?and?S.Yovine.The?tool?Kronos.R.Alur,T.A.Henzinger?and?E.D.Sontag（Eds.）Hybrid?Systems?III,LNCS,Springer,vol.1066,1996,pp.208-219,doi:10.1007/BFb0020947.]、TIMES[T.Amnell，E.Fersman，L.Mokrushin，P.Pettersson，W.Yi.Times-a?tool?for?modelling?and?implementation?of?embedded?systems.K.G.Larsen?and?P.Niebert（Eds.）FORMATS?2003，LNCS，Springer，vol.2791，Sep.2003，pp.60-72，doi：10.1007/978-3-540-40903-8_6.]和UPPAAL[G.Behrmann,A.David,K.G.Larsen.A?Tutorial?on?UPPAAL.M.Bernardo?and?F.Corradini（Eds.）SFM-RT?2004,LNCS,Springer,vol.3185,Sep.2004,pp.200–236,doi:10.1007/978-3-540-30080-9_7.][R.Alur,D.L.Dill.A?Theory?of?Timed?Automata.Theoretical?Computer?Science,126(2）:183-235,1994.][G.Behrmann,J.Bengtsson,A.David,K.G.Larsen,P.Pettersson,and?W.Yi.Uppaal?implementation?secrets.W.Damm?and?E.–R.Olderog(Eds.）FTRTFT?2002,LNCS,Springer,vol.2469,Sep.2002,pp.3-22,doi:10.1007/3-540-45739-91.]，這些工具可以用于分析和驗證系統。目前它們已經足夠成熟可以應用在實時系統的工業開發中，軟件設計人員可以利用這些工具的分析結果撰寫軟件源代碼，但是卻無法確保與系統的可控的物理工作過程相關的源代碼的正確性。