[發(fā)明專利]編程代碼的先決條件的自動化產(chǎn)生

在審

• 申請?zhí)枺?/td>: 202210857485.0
• 申請日: 2022-07-21
• 公開（公告）號: CN115687072A
• 公開（公告）日: 2023-02-03
• 發(fā)明（設(shè)計）人: A·弗萊克賽德爾;B·施密特;J·鄺特;M·施倫德
• 申請（專利權(quán)）人: 羅伯特·博世有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 中國專利代理(香港)有限公司 72001
• 代理人: 張濤;劉春元

本公開的一個方面涉及一種用于自動化地產(chǎn)生編程代碼的先決條件的計算機實現(xiàn)的方法，包括接收編程代碼中的起點，其中所述編程代碼具有一個或多個輸入變量；接收所述起點的標準；檢查所述標準是否可以通過所述編程代碼從所述起點反向傳播到所述一個或多個輸入變量中的至少一個輸入變量；如果所述檢查是肯定的，則為所述一個或多個輸入變量中的至少一個輸入變量產(chǎn)生至少一個先決條件，其中所述反向傳播被設(shè)計為，使得符合為一個或多個輸入變量產(chǎn)生的先決條件保證了符合所述起點的標準。本公開的第二方面涉及一種電子編程環(huán)境，其被設(shè)計為執(zhí)行用于自動化地產(chǎn)生編程代碼的先決條件的計算機實現(xiàn)的方法。

背景技術(shù)

軟件可能包含錯誤，特別是從具有一定的復(fù)雜性開始。一類錯誤例如由軟件運行時期間出現(xiàn)的運行時錯誤形成。運行時錯誤可能導致軟件崩潰或?qū)е萝浖袨椴徽_。軟件的不正確行為有時在開發(fā)和/或測試期間無法被發(fā)現(xiàn)，并且以后在使用時導致軟件崩潰。

在軟件、特別是與安全相關(guān)的軟件中不應(yīng)出現(xiàn)運行時錯誤。但是，如果在執(zhí)行軟件時出現(xiàn)運行時錯誤，則可能會不可避免地中斷軟件的執(zhí)行。然后不能再提供由軟件執(zhí)行引起的軟件功能性（例如，如果安全架構(gòu)中的冗余未攔截錯誤結(jié)果）。如果運行時錯誤導致軟件行為不正確，則軟件的功能性同樣可能被破壞或取消。運行時錯誤例如可能通過以下方式出現(xiàn)，即不符合軟件編程所使用的編程語言的隱含假設(shè)。例如，在除法中除數(shù)不允許為零，或者不允許訪問所定義的數(shù)組大小之外的數(shù)組元素。如果無論如何都這樣做，則通常會導致未定義的行為、不正確的結(jié)果和/或軟件崩潰。

軟件可以被設(shè)計為監(jiān)視、控制和/或調(diào)節(jié)技術(shù)系統(tǒng)，特別是例如駕駛系統(tǒng)。執(zhí)行軟件時運行時錯誤的影響（例如所述錯誤結(jié)果）通常可能取決于許多因素（系統(tǒng)、環(huán)境、應(yīng)用情況、開放的上下文……）。在不好的情況下，所述影響（例如所述錯誤結(jié)果）可能包括事故、損壞、傷害和/或死亡結(jié)果。例如，除以零的運行時錯誤可能導致軟件執(zhí)行遭到中止，然后該執(zhí)行不能再完成其實際任務(wù)（例如操控制動器或觸發(fā)安全氣囊）。另一個示例是用不正確的數(shù)據(jù)覆蓋存儲區(qū)域，例如當寫入超出數(shù)組邊界以及因此無意地改變了碰巧在那里的其他變量時，這可能導致不正確的行為或甚至導致崩潰。對于技術(shù)系統(tǒng)的用戶和/或環(huán)境而言，技術(shù)系統(tǒng)可以是安全關(guān)鍵的。在這種技術(shù)系統(tǒng)中使用的軟件同樣可以是安全關(guān)鍵的。然而，軟件也可以與技術(shù)系統(tǒng)無關(guān)地是安全關(guān)鍵的。

因此需要采取可以/應(yīng)當確保軟件中沒有錯誤的措施，特別是在安全關(guān)鍵軟件的情況下。為此，經(jīng)常對軟件進行廣泛的測試。但是，測試只能顯示錯誤的存在而不能證明錯誤不存在，因為測試總是只能檢查特定的個體配置或個體場景（“抽查”），而不能檢查軟件在所有配置/場景中的正確行為。

存在對軟件進行形式驗證的方案，這些方案可以形式上證明所述軟件是無錯誤的。這些方案通常需要形式規(guī)范，而這種規(guī)范通常不存在并且創(chuàng)建起來可能很復(fù)雜。但是，形式規(guī)范一般可用于運行時錯誤類別。用于形式驗證的方案包括抽象解釋和模型檢查。在抽象解釋中，程序的指令在抽象域上執(zhí)行。因此，在適當選擇抽象域的情況下可以確定程序行為的良好過度近似。相反，模型檢查相對于形式規(guī)范來檢查程序模型，例如在時間邏輯上。有界模型檢查（BMC）是模型檢查的一種特殊變體，其只在給定限制（Bound）內(nèi)做出有效說明。BMC與許多模型檢查方案相比可以更好自動化地使用。

存在多種商業(yè)工具（英語：tool）可以使用這些方法檢查軟件的運行時錯誤（例如AbsInt的Astrée和MathWorks的Polyspace CodeProver），以及一些來自學術(shù)領(lǐng)域的工具（例如牛津大學的CBMC）。然而，所有這些工具都存在以下問題，即這些工具要么無法擴展到大型軟件系統(tǒng)，要么提供許多虛假肯定的結(jié)果。后者通常是由于這些工具為了免于忽略任何錯誤（“健全性”）而設(shè)計得保守，這在原則上對安全相關(guān)系統(tǒng)可能有意義。然而，要分析的系統(tǒng)越復(fù)雜，分析就越不精確，并且可能顯示越多的虛假肯定的錯誤消息。虛假肯定的錯誤消息可以例如是實際上可能永遠不會出現(xiàn)的錯誤的消息。這尤其是因為隨著系統(tǒng)變得越來越復(fù)雜，并非所有信息都可以準確保存（即必須對信息進行匯編或抽象），否則存儲器消耗和運行時間將以指數(shù)方式增加，然后無法再進行錯誤分析。