用于一种嵌入式系统的代码变换器的检验方法

摘要

本发明涉及一种准备嵌入式系统(7)用的、从源代码到被变换代码的变换器的检验方法。该方法至少包含以下步骤：确定将这二个代码(1，3)进行因式分解的唯一的虚拟机，对每个所述源代码(1)和被变换代码(3)，确定多个表示载所述源代码(1)和被变换代码(3)之间的剩余差值的所述辅助函数，以及一个在于检验这些辅助函数之间的对应特性的步骤，该代码变换器(2)的检验从最后步骤开始被获取。该应用尤其适合于芯片卡(7)。

主权项

1.检验供嵌入式系统用的、从所谓源代码到被变换代码的代码变换器的方法，其中所述源代码和被变换代码与虚拟机相关联，该方法的特征在于它至少包含以下若干步骤：-对于所述源代码(1)和被变换代码(3)中的每一个，确定一个第一公用子集(13)，该子集构成影响这二个代码(1，3)的行为的单个虚拟机；-对于每个所述源代码(1)和被变换代码(3)，确定一个第二子集(10，30)，该子集由多个被所述单个虚拟机使用的所谓辅助函数(10i-30i)构成，所述辅助函数(10i-30i)表示在所述源代码(1)和被变换代码(3)之间的剩余差；-将辅助函数成对地关联起来，每一个对中的第一辅助函数(10i)属于与所述源代码(1)相关联的所述第二子集(10)，且每一个对中的第二辅助函数(30i)属于与所述被变换代码(3)相关联的所述第二子集(30)；-对所有所述对的辅助函数(10i-30i)之间的一个给定的对应特性进行检验；以及-验证由所述变换器(2)进行的从源代码(1)到被变换代码(3)的变换遵守所述给定的对应特性。