源代码转换方法和源代码转换程序

技术领域

本发明涉及源代码转换方法和源代码转换程序，特别涉及在软件的模型检查中，使用计算机将软件的源代码转换为检查代码的情况下，能够验证系统（软件）的非功能即处理性能的技术。

背景技术

近年来，软件系统在一般社会中无处不在，对软件要求的可靠性变得非常高，另一方面，软件持续地复杂化和大规模化，通过手工作业的检查和测试进行的品质保障变得非常困难。

模型检查技术例如是非专利文献1中公开的方法，是用特定模型检查器的输入语言描述软件的行为，通过执行特定模型检查器，遍历上述软件可能成为的状态检查上述软件是否满足应该具有的性质的技术。根据非专利文献1中公开的方法，用称为Promela的输入语言描述软件的行为，输入被称为SPIN的模型检查器，由此对于软件应该要满足的功能性质实施检查。

并且，根据非专利文献6中公开的方法，用时间自动机（automaton）表现软件的行为和时间约束，输入到称为UPPAAL的模型检查器，由此对于软件应该要满足的处理时间实施检查。

模型检查技术是对专注于持续复杂化和大规模化的软件的品质保障有前途的技术，但为了遍历软件能够成为的状态地进行检查，在大规模的软件中，可能发生要检查的状态数量庞大的被称为状态爆炸的现象，引起处理所需的时间计算量成为现实中不能容许的大小的现象、或处理所需的空间计算量超过用于处理的计算机中搭载的存储区域的现象的双方或一方，可能不能够完成检查。

为了对应状态爆炸，对源代码或检查代码进行称为抽象化的处理，将状态数削减至能够检查的范围。抽象化例如是选择性执行语句的分支条件的简略化。因为抽象化，可能产生本来不存在的执行路径、或者存在的执行路径消失，所以对检查代码的检查结果呈现的软件的性质与本来的软件的性质可能产生差异。因此，优选鉴于对软件想要检查的性质，在研究抽象化的水平的基础上，应用抽象化。

并且，在模型检查技术中，用特定模型检查器的输入语言描述检查对象的软件的工作量较大，可能成为实际应用上的问题。专利文献1中公开的方法中，源代码被用翻译映射表转换为用特定模型检查器的输入语言书写的检查代码。对于检查代码，使用与上述转换不同的由用户定义的环境模型，用上述特定模型检查器检查。此外，根据专利文献2中公开的方法，从源代码转换为中间表达形式，生成满足实时约束的参数，由此生成带参数的时间自动机。

图15表示现有例的使用计算机的模型检查技术的一例。现有例的模型检查系统中，首先使设计模型化，接着生成与执行环境匹配的时间自动机，进行自动检查。通过该自动检查，对于检查对象的软件进行遍历的性能确认。

此外，模型驱动型开发是软件的开发技术之一。模型驱动型开发是将软件的设计信息描述为模型，对于该模型用转换操作细化，由此进行软件开发的技术。例如，在模型驱动型开发中，模型的形式（format）和含义由利用非专利文献2中公开的方法即MOF描述的元模型规定，用非专利文献3中公开的方法即QVT描述使模型细化的转换规则，用非专利文献4中公开的方法即OCL进行与模型的一致性和健全性相关的约束的描述和验证，用非专利文献5中公开的方法即MOFM2T根据模型生成源代码。

其中，模型检查技术中的“模型”与模型驱动型开发中的“模型”是相互独立的概念，一般没有与数据结构和含义等相关的共通性。

现有技术文献

专利文献1：日本特开2000-181750号公报

专利文献2：WO2004/038620号公报

非专利文献1：Gerard J.Holzmann,"The SPIN Model Checker:Primer and Reference Manual",Addison-Wesley Professional,2003,ISBN:978-0321228628

非专利文献2：The Object Management Group,"Meta Object Facility(MOF)Core Specification",formal/06-01-01,January2006,http://www.omg.org/spec/MOF/2.0/PDF

非专利文献3：The Object Management Group,"Meta Object Facility(MOF)2.0Query/View/Transformation Specification",formal/2008-04-03,April,2008,http://www.omg.org/spec/QVT/1.0/PDF

非专利文献4：The Object Management Group,"Object ConstraintLanguage",formal/2006-05-01,May2006,http://www.omg.org/spec/OCL/2.0/PDF

非专利文献5：The Object Management Group,"MOF Model to TextTransformation Language,v1.0",formal/2008-01-16,January2008,http://www.omg.org/spec/MOFM2T/1.0/PDF

非专利文献6：Gerd Behrmann,Alexandre David and Kim G.Larsen,"A Tutorial on Uppaal",Formal Methods for the Design of Real-TimeSystems Lecture Notes in Computer Science,2004,Volume3185/2004

发明内容

为了有效地实施利用模型检查对软件可靠性的确保，需要用根据源代码自动生成用模型检查器的输入语言描述的检查用代码等的方法，减少用于得到检查用代码的工作量，并且需要对于软件的规格和设计进行抽象化，使得基于模型检查器的遍历检查以现实的时间计算量和空间计算量结束。

此外，关于处理性能，实际上因为缓存和总线的使用状况/外部机构的物理制约等原因而会稍偏离设计值，所以需要按照所选择的抽象水平测定实测数据，确认验证结果的妥当性。

但是，根据专利文献1中公开的方法，存在以下课题：（1）难以变更抽象化的水平，（2）对软件设计变更的追踪成本较高，（3）用不同的模型检查器进行检查时的成本较高，（4）用由用户选择的抽象化水平测定处理时间时的成本较高。

关于上述课题（1），根据专利文献1中公开的方法，翻译映射表的变更仅限定于源代码的修改等新类型的命令导入源代码内的情况。因此，用户变更抽象化的水平的方法，限定于对转换前的检查对象的源代码施加修正的方法、和对转换后的用特定模型检查器的输入语言书写的检查代码施加修正的方法、和对环境模型施加修正的方法，无论哪一种方法，用户都要花费较大的工作量。

关于上述课题（2），根据专利文献1中公开的方法，发生使用的库的变更等变更时，需要进行翻译映射表的修正，和环境模型的修正。但是，翻译映射表由从上述源代码直接转换为上述检查代码的映射表元素构成，且环境模型用特定模型检查器的输入语言书写，因此难以为了追踪设计变更而在保持一致性的同时进行修正。

关于上述课题（3），根据专利文献1中公开的方法，为了用不同的模型检查器进行检查，需要进行翻译映射表的修正和环境模型的修正。但是，翻译映射表由从上述源代码直接转换为上述检查代码的映射表元素构成，且环境模型用特定模型检查器的输入语言书写，因此需要对翻译映射表和环境模型全部修正，需要较大的成本。

关于上述课题（4），根据专利文献2中公开的方法，不能够按照用户选择的抽象度插入观测用的代码，需要另外手动插入源代码，需要较大的成本。

此外，用户只能够实施功能要件的检查，所以为了进行非功能要件的验证，用户需要以要检查的水平手动生成检查代码，存在成本高、再利用性低等课题。

此外，存在用户一侧要管理检查水平与状态数的权衡的需求。即，复杂的系统的检查中，容易发生状态爆炸，不能够完成检查。此时，存在与不能进行任何检查相比，优选即使降低一些水平也能够完成检查的情况。例如，存在仅在循环执行时发生的特定的错误的情况下，通过除去该循环，虽然不能够检测特定的错误，但能够大幅削减状态数。

此外，图15所示的使用模型检查技术的自动的、遍历的性能验证技术中，理论值偏离实测值的情况较多。即，因为基于实现方法的影响度较大，所以理论值与实测值的偏差容易变大。因此，需要计测实测值的手段。

本发明的目的在于鉴于现有技术的课题，提供一种源代码转换方法和源代码转换程序，其能够容易地生成以用户要检查的水平进行非功能要件的验证的检查代码，实现成本降低和再利用性提高。

本发明的其他目的在于提供一种源代码转换方法和源代码转换程序，其能够灵活地对应抽象化的水平等，能够在源代码中插入符合抽象化水平的测定观测用的代码，测定理论值与实测值的偏差，使检查水平与状态数的权衡变得容易。

本发明的代表性的方面如下所述。本发明的利用源代码转换装置的源代码转换方法的特征在于，具有：输入软件的源代码的步骤；输入不同的多个转换规则的步骤；输入与处理性能相关的约束（制约）即非功能规则的步骤；和用上述不同的多个转换规则和上述非功能规则将上述源代码转换为用验证工具的输入语言描述的非功能检查代码的步骤。

根据本发明，具有输入以细粒度分割的多个转换规则和非功能规则的接口。因此，用户对抽象化水平的变更、和非功能要件的验证，可以通过选择输入与检查对象的源代码对应的不同的多个转换规则的操作而容易地实现。由此，即使是复杂的大规模软件，也能够以用户选择的水平容易地进行所输入的源代码的功能要件和非功能要件的验证，能够大幅降低检查用代码等的软件开发成本。

附图说明

图1是用于说明本发明的基本概念的图。

图2是说明本发明的源代码转换处理中的转换规则的输入接口的图。

图3是表示本发明的第一实施例的源代码转换系统的结构例的图。

图4是表示图3的转换系统中的源代码转换装置的结构例的图。

图5是表示第一实施例的处理流程的例子的图。

图6是说明第一实施例的源代码转换装置的动作的图。

图7是更加详细地说明第一实施例的源代码转换的流程的图。

图8A是说明通过第一实施例的源代码转换得到自动机的图。

图8B是表示第一实施例中的源代码转换技术的整体概况的图。

图9是表示本发明的第二实施例的包括源代码转换装置的源代码转换系统的结构例的图。

图10是表示第二实施例中的源代码转换装置的结构例的图。

图11是表示本发明的第二实施例的源代码转换装置的处理流程的例子的图。

图12是说明第二实施例的源代码转换装置的动作的图。

图13是说明第二实施例的源代码-实现模型转换对应表（Table-A～C）的结构例和功能的图。

图14是说明第二实施例的源代码转换的流程的图。

图15是表示现有例的源代码转换装置的一例的图。

符号说明

0001    源代码

0002    转换规则

0003    元模型

0004    书写规则

0005    非功能规则

0006    非功能检查代码

0007    非功能检查代码

0008    带计测源代码

1000    源代码检查装置

1001    源代码信息

1002    元实现模型

1003    元泛化模型

1004    元检查模型

1005    实现-泛化转换规则

1006    抽象化转换规则

1007    泛化-检查转换规则

1008    检查模型

1009    检查代码书写规则

1100    输入部

1101    源代码输入部

1102    转换规则输入部

1200    转换处理部

1201    模型构建部

1202    实现-泛化模型转换部

1203    抽象化模型转换部

1204    非功能约束附加处理部

1209    泛化-检查模型转换部

1205    实现模型

1206    泛化模型

1300    输出部

1301    检查代码输出部

1400    存储部

1401    转换规则数据库

1402    元模型数据库

1403    书写规则数据库

1404    非功能规则数据库

1500    控制部

2000    模型检查工具

4000    实测装置

S101    源代码输入步骤

S102    转换规则输入步骤

S103    转换规则应用步骤

S104    检查代码输出步骤

具体实施方式

本发明中，为了能够验证软件的非功能即处理性能，使用不同的多个转换规则，将检查对象的源代码转换为用模型检查器的输入语言描述的带有非功能的检查代码。上述不同的多个转换规则，对于将检查对象的源代码转换为用模型检查器的输入语言描述的带有非功能的检查代码、并进行抽象化的一系列处理以细粒度分割，通过组合使用多个转换规则，实现从上述源代码向上述带非功能的检查代码的转换。

在本发明中，对于将检查对象的源代码转换为带非功能的检查代码的一系列处理，包括抽象化处理在内以细粒度分割，将分割后的各处理称为“转换规则”。此外，带有非功能的检查代码指的是，检查代码，关于以细粒度分割后的各处理被附加有能够验证非功能要件和功能要件的非功能约束的检查代码（以下简称为非功能检查代码）。并且，“非功能规则”定义为用于将非功能（与处理性能相关的约束）转换为检查代码的转换规则。

通过本发明实现的源代码转换装置，具有在将源代码转换为检查代码时，用于不同的多个转换规则、“非功能规则”被用户选择并输入的接口。上述转换规则、“非功能规则”，通过从事先存储在源代码转换装置内部的多个转换规则、“非功能规则”中选择和由用户描述这些方式中的任意一种方式被输入。

此外，本发明中，转换规则可以分类为：将源代码转换为不依赖于上述源代码的描述语言的具有泛化的程序信息的形式（泛化模型）的实现（implementation）-泛化转换规则；对泛化模型进行抽象化的抽象化转换规则；和将泛化模型转换为模型检查器的描述语言的泛化-检查转换规则。换言之，不同的多个转换规则可以分类为：将源代码转换为不依赖于特定的编程语言的形式即中间形式的第一转换规则；对上述中间形式进行抽象化处理的第二转换规则；和从上述中间形式转换为上述非功能检查代码的第三转换规则。从源代码到非功能检查代码的转换，通过连续进行利用实现-泛化转换规则将源代码转换为泛化模型的步骤、用抽象化转换规则对上述泛化模型进行抽象化的步骤、对该抽象化后的上述泛化模型附加非功能的约束的步骤、和用泛化-检查转换规则将该泛化模型转换为非功能检查代码的步骤这四个步骤而实现。

换言之，从源代码向检查代码的转换，通过连续进行：将上述第一、第二、第三转换规则分别进行输入1个以上的步骤、用上述第一转换规则将软件的源代码转换为上述中间形式的步骤、用上述第二转换规则对以上述中间形式表现的软件进行抽象化的步骤、用非功能规则对上述中间形式附加非功能的约束的步骤、和用上述第三转换规则将上述中间形式转换为用验证工具的输入语言描述的验证用代码的步骤这四个步骤而实现。

此外，在本发明中，在将检查对象的源代码转换为检查代码的一系列处理中，内部保存的信息（模型）的形式由元模型定义。上述模型可以分类为：具有与检查对象的源代码对应的信息的实现模型；上述泛化模型；和具有与模型检查器的描述语言对应的信息的检查模型。实现模型由其元模型即元实现模型定义，泛化模型由其元模型即元泛化模型定义，检查模型由其元模型即元检查模型定义。上述各个元模型，具有数据结构的定义和与数据中包括的元素间的约束相关的信息。

此外，根据本发明的其他实施方式，具有：用上述不同的多个转换规则将上述中间形式转换为抽象化中间形式，进而转换为非功能检查代码的步骤；对上述抽象化中间形式附加观测点的步骤；用上述不同的多个逆转换规则将附加有上述观测点的抽象化中间形式转换为附加有观测点的中间形式的步骤；和用上述不同的多个逆转换规则将上述附加有观测点的中间形式转换为附加有观测点的源代码的步骤。

以下参照附图详细说明本发明的实施方式。

首先，参照图1、图2说明本发明的基本概念。本发明中，对于源代码进行组合有多个转换规则的转换处理，由此转换为适合现有模型检查装置的非功能检查代码。即：（a）对“转换”以细粒度分割，作为多个“转换规则”的组合形成组件（package），由此实现灵活的转换。（b）用户（检查者）输入检查对象的源代码0001，选择与对象的源代码和检查水平相应的“转换规则”0002，通过转换处理1000对用中间形式表现的软件进行抽象化，对于该抽象化后的软件的各组件（功能）附加基于非功能规则0005的非功能的约束，由此得到所要求的非功能检查代码0006。对于非功能检查代码0006，进一步在模型检查工具2000中判定是否满足系统的约束条件。不满足约束条件的情况下，修正源代码并重复转换处理1000。这样，生成满足系统的约束条件的非功能检查代码0006。

列举本发明中的“转换规则”的例子，如下所述：

（a）单纯的语法转换

将“C语言的条件分支（If语句、Switch语句）”转换为“检查代码的条件分支（If语句）”

将“C语言的循环语句（for语句、while语句）”转换为“检查代码的循环（Do语句）”

（b）外部环境的模型化

将“读取数据”置换为“随机输入”

（c）抽象化

“除去循环”

“简化条件”

此外，本发明中的“非功能”规则中有时间约束、容量约束。即，本发明中的非功能要件中，包括处理时间、存储器使用量、或者双方。

根据图2补充说明本发明的源代码转换处理的转换规则的输入接口。

根据本发明，通过具有输入以细粒度分割的多个转换规则0002的接口，可以用选择、输入多个不同的转换规则的操作容易地实现基于用户的对抽象化水平的变更。即，用户对抽象化水平的变更，可以通过与域信息、要检查的性质、检查水平的信息（抽象化对性质的影响）相应地，由用户选择调用多个不同的转换规则，对源代码转换处理装置1000输入的操作而容易地实现。

本发明特别是对于系统（软件）的功能要求和非功能（处理性能）要求的验证有效的技术。即，通过具有输入非功能规则0005的接口，能够生成附加有对于基于用户进行了抽象化后的软件的各组件（功能）的非功能约束的、所要求的非功能检查代码0006，容易验证非功能要件。

此外，非功能检查代码0006是对以细粒度分割的状态的中间形式应用“转换规则”、“非功能”规则而生成的。该非功能检查代码0006需要判定是否满足作为系统整体的约束条件，具有将其输入到模型检查工具2000，并判定其结果的功能（3000）。

根据本发明，通过提供在以用户选择的水平将源代码转换为检查代码后追加非功能要件的单元，能够进行用户指定的水平的非功能检查。

此外，根据本发明，能够进行与用户选择的抽象化水平符合的实测数据的观测，能够观测理论值与实测值的背离，能够容易地解决检查水平与状态数的权衡。

实施例1

接着，参照图3至图11B说明本发明的第一实施例的源代码转换装置和转换处理方法。

图3是表示第一实施例的包括源代码转换装置的源代码转换系统的结构例的图。本发明的实施方式中应用的源代码转换装置1000，是将检查对象的源代码转换为非功能检查代码0006的装置，具有输入部1100、转换处理部1200、输出部1300、存储部1400和控制部1500。2000表示模型检查工具，3000表示检查结果的判定功能。存储部1400中，保存有转换规则0002、元模型0003、书写规则0004和非功能规则0005。此外，对于模型检查工具2000给出系统约束条件0009。

图4表示源代码转换装置1000的结构例。输入部1100具有源代码输入部1101、转换规则输入部1102、非功能规则输入部1103。转换处理部1200具备模型构建部1201、实现-泛化模型转换部1202、抽象化模型转换部1203、非功能约束附加处理部1204和泛化-检查模型转换部1209。输出部1300具有非功能检查代码书写部1301。存储部1400具有转换规则数据库1401、元模型数据库1402、书写规则数据库1403和非功能规则数据库1404。

源代码转换装置1000例如作为在1台计算机、或者通过网络连接的多台计算机上工作的程序实施。源代码0001、转换规则集合0002、非功能规则0005，例如通过从计算机上的存储装置读取的方法、和利用与计算机连接的输入设备直接输入的方法等方法被输入。此外，非功能检查代码0006例如通过对计算机的存储装置书写的方法、和在计算机的显示装置上显示的方法等被输出。

输入部1100受理由用户输入的数据，进行对转换处理部1200供给被输入的数据的处理。输入部1100具备对与源代码0001相关的信息进行输入、修正的源代码输入/修正部1101、输入与以细粒度分割的多个转换规则即“转换规则集合”0002相关的信息的转换规则输入部1102、和输入非功能规则0005的非功能规则输入部1103，对转换处理部1200供给所受理的各输入。在某个实施方式中，输入部1100也可以受理与由用户对转换处理部的驱动和控制、输出部的驱动和控制相关的指示。

转换处理部1200从输入部供给源代码0001的信息、要对源代码0001应用的转换规则集合0002的信息、和非功能规则0005，进行利用转换规则集合0002对源代码0001进行转换并附加非功能的处理，将转换结果的信息对输出部1300供给。在某个实施方式中，也可以是与从输入部供给的转换规则集合0002相关的信息仅包括指示出存储部中保存的转换规则的识别信息，使用上述识别信息从存储部1400读取转换规则集合0002的实体用于转换。

转换处理部1200具有模型构建部1201、实现-泛化模型转换部1202、抽象化模型转换部1203、非功能约束附加处理部1204、和泛化-检查模型转换部1209。在本实施方式中，转换处理部1200如图6所示，通过元模型和使用转换规则的模型转换，将源代码信息1001转换为检查模型1008。元实现模型1002、元泛化模型1003和元检查模型1004，例如用非专利文献2中记载的MOF描述。此外，例如用非专利文献3中记载的QVT描述实现-泛化转换规则1005、抽象化转换规则1006、和泛化-检查转换规则1007，进行模型的转换。上述转换中，也可以是与已举例的方法以外的模型转换方法，或者同时混用多个方法。

此外，在某个实施例中，也可以使实现-泛化模型转换部1202、抽象化模型转换部1203、非功能约束附加处理部1204、泛化-检查模型转换部1209不分别独立，而是用同一部位进行，进而，作为实现模型1205、泛化模型1206、检查模型1008各自的元模型，也可以不分别地准备元实现模型1002、元泛化模型1003、元检查模型1004，而是用单一的元模型定义实现模型1205、泛化模型1206和检查模型1008。此外，在某个实施例中，对于元实现模型1002、元泛化模型1003、元检查模型1004，也可以用多个方式分别定义实现模型1205、泛化模型1206、检查模型1008的形式和约束。例如，也可以有各个元模型在基于上述MOF的定义外，也包括非专利文献4中记载的用OCL记载的约束条件，进行模型的转换时，进行是否满足约束条件的验证的方法。

模型构建部1201从源代码输入部1101接受源代码信息1001，转换为实现模型1205。实现模型1205的形式由其元模型即元实现模型1002定义。实现模型1205为了最大限度得到本发明的效果，优选具有与源代码信息1001相互转换时所需的充分的信息，但根据某个方式，也可以在不脱离输出检查代码的目的的程度上省略或追加信息。

在某个实施方式中，模型构建部1201也可以用与源代码输入部1101不可分的方式实现，以不产生源代码信息1001的方式进行处理。

实现-泛化模型转换部1202使用实现-泛化转换规则1005、元实现模型1002、元泛化模型1003将实现模型1205转换为泛化模型1206。泛化模型具有能够表现多个编程语言中的结构和处理的数据结构。例如，泛化模型中，对于源代码0001中的If语句和Switch语句不加区别地作为选择执行语句表现。在某个实施方式中，将实现模型1205转换为泛化模型1206时，也可以仅使用实现-泛化转换规则1005。此外，在某个实施方式中，实现-泛化转换规则1005包括多个转换规则的情况下，也可以是综合多个转换规则作为1个转换规则，用于从实现模型1205到泛化模型1206转换的方法。此外，在某个实施方式中，实现-泛化转换规则1005包括多个转换规则的情况下，也可以是通过多次反复转换处理而进行从实现模型1205到泛化模型1206的转换的流程。

抽象化模型转换部1203使用抽象化转换规则1006、元泛化模型1003，进行泛化模型1206的抽象化。作为抽象化的例子，有对于选择语句中的条件式用恒真、或恒伪、或非确定的选择进行置换的方法。在某个实施方式中，对泛化模型1206进行抽象化时，也可以仅使用抽象化转换规则1006。此外，在某个实施方式中，在抽象化转换规则1006包括多个转换规则的情况下，也可以是综合多个转换规则作为1个转换规则用于泛化模型1206的抽象化的方法。此外，某个实施方式中，抽象化转换规则1006包括多个转换规则的情况下，也可以是通过多次反复转换处理而进行泛化模型1206的转换的流程。

非功能约束附加处理部1204对于抽象化后的泛化模型1206的各组件（功能）附加基于非功能规则0005的非功能的约束，生成泛化模型1207。

泛化-检查模型转换部1209使用泛化-检查转换规则1007、元泛化模型1003、元检查模型1004，将附加有非功能约束的泛化模型1207转换为检查模型1008。例如，检查代码是Promela形式的情况下，泛化模型中作为选择执行语句表现的元素，在检查模型中表现为If语句。在某个实施方式中，将泛化模型1206转换为检查模型1008时，也可以仅使用泛化-检查转换规则1007。此外，在某个实施方式中，泛化-检查转换规则1007包括多个转换规则的情况下，也可以是综合多个转换规则作为1个转换规则用于从泛化模型1206到检查模型1008的转换的方法。此外，在某个实施方式中，泛化-检查转换规则1007包括多个转换规则的情况下，也可以是通过多次反复转换处理而进行从泛化模型1206到检查模型1008的转换的流程。

输出部1300使用从转换处理部1200供给的转换结果的信息，输出非功能检查代码0006。在某个实施方式中，输出检查代码时，例如也可以从存储部供给模型检查器的描述语言的语法信息等信息。

检查代码输出部1301使用元检查模型1004、从存储部1400的书写规则数据库1403取得的检查代码书写规则1009，将检查模型1008转换为非功能检查代码0006。例如，用非专利文献5中记载的方法，描述检查代码书写规则1009，进行从检查模型1008向非功能检查代码0006的转换。在某个实施例中，也可以不限于此，而是将检查模型1008向用于检查的模型检查器的描述形式转换的任意方法。非功能检查代码0006例如在使用SPIN作为模型检查器的情况下，用SPIN的输入语言即Promela描述。

存储部1400中，转换规则数据库1401、元模型数据库1402、书写规则数据库1403、非功能规则数据库1404分别用例如关系数据库或层次型数据库等的在计算机上实现的任意的数据保存方式实现。转换规则数据库1401、元模型数据库1402、书写规则数据库1403、非功能规则数据库1404不需要用相互相同的方式实现，也可以用相互不同的方式实现。此外，检查规则数据库1401、元模型数据库1402、书写规则数据库1403、非功能规则数据库1404各自不需要用单一的方式实现，例如也可以将要保有的信息的一部分保存在关系数据库中，将要保有的信息的一部分组合在实现发明的计算机程序中等，分别用不同的方式的组合实现。

存储部1400供给输入部1100、转换处理部1200、输出部1300进行各自的处理所需的信息。例如，存储部1400存储与转换规则相关的信息、与元模型相关的信息、与模型检查器的描述语言的语法相关的信息。

转换规则数据库1401，如上所述，将转换规则与元数据一同保有。上述元数据用于选择转换规则，可以是具有实现-泛化转换规则1005、抽象化转换规则1006、泛化-检查转换规则1007的各不相同的信息的方法。实现-泛化转换规则1005的元数据，例如可以是转换源代码的描述语言的种类。抽象化转换规则1006的元数据，例如可以是为了容易理解抽象化的简明表达的名称、简单的说明、“数据的抽象化”“处理的抽象化”等抽象化的种类、用自然语言或字母或数值表现的抽象化引起的状态数量削减效果、用自然语言或字母或数值表现的抽象化对性质的影响、抽象化能够适用的软件的域。泛化-检查转换规则1007的元数据，例如可以是指示用于检查的模型检查器的名称。

以下参照图5至图6说明输入部1100、转换处理部1200、输出部1300、存储部1400、控制部1500的详情。

首先，参照图5说明本实施例中的源代码转换流程的一例。图5是表示第一实施例的处理流程的例子的图。本实施例中的源代码转换流程包括：源代码输入步骤S101、转换规则输入步骤S102、转换规则应用步骤S103、检查代码输出步骤S104、系统约束条件的输入步骤S105、判定步骤S106、和修正步骤S107。

首先，在源代码输入步骤S101中，通过源代码输入部1101对源代码转换装置1000读取源代码0001，转换为源代码信息1001。

源代码输入部1101受理由用户输入的检查对象的源代码0001，转换为源代码信息1001。源代码0001例如用JIS X3010-1993中公开的C编程语言描述。源代码信息1001，具体而言，例如用抽象语法树的形式保存。源代码信息1001的形式不限于抽象语法树，也可以是保存结构和逻辑等源代码0001的检查所需的信息的任意形式。

继源代码输入步骤S101之后，在转换规则输入步骤S102中，通过转换规则输入部1102对源代码转换装置1000读取以细粒度分割的多个转换规则即转换规则集合0002。在该转换规则输入步骤S102中，定义转换前的模型元素与转换后的模型元素的对应关系、和通过转换对转换前的模型元素施加的操作的一方或双方。对源代码转换装置1000读取转换规则集合0002的处理，也可以不需要通过用户的一次操作进行，而通过反复操作进行。此外，源代码输入步骤S101和转换规则输入步骤S102不一定要按该顺序完成，只要在通过源代码输入部1101生成源代码信息1001之前输入源代码0001，并且在转换规则输入部1102为了转换规则输入处理而要求源代码信息1001之前输入源代码0001即可，从而，也可以以源代码输入步骤S101的处理和转换规则输入步骤S102的处理混合存在的顺序进行处理。例如，也可以是源代码输入部1102受理源代码0001，接着转换规则输入部受理转换规则集合0002，接着源代码输入部1102将源代码0001转换为源代码信息1001的流程。

转换规则输入部1102受理由用户输入的转换规则集合0002。从用户处受理转换规则集合0002的方法，例如可以是以下所示的方法。

第一个转换规则输入方法的例子是，转换规则输入部1102接受用户直接手动操作而输入的转换规则作为转换规则集合0002的一部分。

第二个转换规则输入方法的例子是，转换规则集合0002的至少一部分，也可以通过用户描述的转换规则（描述）进行输入。或者，输入部1100也可以从存储部1400取得转换规则的一览，以一览等的形式对用户提示转换规则，用户从上述一览中选择，由此受理转换规则集合0002的输入。即，用户在转换规则的输入之前，对输入部1100的转换规则输入部1102输入（描述）转换规则的检索条件，接着，转换规则输入部1102从存储部1400所具有的转换规则数据库1401取得符合上述检索条件的转换规则并作为转换规则一览对上述用户提示。接着，上述用户选择所提示的上述转换规则一览中包括的1个以上的转换规则。转换规则输入部1102将该由用户选择的1个以上的转换规则作为转换规则集合0002的一部分受理。

第三个转换规则输入方法的例子是，也可以首先由使用者在转换规则的输入之前，对转换规则输入部1102输入转换规则的检索条件，接着，转换规则输入部1102从转换规则数据库1401取得符合上述检索条件的转换规则，作为转换规则集合的一部分受理。

第四个转换规则输入方法的例子是，转换规则输入部1102从所输入的源代码0001中抽出、生成转换规则的检索条件，进而从转换规则数据库1401取得符合上述检索条件的转换规则，作为转换规则集合的一部分受理。

此外，第五个转换规则输入方法的例子是，转换规则输入部1102用某种方法对被输入的转换规则进行加工，由此受理转换规则。上述加工方法的例子，可以是在转换规则数据库1401中，以将源代码0001中的变量名等作为参数的状态保存转换规则，例如通过基于用户明确的输入的方法等，在源代码0001的信息代入参数，将其包含在转换规则集合中的方法。

继转换规则输入步骤S102之后，在转换规则应用步骤S103中，模型构建部1201将源代码信息1001转换为实现模型1205，接着，实现-泛化模型转换部1202将实现模型1205转换为泛化模型1206（S1031），接着，抽象化模型转换部1203对泛化模型1206进行抽象化（S1032）。接着，对抽象化后的泛化模型1206的各组件（功能）附加基于非功能规则0005的非功能约束，生成泛化模型1207（S1033），接着，泛化-检查模型转换部1209将泛化模型1207转换为检查模型1008（S1034）。转换规则输入步骤S102和转换规则应用步骤S103不一定要按该顺序完成处理，只要在实现-泛化模型转换部1202的处理前输入实现-泛化转换规则1005，并且在抽象化模型转换部1203的处理之前输入非功能规则0005和抽象化转换规则1006，并且在泛化-检查模型转换部的处理之前输入泛化-检查转换规则1007即可。

继转换规则应用步骤S103之后，在检查代码输出步骤S104中，通过检查代码书写部1301使检查模型1008作为非功能检查代码0006被书写。非功能检查代码0006的书写目标的指定不一定要在转换规则应用步骤S103之后，只要在非功能检查代码0006书写之前即可。例如，也可以是与源代码输入步骤S101并行地进行非功能检查代码0006的书写目标的指定的流程。

其中，也可以是继检查代码输出步骤S104之后，前进到转换规则输入步骤S102，由此对于已输入的源代码0001反复使用不同的转换规则集合0002进行转换的流程。此外，在某个实施例中，也可以继检查代码输出步骤S104之后，前进到转换规则输入步骤S102，将已输入的转换规则集合0002的全部或一部分与在转换规则输入步骤S102中新输入的转换规则集合0002一同用作转换规则集合0002。

非功能检查代码0006被输入到模型检查工具2000。对于该模型检查工具2000，在系统约束条件的输入步骤S105中被赋予系统约束条件0009（步骤S105的输入时间也可以在此之前）。然后，在步骤S106中，判定非功能检查代码0006是否满足系统约束条件0009。非功能检查代码0006不满足系统约束条件0009的情况下，在步骤S107中，操作者对源代码加以修正，以下反复同样的处理直到满足系统约束条件0009。

接着，用图6、图7详细说明转换处理部4111。图6是说明第一实施例的源代码转换装置的动作的图。图7是更加详细地说明第一实施例的源代码转换的流程的图。

在本实施方式中，转换处理部4111通过元模型、使用了转换规则的模型转换，将源代码信息1101转换为非功能检查模型1008。首先，模型构建部1201从源代码输入部1001受理源代码信息1001，转换为实现模型1205。实现-泛化模型转换部1202从转换规则数据库读取实现-泛化转换规则1005，从元模型数据库1读取元实现模型1002和元泛化模型1003，将实现模型1205转换为泛化模型1206。抽象化模型转换部1203从转换规则数据库读取抽象化转换规则1006，从元模型数据库读取元泛化模型1003，进行泛化模型1206的抽象化。非功能要件附加处理部1204从非功能规则数据库读取非功能要件1600，对泛化模型1206的对应的模型元素进行非功能要件的附加，进行带有非功能要件的泛化模型1207的生成。例如，非功能要件表现为模型元素和要件项目的表形式。

泛化-检查模型转换部1209从转换规则数据库读取泛化-检查转换规则1007，从元模型数据库读取元泛化模型1003和元检查模型1004，将带有非功能要件的泛化模型1207转换为检查模型1008。例如，非功能要件在处理中在模型检查工具是UPPAAL的情况下，将检查代码转换为时间自动机的形式。检查代码输出部1301使用元检查模型1004和从书写规则数据库取得的检查代码书写规则，将检查模型1008转换为非功能检查代码0006。例如，使用UPPAAL作为模型检查工具的情况下，由于能够直接输入模型，所以不进行转换处理地书写即可。

这样，本发明中，为了使用模型转换技术阶段性地进行转换，进行如下处理：

（1）将源代码0001转换为与其（大致）等效的“实现模型”1205

（2）将“实现模型”转换为用不依赖于特定编程语言的形式表现结构和逻辑等的程序信息的“泛化模型”

即，使用不同的多个第一转换规则1005-1～1005-n中的至少1个，将“实现模型”1205转换为不依赖于特定编程语言的形式即中间形式的“泛化模型”1206。图7的例子中，选择“‘If语句’→条件分支”、“‘switch语句’→条件分支”、“‘while语句’→‘循环’”、“‘for语句’→‘循环’”、“‘int语句’→‘整型’”、“‘float语句’→‘流型’”、“‘double语句’→‘流型’”这至少7个不同的转换规则作为第一转换规则。

（3）实施对“泛化模型”1206附加非功能约束的处理

即，用非功能规则，将中间形式的“泛化模型”1206转换为带有非功能约束的泛化模型1207。图7的例子中，选择“‘子程序’→t>60”、“‘循环’→t>50”、“‘条件分支’→t>30”、“‘四则运算’→t>10”这些不同的非功能规则作为时间约束（单位：秒）。此外，选择“‘整型’→4字节”、“‘流型’→8字节”这些不同的非功能规则作为容量约束。

（4）对于带有非功能约束的泛化模型1207，实施用于抽象化的转换

即，使用不同的多个第二转换规则1006-1～1006-n中的至少1个，对与上述中间形式的泛化模型进行抽象化处理。

图7的例子中，选择“数据读取→随机输入”、“数据的抽象化”这至少2个不同的转换规则作为第二转换规则。

（5）将泛化模型转换为“非功能检查模型”，生成（输出）代码

即，使用不同的多个第三转换规则1007-1～1007-n中的至少1个，从上述中间形式的泛化模型1207转换为具有非功能检查代码的生成所需的信息的非功能检查模型1008。图7的例子中，选择与第一转换规则对应的“‘条件分支’→‘if’语句”、“‘循环’→‘do’语句”这至少2个不同的转换规则作为第三转换规则。

此外，实现模型、泛化模型、检查模型分别由定义语法的“元模型”定义数据结构和语义。

这样，从实现模型转换到泛化模型时，例如，转换对象源代码的描述语言的语法包括“for语句”、“while语句”作为循环处理的描述方法时，用户使用以上所述的转换规则输入方法选择将“for语句”转换为“循环”的规则和将“while语句”转换为“循环”的规则作为第一转换规则。在泛化模型的抽象化的转换时，用户决定检查水平（抽象化的程度），作为达成所决定的检查水平的转换规则，例如用以上所述的转换规则输入方法，选择将与外部数据读取相关的命令和一系列处理转换为随机输入的规则、和将特定的数据类型转换为抽象度更高的类型的规则作为第二转换规则。进而，当从泛化模型向检查模型的转换时，例如在模型检查器的输入语言的语法具有“do语句”作为循环处理的描述方法时，用户使用以上所述的转换规则输入方法，选择将“循环”转换为“do语句”的规则作为第三转换规则。转换规则中，能够跨多个软件应用的通用性的规则等能够反复使用的规则被数据库化。数据库中保存的转换规则具有域信息和检查水平（抽象化对检查的影响）的信息，作为用作由用户进行检索和规则选择的判断材料的元信息。

此外，转换规则的选择方法有如下所述的方法。

（1）通用性规则：总是选择

（2）依赖于特定的程序库的规则：通过输入使用的程序库或检查对象的域（畴（category））而一并选择

（3）与抽象化对应的规则：用户从（输入要检查的性质、检查水平而得到的）转换规则一览中选择，或者用户自身进行描述输入，或者根据要检查的性质自动生成。

本发明中，按照转换规则从源代码生成检查模型时，对于抽象化后的软件的各组件（功能）描述与各执行环境对应的处理时间，由此能够对自动机赋予时间的概念。例如，如图8A的自动机所示，对于抽象化后的软件的各组件（功能）、即各状态（A）～（E），能够描述处理时间（PC）作为与各执行环境对应的约束。由此，用户与对象源代码和检查水平（抽象化的程度）相应地选择转换规则和非功能规则，由此能够转换为可检查的非功能检查代码，解决以用户选择的抽象化水平进行非功能验证的课题。

根据本发明，如图8B所示，能够实现与抽象度对应的功能要求和非功能要求的验证，并且能够仅通过变更转换规则对应各种执行环境。

即，通过模型的抽象化，能够削减状态数。但是，通过抽象化可能对模型的性质产生影响。例如，检测出的缺陷（反例）在原本的系统中不存在，不能够发现原本的系统中存在的缺陷等。另一方面，对性质不产生影响的健全的抽象化，存在状态数削减效果较小的倾向。

根据本发明，通过具有输入以细粒度分割的多个转换规则的接口，用户对抽象化的水平的变更和非功能约束的附加可以通过输入转换规则的操作容易地实现。即，用户能够通过输入接口选择多个细粒度的转换规则和非功能约束的附加。

源代码转换方法具有使用多个转换规则将检查对象的源代码转换为用模型检查器的输入语言描述的检查代码的流程，上述转换规则分类为实现-泛化转换规则、抽象化转换规则、泛化-检查转换规则，转换阶段性地进行。由此，追踪检查对象的源代码的设计变更时，仅对多个转换规则中的与变更相关的转换规则和非功能约束的附加进行变更即可，变更可以抑制在最小限度。此外，分别用元模型定义实现模型、泛化模型、检查模型，施加约束，由此能够验证使用转换规则的转换结果没有错误。由此，能够防止因为组合细粒度的转换规则和非功能规则实现将检查对象的源代码向检查代码在进行抽象化的同时进行转换的一系列处理而产生的、转换规则和非功能规则的验证成本的增大。

此外，通过具有输入以细粒度分割的多个转换规则的接口，用户对抽象化的水平的变更，可以通过与要检查的性质、检查水平相应地由用户选择、输入转换规则和非功能规则的操作容易地实现。由此，可以解决抽象化的水平的变更困难的课题，能够降低用模型检查工具的输入语言描述检查代码的成本。例如，存在仅在执行循环时发生的特定的错误的情况下，通过除去该循环，尽管不能够检测出特定的错误，但能够检测出该循环不包括在发生原因中的错误，能够大幅削减状态数。

进而，通过在数据库中保存模型的转换规则和非功能规则加以再利用，能够以低成本对应检查对象源代码的设计变更和对其他软件的应用。

作为本发明的系统（软件）的非功能验证的例子，列举与系统的时间约束相关的验证的例子，如下所述：

（1）确认DTV的频道切换在1秒以内切换。

（2）确认超分辨算法对于1个画面在1/120秒以内结束。

（3）确认用传感器检测到装置异常的情况下，在5秒以内通知用户。

实施例2

接着，用图9至图14说明本发明的第二实施例的源代码转换装置和转换处理方法。本实施例中，特征在于具有对于抽象化转换后的中间形式附加抽象化标志的步骤。即，是一种利用源代码转换装置进行的源代码转换方法，对源代码转换装置输入软件的源代码、不同的多个转换规则、不同的多个逆转换规则，用不同的多个转换规则将源代码转换为中间形式，进而用不同的多个转换规则将中间形式转换为抽象化中间形式。然后，对抽象化中间形式附加观测点。进而，用不同的多个逆转换规则将附加有观测点的抽象化中间形式转换为附加有观测点的中间形式，用不同的多个逆转换规则将该附加有观测点的中间形式转换为附加有观测点的源代码。

图9是表示第二实施例的包括源代码转换装置的源代码转换系统的结构例的图。本发明的实施方式中应用的源代码转换装置1000，是将检查对象的源代码0001转换为非功能检查代码0007、输出带计测源代码0008的装置，具有输入部1110、转换处理部1200、输出部1300、存储部1400、控制部1500。2000表示模型检查工具，4000表示实测装置。

图10是表示源代码转换装置1000的结构例的图。输入部1100具有源代码输入/修正部1101、转换规则输入部1102、非功能规则输入部1103。转换处理部1200具备模型构建部1201、实现-泛化模型转换部1202、抽象化模型转换部1203、非功能要件附加处理部1204、泛化-检查模型转换部1209、具体化模型转换部1210、泛化-实现模型转换部1211和代码生成部1212。输出部1300具有非功能检查代码输出部1301和带计测源代码输出部1302。存储部1400具有转换规则数据库1401、元模型数据库1402、输出规则数据库1403、非功能规则数据库1404和逆转换规则数据库1405。

源代码转换装置1000例如作为在1台计算机或者通过网络连接的多台计算机上进行工作的程序实施。源代码0001和转换规则集合0002，例如通过从计算机上的存储装置读取的方法、和利用与计算机连接的输入设备直接输入的方法等方法被输入。此外，非功能检查代码0007和带计测源代码0008，例如通过对计算机上的存储装置书写的方法、和在计算机的显示装置上显示的方法被输出。输入部1100受理由用户输入的数据即与源代码0001相关的信息、和与以细粒度分割的多个转换规则即“转换规则集合”0002相关的信息，对转换处理部1202供给。在某个实施方式中，输入部1100也可以受理与用户对转换处理部的驱动和控制、对输出部的驱动和控制相关的指示。

图11是表示本发明的第二实施例的源代码转换装置的处理流程的例子的图。转换处理部1200从输入部1100供给源代码0001的信息和要对源代码0001应用的转换规则集合0002的信息（图11的S101、S102），进行用转换规则集合0002对源代码0001加以转换的处理（S1031～S1034、S104～S107）和逆转换处理（S1035～S1038），将转换结果的信息和追加有与用户的抽象化水平相应的计测处理的带计测源代码0008供给到输出部1300（S108）。输出部1300使用从转换处理部1200供给的转换结果的信息，输出非功能检查代码0007。

以下参照图12～图14详细说明转换处理部1200的结构、功能。首先，图12是说明第二实施例的源代码转换装置的动作的图。图13是说明源代码-实现模型转换对应表（Table-A～C）的结构例和功能的图。

在本实施方式中，转换处理部1200通过使用元模型和转换规则的模型转换，将源代码信息0001转换为非功能检查模型1207，输出带计测源代码0008。模型构建部1201从源代码输入/修正部1201接受源代码信息，转换为实现模型1205，将其转换过程作为源代码-实现模型转换对应表（Table-A）登记在逆转换数据库1405中。在源代码-实现模型转换对应表（Table-A）中，例如像“if（）”→“if语句”、“switch”→“switch语句”、“while”→“while语句”这样记录。

实现-泛化模型转换部1202从转换规则数据库1401读取实现-泛化转换规则，从元模型数据库1402读取元实现模型和元泛化模型，将实现模型转换为泛化模型，将该转换过程作为实现-泛化模型转换对应表（Table-B）登记在逆转换数据库1405中。在源代码-实现模型转换对应表（Table-B）中，例如像位置10、“循环”→“while语句”Step10，位置20、“循环”→“while语句”Step15，位置30、“循环”→“for语句”Step30这样记录。

抽象化模型转换部1203从转换规则数据库1401读取抽象化转换规则，从元模型数据库1402读取元泛化模型，进行泛化模型的抽象化，将其转换过程作为抽象化转换对应表（Table-C）登记在逆转换数据库1405中。源代码-实现模型转换对应表（Table-C）中，例如像位置20、“随机输入”→位置50、“读取数据”这样记录。

非功能要件附加处理部1204从非功能规则数据库1404读取非功能要件，对泛化模型的对应模型元素进行非功能要件的附加，对泛化-检查模型转换部1209和具体化模型转换部1210输出。泛化-检查模型转换部1209从转换规则数据库读取泛化-检查转换规则，从元模型数据库读取元泛化模型和元检查模型，将泛化模型转换为检查模型。具体化模型转换部1210从逆转换规则数据库1405取得抽象化转换对应表（Table-C），按照对应表进行抽象化后的泛化模型的具体化。泛化-实现模型转换部1211从逆转换规则数据库1405取得实现-泛化模型转换对应表（Table-B），按照对应表将泛化模型逆转换为实现模型。代码生成部1212从逆转换规则数据库1405取得源代码-实现模型转换对应表（Table-A），按照对应表将实现模型转换为带计测源代码0008，向源代码输出部1302输出。检查代码输出部使用元检查模型和从存储部1400的书写规则数据库1403取得的检查代码书写规则，将检查模型转换为非功能检查代码0007。例如，使用UPPAAL作为模型检查工具的情况下，能够直接输入模型，所以不进行转换处理地书写即可。源代码输出部中，将所输入的带测定源代码输出到系统外部。例如，保存到外部存储介质，或者在显示器上显示。

接着，图14是说明源代码转换的流程的图。根据本发明的使用非功能规则、例如时间转换规则的自动生成技术，（1）使抽象程序模型转换至要验证的抽象度，（2）对检查对象的抽象程序模型追加计测用的检查，（3）按照逆转换规则转换为源代码，在被计测检查的地方填入计测用的代码，生成带计测代码的源代码。进而，（4）使用实际环境计测执行时间，生成时间转换规则。（5）使用上述生成的时间转换规则生成非功能检查用代码0007。其中，如图12、图13中所说明，也可以在附加时间转换规则之后生成带有计测代码的源代码。

由此，能够在实际的软件的源代码中自动插入与用户对抽象化水平的变更相应的观测用探针（probe），解决难以观测用户所选择的抽象化水平的非功能、例如执行处理时间的观测的课题。

即，根据本发明，用户对抽象化水平的变更，可以通过选择输入与检查对象的源代码对应的不同的多个转换规则而自动地实现。而且，能够与用户所选择的抽象化水平相应地，进行使软件的理论上的位置与实际位置1：1对应的实测数据的观测。