[發(fā)明專利]應(yīng)用邏輯及其驗證方法和構(gòu)成方法

有效

• 申請?zhí)枺?/td>: 201710271230.5
• 申請日: 2017-04-18
• 公開（公告）號: CN107506509B
• 公開（公告）日: 2020-08-07
• 發(fā)明（設(shè)計）人: 本谷徹;白石雅裕;西川悟史;山本圭輔;鳥羽忠信;上薗巧;原田英雄;菅野雄介
• 申請（專利權(quán)）人: 株式會社日立制作所
• 主分類號: G06F30/20
• 分類號: G06F30/20;G06F30/327
• 代理公司: 北京銀龍知識產(chǎn)權(quán)代理有限公司 11243
• 代理人: 范勝杰;曹鑫

1.一種核反應(yīng)堆儀控裝置的安全保護系統(tǒng)的應(yīng)用邏輯的驗證方法，具備：

一個或多個宏邏輯，進行規(guī)定的運算；

宏運算控制部，為了使所述宏邏輯進行所述運算而向所述宏邏輯指示開始所述運算；和

運算數(shù)據(jù)存儲區(qū)域，對數(shù)據(jù)進行存儲，

所述應(yīng)用邏輯的驗證方法的特征在于，

分別針對所述宏邏輯、所述宏運算控制部、所述運算數(shù)據(jù)存儲區(qū)域，進行基于形式驗證語言的屬性描述的靜態(tài)驗證，

針對所述宏邏輯的至少一個，還進行基于仿真的動態(tài)驗證，

所述宏邏輯具備：

一個或多個運算邏輯，進行規(guī)定的浮動小數(shù)點數(shù)運算；

浮動小數(shù)點數(shù)運算控制部，為了使所述運算邏輯按照運算算法的順序進行所述浮動小數(shù)點數(shù)運算，向所述運算邏輯指示開始所述浮動小數(shù)點數(shù)運算；

選擇器，通過所述浮動小數(shù)點數(shù)運算控制部的控制，向所述運算邏輯轉(zhuǎn)送所述浮動小數(shù)點數(shù)運算所需的數(shù)據(jù)；和

輸出值處理部，對從所述運算邏輯獲取的輸出數(shù)據(jù)進行處理并輸出，

分別針對所述運算邏輯、所述浮動小數(shù)點數(shù)運算控制部、所述選擇器以及所述輸出值處理部，進行基于形式驗證語言的屬性描述的靜態(tài)驗證，

針對所述運算邏輯，還進行基于仿真的動態(tài)驗證。

2.根據(jù)權(quán)利要求1所述的應(yīng)用邏輯的驗證方法，其特征在于，

所述應(yīng)用邏輯還具備：

運算順序存儲區(qū)域，存儲使所述宏邏輯進行所述運算的順序；

輸入選擇器，在所述運算之前向所述宏邏輯轉(zhuǎn)送存儲于所述運算數(shù)據(jù)存儲區(qū)域的所述數(shù)據(jù)；

輸出選擇器，在所述運算之后，將所述宏邏輯的運算結(jié)果向所述運算數(shù)據(jù)存儲區(qū)域轉(zhuǎn)送；

運算開始信號線，從所述宏運算控制部向所述宏邏輯發(fā)送用于指示開始所述運算的運算開始信號；和

運算結(jié)束信號線，從所述宏邏輯向所述宏運算控制部發(fā)送用于通知結(jié)束所述運算的運算結(jié)束信號，

分別針對所述運算順序存儲區(qū)域、所述輸入選擇器以及所述輸出選擇器進行基于形式驗證語言的屬性描述的靜態(tài)驗證。

3.根據(jù)權(quán)利要求1所述的應(yīng)用邏輯的驗證方法，其特征在于，

所述應(yīng)用邏輯的所述宏邏輯在功能框圖中經(jīng)由輸入輸出信號線或運算控制信號線相互連接；

所述應(yīng)用邏輯還具備：

運算開始信號線，從所述宏運算控制部向所述宏邏輯發(fā)送用于指示開始所述運算的運算開始信號；和

運算結(jié)束信號線，從所述宏邏輯向所述宏運算控制部或其他的宏邏輯發(fā)送用于通知結(jié)束所述運算的運算結(jié)束信號。

4.根據(jù)權(quán)利要求1所述的應(yīng)用邏輯的驗證方法，其特征在于，

所述運算邏輯由多個子功能模塊的組合構(gòu)成；

分別針對所述子功能模塊，進行基于形式驗證語言的屬性描述的靜態(tài)驗證。