应用逻辑及其验证方法和构成方法

摘要

本发明涉及应用逻辑及其验证方法和构成方法，提供与SIL4相当的高安全性的应用逻辑。该应用逻辑的验证方法具备：一个或多个宏逻辑，进行规定的运算；宏运算控制部，为了使宏逻辑进行运算而向宏逻辑指示开始运算；和运算数据存储区域，对数据进行存储。该应用逻辑分别针对宏逻辑、宏运算控制部、运算数据存储区域，进行基于形式验证语言的属性描述的静态验证，针对宏逻辑的至少一个，还进行基于仿真的动态验证。

说明书

技术领域

本发明涉及核反应堆等的安全保护系统的应用逻辑及其设计方法。

背景技术

核反应堆的仪控装置分为控制系统和安全保护系统。安全保护系统担负着对核反应堆的异常进行检测并紧急停止的作用。因此，对于安全保护系统的应用逻辑而言，需要是与在IEC 61508中表示系统的安全性能的程度的SIL(Safety Integrity Level)4相当的高安全性。作为至安全保护系统的应用逻辑检测到异常为止的处理，有对核反应堆内的中子通量进行计测，对其上升率进行运算并判断是否超过了规定值的方法。对于中子通量的计测值而言，由于运算所需的精度是十进制的小数点后5位以上，计测值的最大值和最小值的比率是十进制的小数点后7位左右，因此在使用计测值的运算方法中不是固定小数点数运算，而是需要可处理的数值的范围较大的浮动小数点数运算。

在日本特开2005-249609号公报(专利文献1)中，公开了一种安全保护系统的仪控系统，其是使用了硬件逻辑的核反应堆的安全保护仪控系统，组合了针对输入的所有逻辑模式，输出的逻辑模式被预先验证的功能单元而构成。

现有技术文献

专利文献

专利文献1：日本特开2005-249609号公报

发明内容

发明要解决的问题

在专利文献1所公开的技术中，公开了组合了针对输入的所有逻辑模式的输出的逻辑模式被预先验证的功能单元的安全保护仪控系统。但是，在专利文献1所公开的技术中，存在无法开发与SIL4相当的高安全性系统的问题。根据基本安全标准IEC61508的定义，通过基于仿真的动态验证而被验证的逻辑的安全性最多与SIL3相当。由于专利文献1所公开的验证内容仅仅是基于仿真的动态验证，因此存在无法保证与SIL4相当的安全性的问题。

解决问题的方案

本发明的一个方面是具备进行规定的运算的一个或多个宏逻辑、为了使宏逻辑进行运算而对宏逻辑指示开始运算的宏运算控制部、存储数据的运算数据存储区域的应用逻辑的验证方法。该应用逻辑针对各个宏逻辑、宏运算控制部、运算数据存储区域，进行基于形式验证语言的属性描述的静态验证，还针对宏逻辑的至少一个进行基于仿真的动态验证。

本发明的另外一个方面是具备进行规定的运算的一个或多个宏逻辑、为了使宏逻辑进行运算而对宏逻辑指示开始运算的宏运算控制部、存储数据的运算数据存储区域的应用逻辑。在该应用逻辑中，宏逻辑具备进行规定的浮动小数点数运算的一个或多个运算逻辑、为了使运算逻辑按照运算算法的顺序进行浮动小数点数运算而对运算逻辑指示开始浮动小数点数运算的浮动小数点数运算控制部、通过浮动小数点数运算控制部的控制来向运算逻辑转送浮动小数点数运算所需的数据的选择器、对从运算逻辑获取的输出数据进行处理并输出的输出值处理部。另外，运算逻辑由多个子功能模块的组合构成。

本发明的其他的另外一个方面是核反应堆仪控装置的安全保护系统应用逻辑的构成方法，其特征在于，由通过基于形式验证语言的属性描述的静态验证预先验证完毕的功能模块的组合构成安全保护系统应用逻辑。

发明效果

根据本发明，能够开发高安全性的应用逻辑，能够实现与IEC61508的SIL4相当的高安全性。

附图简要说明

图1是表示实施例1中的安全保护系统应用逻辑的构成的框图。

图2是表示实施例1中的应用逻辑的处理顺序的流程图。

图3是表示实施例1中的进行静态验证时的验证方法的示意图。

图4是表示实施例1中的进行动态验证时的验证方法的示意图。

图5是表示实施例1中的应用逻辑的子模块的验证方法的表图。

图6是表示实施例1中的电路规模较大、处理内容复杂的宏逻辑的构成的框图。

图7是表示实施例1中的电路规模较大、处理内容复杂的宏逻辑的处理顺序的流程图。

图8是表示实施例1中的宏逻辑的子模块的验证方法的表图。

图9是表示实施例1中的单精度浮动小数点数运算逻辑的构成的框图。

图10是表示实施例1中的单精度浮动小数点数运算逻辑的子模块的验证方法的表图。

图11是表示实施例2中的应用逻辑的构成的框图。

图12是实施例3中的应用程序开发画面的俯视图。

图13是表示实施例3中的软件宏库和宏逻辑库的一对一对应关系的示意图。

图14是表示实施例3中的应用逻辑设计方法的示意图。

图15是实施例4中的应用程序开发画面的俯视图。

图16是表示实施例4中的应用逻辑设计方法的示意图。

图17是表示实施例5中的应用逻辑设计方法的示意图。

图18是表示实施例6中的应用逻辑设计方法的示意图。

图中符号说明：

100：应用逻辑

101：宏逻辑

102：宏运算控制部

150：单精度浮动小数点数运算逻辑

183：符号部处理部

184：指数部处理部

185：尾数部处理部

186：指数部调整部

具体实施方式

以下利用附图对实施例进行说明。另外，在说明实施例的所有附图中，对具有相同功能的部件标注相同的附图标记，除了特别需要的情况以外，省略其重复的说明。

在图面等中表示的各构成的位置、大小、形状、范围等，为了容易理解发明，有时不示出实际的位置、大小、形状、范围等。因此，本发明不一定必须限定于图面等公开的位置、大小、形状、范围等。

【实施例1】

图1是表示实施方式1中的安全保护系统应用逻辑100的构成的框图。安全保护系统应用逻辑100的运算通过宏逻辑101的组合来实现。宏逻辑101有多种种类，根据应用程序的需要而设置n种宏逻辑101a,101b,…,101n。安全保护系统应用逻辑100例如能够由微型处理器、FPGA(Field Programmable Gate Array)、或ASIC(Application SpecificIntegrated Circuit)等的一个或多个半导体芯片构成。

宏逻辑101通过宏运算控制部102控制。宏运算控制部102和宏逻辑101分别通过宏运算开始信号线103和宏运算结束信号线104连接。宏运算控制部102经由宏运算开始信号线103将运算开始信号发送至宏逻辑101，并指示开始运算。

在应用逻辑100具有n种宏逻辑101a,101b,…,101n的情况下，宏运算开始信号线103和宏运算结束信号线104也同样存在n种。宏逻辑101经由宏运算结束信号线104将运算结束信号发送至宏运算控制部102，并通知结束运算。将宏运算控制部102向宏逻辑101发送了运算开始信号开始，至宏逻辑101执行宏运算并将运算结束信号向宏运算控制部102发送为止的处理定义为“宏逻辑101的调用”。应用程序运算通过重复进行宏逻辑101的调用来执行。

宏逻辑101的调用顺序被保存于运算顺序存储区域105。在重复调用宏逻辑101时，应用程序运算的中间数据保存于运算数据存储区域106。宏逻辑101的宏运算所需的输入数据被从运算数据存储区域106适当地调用，作为宏逻辑101的运算结果的输出数据被保存于运算数据存储区域106。

在宏逻辑101的调用前，在运算数据存储区域106保存的运算数据根据需要，通过输入选择器107被转送至p个输入寄存器108a，108b,…，108p。共p个输入寄存器108a，108b，…，108p分别作为n种宏逻辑101a，101b，…，101n全部的输入被连接。宏运算控制部102分别控制运算数据存储区域106和输入选择器107，并适当地将运算数据转送至输入寄存器108a,108b,…,108p。在该例中，由于设定浮动小数点运算，因此来自输入选择器107的各输出设定为32比特。在图1等各图中，较粗地示出的信号线是32比特的信号线。

在宏逻辑101的调用后，宏逻辑101的运算结果被保存至q个输出寄存器110a,110b,…,110q。为了在宏逻辑101a,101b,…,101n中也保存被调用的宏逻辑101的运算结果，宏运算控制部102控制选择器109a,109b,…,109q，将被调用的宏逻辑101和输出寄存器110a,110b,…,110q连接。

宏运算控制部102为了将输出寄存器110a,110b,…,110q中保存的输出数据写入运算数据存储区域106，对输出选择器111依次进行切换。应用程序运算开始信号线START112、输入信号线IDAT113、应用程序运算结束信号线114、输出信号线ODAT115、时钟信号线CLK116、复位信号线RST117分别是应用逻辑100与外部模块连接并进行通信所用的输入输出信号线。

应用逻辑100从应用程序运算开始信号线START112接收应用程序运算开始信号，由此开始应用程序运算。应用逻辑100中的应用程序运算所需的运算初始值由输入信号线IDAT113供给。若应用程序运算结束，则应用逻辑100从应用程序运算结束信号线END114发送应用程序运算结束信号。应用逻辑100中的应用程序运算的运算结果由输出信号线ODAT115输出。由时钟信号线116、复位信号线117将时钟信号和复位信号供给至应用逻辑100，应用逻辑100对以宏逻辑101为代表的内部的子模块进行再分配。这样，应用逻辑100进行同步工作。在图中，省略了向应用逻辑100内部的子模块供给的时钟信号线和复位信号线。

图2是表示实施方式1中的应用逻辑100的处理顺序的流程图。

步骤120:若应用程序运算的初始值数据通过输入信号线IDAT113从外部模块到达，则宏运算控制部102将这些初始值数据保存至运算数据存储区域106。若步骤120结束，应用程序运算所需的初始值数据一整套地被完整保存至运算数据存储区域106，则进入步骤121。

步骤121:从外部模块通过应用程序运算开始信号线112发送来应用程序运算开始信号。由于应用逻辑100将应用程序运算开始信号作为触发信号来开始应用程序运算，因此应用逻辑100等待应用程序运算开始信号的接收。若接收到应用程序运算开始信号则进入步骤122，否则进入步骤121。

步骤122:在运算顺序存储区域105中，宏逻辑101的调用顺序以列表的形式被记载。另外，调用宏逻辑101时使用的运算数据的运算数据存储区域106中的地址也被一起记载。宏运算控制部102从运算顺序存储区域读入下次调用执行的宏逻辑的种类及其输入数据的地址。之后，进入步骤123。

步骤123:在宏逻辑101进行运算之前，在输入寄存器108a,108b,…,108n准备输入数据。宏运算控制部102对输入选择器107进行切换，并且按照输入寄存器108a，108b,…,108n的顺序从运算数据存储区域106转送输入数据。若宏逻辑101所需的输入数据在各种输入寄存器108中收集完毕，则进入步骤124。

步骤124:宏运算控制部102经由宏运算开始信号线103向宏逻辑101发送运算开始信号。利用对应的宏运算开始信号线103x发送运算开始信号，以便执行本次要从宏逻辑101a,101b,…,101n中调用的宏逻辑101x的运算。另外，此时，对选择器109进行切换以便将宏逻辑的运算结果数据恰当地保存至输出寄存器110。

步骤125:若宏逻辑101结束了运算，则经由宏运算结束信号线104向宏运算控制部102输出运算结束信号。宏运算控制部102等待运算结束信号的接收。若接收到运算结束信号则进入步骤126，否则进入步骤125。

步骤126:作为宏逻辑101的运算结果的输出数据被保存至输出寄存器110。首先，宏运算控制部102以在输出寄存器中保存的数据不被破坏的方式，对选择器109进行切换来连接输出寄存器的输出和输入。之后，宏运算控制部102对输出选择器111进行切换，由此将输出寄存器110a,110b,…,110q中保存的运算结果数据向运算数据存储区域106转送。若所有的输出数据被转送至运算数据存储区域106，则进入步骤127。

步骤127:宏运算控制部102参照运算顺序存储区域105，确认下次要运算的宏是否存在。若下次要运算的宏存在则进入步骤122，否则进入步骤128。

步骤128:在运算顺序存储区域105中保存的所有的宏逻辑101的运算结束时，在运算数据存储区域106中保存应用程序运算结果的数据。宏运算控制部102经由输出信号线ODAT115，将应用程序运算结果的数据从运算数据存储区域106向外部模块发送。此时，宏运算控制部102经由应用程序运算结束信号线END114，将应用程序运算结束信号向外部模块发送，并通知应用程序运算的结束。

图3和图4是表示实施方式1中的硬件模块的验证方法的图。首先，以硬件描述语言描述作为检查对象的硬件模块。

图3是表示实施方式1中的进行静态验证130时的验证方法的图。在静态验证130中，通过基于形式验证语言的属性描述对硬件模块的功能设计进行验证。形式验证工具133获取以硬件描述语言描述的检查对象131和以形式验证语言描述的检查对象的属性132，并输出检查结果134。若检查结果没有错误，则可以认为硬件模块没有缺陷。

图4是表示实施方式1中的进行动态验证140时的验证方法的图。在动态验证140中，使硬件模块在仿真器中工作，并与有实际验证成果的高信赖性的比较对象比较结果，由此对硬件模块的功能设计进行验证。首先，随机数生成器141利用随机数生成针对硬件模块的输入值142。硬件描述语言仿真器143获取以硬件描述语言描述的检查对象131和输入值142，并输出该硬件模块的输出值145。另外，在动态验证140中，需要用于与输出值145进行比较的输出期待值146。为了得到输出期待值146，设置具有与作为验证对象的硬件模块同等功能，并且有实际验证成果的高信赖性的比较对象144，并将输入值142赋值。最后，比较器147获取输出值145和输出期待值146，输出检查结果148。在检查结果148中，若比较结果不一致，则视为在硬件模块中检测出缺陷。

图5是表示实施方式1中的应用逻辑100的子模块的验证方法的图。宏逻辑A101a、宏逻辑N101n、宏运算控制部102、运算顺序存储区域105、运算数据存储区域106、输入选择器107、输入寄存器108、选择器109、输出寄存器110、输出选择器111通过静态验证130进行验证。宏逻辑B101b通过动态验证140和静态验证130的组合进行验证。电路规模较小、处理内容简单的硬件模块能够通过静态验证130进行验证。

相反，对于电路规模较大、处理内容复杂的硬件模块而言，由于基于形式语言的属性描述的验证较难，因此不仅通过静态验证130，还通过动态验证140进行验证。以宏逻辑B101b为代表的多种宏逻辑由于进行例如使用了单精度浮动小数点数的指数函数的运算，因此电路规模较大、处理内容复杂。对于这样的电路规模较大、处理内容复杂的宏逻辑101而言，除了主模块本身通过动态验证确认无缺陷之外，还进行分割子模块来通过静态验证130进行验证。这样的电路规模较大、处理内容复杂的宏逻辑101较多地对三角函数、指数函数、对数函数等的数学函数进行运算。因此，对于这样的宏逻辑101的动态验证140中的有实际验证成果的高信赖性的比较对象144，例如使用一般在PC上动作的C语言的数学函数库。

图6是表示实施方式1中的电路规模较大、处理内容复杂的宏逻辑101的构成的框图。一般而言，三角函数、指数函数、对数函数等的数学函数通过利用最优近似多项式等进行多项式近似来实现。最优近似多项式能够通过单精度浮动小数点数的四则运算、地板函数、型转换的组合来实现。因此，电路规模较大、处理内容复杂的宏逻辑101成为在内部具有多种单精度浮动小数点数运算逻辑150a,150b,…,150m这样的构成。

在对数学函数通过最优近似多项式等进行多项式近似的情况下，多次重复进行单精度浮动小数点数加法运算和单精度浮动小数点数乘法运算。此时，当然，对于每一次单精度浮动小数点数运算都具有1个单精度浮动小数点数运算逻辑150的处理而言，电路规模效率低。因此，宏逻辑101根据需要，设为每一种类仅具备1个单精度浮动小数点数运算逻辑150，按照宏运算的算法对单精度浮动小数点数运算逻辑150重复调用。

因此，对于单精度浮动小数点数运算逻辑150的输入，分别设置选择器151和寄存器152，能够将宏逻辑101的输入数据、以前的单精度浮动小数点数运算的输出数据作为输入数据进行利用。因此，选择器151a,151b,…,151i,151j根据需要与宏逻辑的输入信号线IN_A154a,…,IN_P154p、单精度浮动小数点数运算逻辑150的输出信号线155a,…,155m连接。

单精度浮动小数点数运算逻辑150、设置成其输入的选择器151被浮动小数点数运算控制部153控制。浮动小数点数运算控制部153经由浮动小数点数运算开始信号线156和浮动小数点数运算结束信号线157与单精度浮动小数点数运算逻辑150连接。

若浮动小数点数运算控制部153经由浮动小数点数运算开始信号线156，向单精度浮动小数点数运算逻辑150发送运算开始信号，则单精度浮动小数点数运算逻辑150开始运算。若单精度浮动小数点数运算逻辑150结束了运算，则经由浮动小数点数运算结束信号线157，向浮动小数点数运算控制部153发送运算结束信号。

浮动小数点数运算控制部153与宏运算开始信号线IVALID103以及宏运算结束信号线OVALID104连接。若从宏运算开始信号线IVALID103接收了宏运算开始信号，则浮动小数点数运算控制部153按照要由宏逻辑101实现的运算的算法，对单精度浮动小数点数运算逻辑150和选择器151进行控制，并进行浮动小数点数运算。

若一整套的浮动小数点数运算结束，则输出值处理部158对从单精度浮动小数点数运算逻辑150的输出信号线155a,…,155m、异常信号线159a,…,159m获取的数据进行数字处理，并从宏逻辑输出信号线OUT_A160a,…,OUT_Q160q输出宏输出数据。此时，浮动小数点数运算控制部153经由宏运算结束信号线104发送运算结束信号。另外，宏逻辑101被从时钟信号线CLK116和复位信号线RST117分别供给了时钟信号和复位信号，并将时钟信号和复位信号再分配给内部的各子模块。由此，宏逻辑101进行同步工作。

在图中省略了向宏逻辑101内部的子模块供给的时钟信号线和复位信号线。另外，宏逻辑的输入信号线IN_A154a,…,IN_P154p分别根据需要与应用逻辑100中的各输入寄存器108a,…,108p连接，宏逻辑输出信号线OUT_A160A,…,OUT_Q160q根据需要与应用逻辑100中的选择器109a,…,109q连接。

图7是表示实施方式1中的电路规模较大、处理内容复杂的宏逻辑101的处理顺序的流程图。

步骤170:宏逻辑101将经由宏运算开始信号线IVALID103从宏运算控制部102发送来的运算开始信号作为触发来进行宏运算。若浮动小数点数运算控制部153接收了运算开始信号则进入步骤171，否则进入步骤170。

步骤171:浮动小数点数运算控制部153按照宏逻辑101的运算算法的顺序执行单精度浮动小数点数运算逻辑150的运算。因此，选择在算法的当前的步骤中要执行的单精度浮动小数点数运算逻辑150及其输入数据，对选择器151进行切换。之后，进入步骤172。

步骤172:浮动小数点数运算控制部153经由浮动小数点数运算开始信号线156将开始信号向单精度浮动小数点数运算逻辑150发送。之后，进入步骤173。

步骤173:单精度浮动小数点数运算逻辑150若结束了运算，则经由浮动小数点数运算结束信号线157，向浮动小数点数运算控制部153输出浮动小数点数运算结束信号。浮动小数点数运算控制部153等待浮动小数点数运算结束信号的接收。若接收了浮动小数点数运算结束信号则进入步骤174，否则进入步骤173。

步骤174:浮动小数点数运算控制部153若接收了浮动小数点数运算结束信号，则更新内部状态，并使宏逻辑101的运算算法进入到下一步骤。在运算算法结束的情况下进入步骤175，否则进入步骤171。

步骤175:输出值处理部158通过利用经由输入信号线IN_A154a,…,IN_P154p接收的输入数据、从单精度浮动小数点数运算逻辑的输出信号线155a,…,155m、异常信号线159a,…,159m接收的运算数据来生成宏逻辑101的运算结果数据，并经由宏逻辑输出信号线OUT_A160a,…,OUT_Q160q来发送运算结果数据。之后，进入步骤176。

步骤176:浮动小数点数运算控制部153经由宏运算结束信号线OVALID104发送宏运算结束信号。

图8是表示实施方式1中的宏逻辑101的子模块的验证方法的图。选择器151、寄存器152、浮动小数点数运算控制部153和输出值处理部158通过静态验证130进行验证。单精度浮动小数点数运算宏逻辑A150a,…、单精度浮动小数点数运算宏逻辑M150m通过动态验证140和静态验证130的组合进行验证。

对于单精度浮动小数点数运算逻辑150，由于电路规模较大、处理内容复杂，因此主模块的静态验证130较难。因此，单精度浮动小数点数运算逻辑150的主模块通过动态验证140进行验证，作为有实际验证成果的高信赖性的比较对象144、例如使用一般搭载于PC上、符合IEEE754标准的单精度浮动小数点数运算器。单精度浮动小数点数运算逻辑150进行子模块分割并进行静态验证130。

图9是表示实施方式1中的单精度浮动小数点数运算逻辑150的构成的图。

输入比较部180输出经由输入信号线IN_0 181，IN_1 182获取的输入数据的比较结果。

符号部处理部183使用输入比较部180的比较结果来处理输入数据的符号部。

指数部处理部184使用输入比较部180的比较结果来处理输入数据的指数部。

尾数部处理部185使用输入比较部180的比较结果和指数部处理部184的处理结果来处理输入数据的尾数部。

指数部调整部186使用指数部处理部184的处理结果和尾数部处理部185的处理结果来进行要输出的指数部的调整。

异常处理部187使用输入数据和指数部调整部186的调整结果来处理浮动小数点数异常。

输出值处理部188利用符号部处理部183的处理结果、尾数部处理部185的处理结果、指数部调整部186的处理结果和异常处理部187的处理结果，生成单精度浮动小数点数运算逻辑150的运算结果数据，并分别经由输出信号线OUT155和异常信号线EXCEPTION159输出。

单精度浮动小数点数运算逻辑150在经由浮动小数点数运算开始信号线IVALID156获取了浮动小数点数运算开始信号后开始运算。

运算循环数计数部189向输入比较部180、符号部处理部183、指数部处理部184、尾数部处理部185、指数部调整部186、异常处理部187、输出值处理部的单精度浮动小数点数运算逻辑150的子模块通知经过循环数，能够进行它们内部中的重复处理。

单精度浮动小数点数运算逻辑150的子模块进行重复处理，由此能够节约电路规模。

运算循环数计数部189在获取了浮动小数点数运算开始信号后开始对运算循环数进行计数，在浮动小数点数运算结束的定时从浮动小数点数运算结束信号线OVALID157输出浮动小数点数运算结束信号。

图10是表示实施方式1中的单精度浮动小数点数运算逻辑150的子模块的验证方法的图。对输入比较部180、符号部处理部183、指数部处理部184、尾数部处理部185、指数部调整部186、异常处理部187、输出值处理部188、运算循环数计数部189全部通过静态验证130进行验证。在通过单精度浮动小数点数运算逻辑150的运算方式、安装方法等，形式验证的属性描述较难的情况下，能够对这些子模块进一步进行子模块分割来通过静态验证130进行验证。

由此，构成应用逻辑100的硬件模块都通过静态验证130进行验证。另外，通过以宏逻辑101、浮动小数点数运算逻辑150等的在安装方面有意义的单元进行动态验证140，可容易发现硬件模块的缺陷。由此，应用逻辑100能够被开发成与IEC61508SIL4相当的高安全性。另外，单精度浮动小数点数运算逻辑150被从时钟信号线CLK116、复位信号线RST117分别供给时钟信号和复位信号，并向内部的各子模块再分配时钟信号和复位信号。由此，单精度浮动小数点数运算逻辑150进行同步工作。在图中，省略了向宏逻辑101内部的子模块进行供给的时钟信号线和复位信号线。

【实施例2】

在实施方式1中示出的应用逻辑100为了节约电路规模而构成为将各种宏逻辑101a,…,101n按每一种类仅配置1个。因此，在实施方式1中能够节约电路规模，但作为不利的一面，存在难以根据电路图理解宏逻辑101的运算顺序、应用逻辑100的运算内容的问题。在实施方式2中，通过运算顺序、应用程序运算的内容在视觉上容易理解的构成配置宏逻辑101。

图11是表示实施方式2中的应用逻辑100的构成的图。宏逻辑101以功能框图的形式配置在应用逻辑100的内部。在这些宏逻辑101中，一部分经由输入信号线190与运算数据存储区域106连接，接收初始值数据的供给。另外，这些宏逻辑中的一部分经由输出信号线191与运算数据存储区域106连接，将运算结果数据保存于运算数据存储区域106。

以功能框图的形式配置的宏逻辑101经由输入输出信号192相互连接，各个宏逻辑101的输出数据能够作为其他的宏逻辑101的输入数据，不经由运算数据存储区域106地直接输入输出。另外，以功能框图的形式配置的宏逻辑101通过运算控制信号线194相互连接，以便某一宏逻辑101的宏运算结束信号线OVALID作为其他的宏逻辑101的宏运算开始信号线IVALID而被连接。即，在1个运算控制信号线194中流动的运算控制信号若从某一宏逻辑101来看是宏运算结束信号，若从其他的宏逻辑101来看是宏运算开始信号。

因此，在功能框图中相互连接的宏逻辑101通过运算控制信号线194被串联地连接成珠串连接状，沿着运算控制信号的流向进行宏逻辑101的运算。此时，需要留意到排在之前的宏逻辑101的输出数据一定成为排在之后的宏逻辑的输入数据来设计应用逻辑100。

最开始执行的宏逻辑101的宏运算开始信号线IVALID是应用程序运算开始信号线START112，最后执行的宏逻辑101的宏运算结束信号线OVALID是应用程序运算结束信号线END114。对于实施方式2中的硬件模块的验证而言，针对宏运算控制部102和运算数据存储区域106通过静态验证130执行，针对宏逻辑101与实施方式1同样地，如图8/图10所示那样通过静态验证130和动态验证140的组合执行。

【实施例3】

在实施方式3中，是实施方式1中示出的应用逻辑100的设计方法。

在图12中示出了实施方式3中的应用程序开发画面200。对于开发与IEC61508SIL4相当的高安全性的应用程序而言，需要不是基于字符用户界面而是基于图形用户界面的、利用视觉性且直观的基于模型的开发。因此，应用程序开发者将能够进行应用程序中所需的宏运算的软件宏201配置于应用程序开发画面200，由此进行应用程序的开发。

在开发应用程序时，准备软件宏库202。在软件宏库202中，备齐对应用程序进行开发时所需的种类的软件宏A201a，软件宏B201b,…,软件宏N201z。应用程序开发者通过从软件宏库202将希望配置的软件宏201向应用程序开发画面200拖拽203来开发应用程序。

另外，对应用程序开发画面200中配置的软件宏201分别赋予连续编号204。在应用程序运算中利用英文数字指定对软件宏201不是进行并行处理而是串行执行时的执行顺序的编号是连续编号204。连续编号204在将应用程序安装于应用逻辑100时是必须的。

图13是表示实施方式3中的软件宏库与宏逻辑库的一对一对应关系210的图。对于为了开发应用程序而使用的软件宏201的库亦即软件宏库202，准备作为宏逻辑101的库的宏逻辑库211。针对软件宏库202中包含的各种软件宏A201a,软件宏B201b,…,软件宏N201z，在宏逻辑库211中分别包含同等的运算的宏逻辑A101a,宏逻辑B101b,…,宏逻辑Z101z。

即，软件宏A201a和宏逻辑A101a是进行同等的运算的宏，软件宏B201b和宏逻辑B101b是进行同等的运算的宏，…，软件宏Z201z和宏逻辑Z101z是进行同等的运算的宏。因此，软件宏库202中包含的软件宏201与宏逻辑库211中包含的宏逻辑101是一对一对应的关系。

软件宏201和宏逻辑101的差异在于，宏逻辑101是硬件因此具有时钟信号线116和复位信号线117，另外应用逻辑100为了控制宏逻辑101而具有宏运算开始信号线103和宏运算结束信号线104。虽然在这样的界面中存在这样的差异，但软件宏201和宏逻辑101分别进行同等的运算。

软件宏201和宏逻辑101分别进行同等的运算这一情况通过静态验证130、动态验证140进行验证。在使用静态验证130的情况下，首先将软件宏201高位合成至硬件描述语言。以硬件描述语言描述的检查对象131是以硬件描述语言描述的软件宏201与宏逻辑101的双方的组合。对于以形式验证语言描述的检查对象的属性132，对以硬件描述语言描述的软件宏201和宏逻辑101的输入若相等则输出也相等的情况进行属性描述。在使用动态验证140的情况下，以硬件描述语言描述的检查对象131是宏逻辑101，有实际验证成果的高信赖性的比较对象144是软件宏201。

图14是表示实施方式3中的应用逻辑设计方法的图。示出至根据应用程序开发者开发的应用程序220和软件宏库202生成应用逻辑100。宏连接信息提取部221根据应用程序220中的软件宏201、连续编号204、软件宏库与宏逻辑库的一对一对应关系210的信息输出宏逻辑运算顺序222。

通过按照对软件宏201赋予的连续编号204的顺序排列软件宏201而得到软件宏201的运算顺序，根据软件宏201的运算顺序和软件宏库与宏逻辑库的一对一对应关系210得到宏逻辑运算顺序222。另外，宏连接信息提取部221根据应用程序220中的软件宏201彼此的连接信息，输出对软件宏的输入输出数据赋予的输入输出地址223。并且，宏连接信息提取部进行将应用程序开发者以10进制输入的应用程序220中的常数值转换成单精度浮动小数点数的处理等，并作为常数数据224输出。宏逻辑利用信息提取部225对应用程序220中利用的软件宏201的种类进行调查，根据软件宏库和宏逻辑库的一对一对应关系210提取利用的宏逻辑101，并作为宏逻辑利用信息226输出。运算顺序存储区域105基于宏逻辑运算顺序222和输入输出地址223所记载的信息而被开发。运算数据存储区域106基于输入输出地址223和常数数据224所记载的信息而被开发。作为搭载于应用逻辑100的宏逻辑101的种类的宏逻辑A101a,宏逻辑101b,…,宏逻辑101n与宏逻辑利用信息226中记载的信息一致。

【实施例4】

在实施方式4中，是实施方式1中示出的应用逻辑100的设计方法。

图15示出了实施方式4中的应用程序开发画面200。也可以不通过实施方式3的图12所示的连续编号204，而是通过使软件宏201具有运算控制信号线193来指定运算顺序。为了连接运算控制信号线193，使软件宏201也分别具有宏运算开始信号线103和宏运算结束信号线104。在应用程序开发者开发应用程序220时，将某一软件宏201的宏运算结束信号线104作为下一个运算顺序的另一软件宏201的宏运算开始信号线103进行连接，设为运算控制信号线193。软件宏201通过运算控制信号线193，按照运算顺序成为珠串连接。运算控制信号在运算控制信号线193传输，由此进行应用程序运算。

图16是表示实施方式4中的应用逻辑设计方法的图。宏连接信息提取部231按照应用程序220中运算控制信号线194连接的顺序遍历软件宏201，得到软件宏201的运算顺序。根据软件宏的运算顺序和软件宏库与宏逻辑库的一对一对应关系210得到宏逻辑运算顺序222。

【实施例5】

在实施方式5中，是实施方式2所示的应用逻辑100的设计方法。

图17是表示实施方式5中的应用逻辑设计方法的图。在本实施例中，设为对应用程序220中的软件宏201的运算顺序的指定使用连续编号204的情况。根据软件宏库和宏逻辑库的一对一对应关系210，将应用程序220中的软件宏201置换成宏逻辑101，基于宏连接信息提取部221所输出的宏逻辑运算顺序222来将运算控制信号线194以珠串连接的方式连接，由此得到应用逻辑中的宏逻辑的功能框图230。

【实施例6】

在实施方式6中，是实施方式2所示的应用逻辑100的设计方法。

图18是表示实施方式6中的应用逻辑设计方法的图。在本实施例中，设为对应用程序220中的软件宏201的运算顺序的指定使用运算控制信号线194的情况。根据软件宏库和宏逻辑库的一对一对应关系210，将应用程序220中的软件宏201置换成宏逻辑101，由此得到应用逻辑中的宏逻辑的功能框图230。

如上述实施例中说明的那样，本发明的一实施例的安全保护系统应用逻辑被分割成分层构成的多个功能模块，可容易地按功能模块任意地应用基于形式验证语言的静态验证或动态验证。通过一实施例的验证方法验证的应用逻辑能够按功能模块应用静态验证。因此，根据基本安全标准IEC61508的定义，通过基于形式验证语言的静态验证验证的逻辑满足与SIL4相当的安全性的要件。

另外，在实施例的分层结构中，应用逻辑的运算通过宏逻辑的组合实现。宏逻辑根据需要在内部包含浮动小数点数运算逻辑。宏逻辑和浮动小数点数运算逻辑分别通过基于仿真的动态验证进行验证。因此，本发明的安全保护系统应用逻辑能够通过基于形式验证语言的静态验证和基于仿真的动态验证的组合而被全面地验证。

这样的信赖性高的应用逻辑及其设计方法例如能够应用于核反应堆仪控装置的安全保护系统。作为一般的应用例，在通过将浮动小数点数运算逻辑搭载于内部的数十种宏逻辑的组合开发的应用逻辑中，使构成应用逻辑的所有功能模块通过基于属性描述的形式验证等的静态验证成为验证完毕，另外浮动小数点数运算逻辑、宏逻辑通过基于仿真的动态验证成为验证完毕，由此能够提供信赖性高的应用逻辑。

本发明不被限定于上述实施方式，包含各种变形例。例如，能够将某一实施例的构成的一部分置换成其他的实施例的构成，另外，能够对某一实施例的构成附加其他的实施例的构成。另外，针对各实施例的构成的一部分，能够进行其他的实施例的构成的追加、删除、置换。