摘要:描述:在先前的许多项目中并未发现性能异常的证据的情况下,才使用一个翻译器,除非存在正确运行的一些其他保证(例如:参看C.4.4.1),应避免使用没有运行经验或者带有任何已知的严重故障的翻译器。
C.4.4 工具和翻译器:通过使用提高置信度
注:在GB/T20438.3一2017的表A.3中引用了本技术/措施。
目的:为了避免在开发、验证和维护一个软件包的过程中出现的翻译器失效引起的任何困难。
描述:在先前的许多项目中并未发现性能异常的证据的情况下,才使用一个翻译器,除非存在正确运行的一些其他保证(例如:参看C.4.4.1),应避免使用没有运行经验或者带有任何已知的严重故障的翻译器。
在一个与安全相关的项目过程中,当翻译器存在微小缺陷时,记录下有关的语言结构并应小心避免使用这些结构。
使用本措施的另一种方案是把语言的使用只限在常用的特征。
这些建议是根据许多项目的经验提出来的。不成熟的翻译器已显示出它对于任何软件开发都是一个严重的障碍。它们使得开发一个安全软件成为不可能。
事实上,目前不存在证明所有工具或者翻译器都正确的方法。
C.4.4.1 源程序和执行代码的比较
目的:为了检验用来产生一幅PROM(可编程只读存储器)映像的工具未向产生的映像中引入任何错误。
描述:为了得到成分“对象”模块逆向设计PROM映像。把这些“对象”模块逆向设计成汇编语言文件。使用适当的技术,把这些逆向生成的汇编语言文件同最初用来产生PROM的实际源文件进行比较。
本技术的主要优点是,用于产生PROM映像的工具(编译器、连接器等)不必针对所有程序进行确认。本技术可验证用于特定安全相关系统的源文件的转换的正确性。
参考文献:
Demonstrating Equivalence of Source Code and PROM Contents.D.J.Pavey and L.A,Winsborrow, The Computer Journal Vol.36,No.7,1993
Formal demonstration of equivalence of source code and PROM contents;an industrial example.D. J.Pavey and I..A. Winsborrow, Mathematics of Dependable Systems,Ed.C. Mitchell and V.Stavridou, Clarendon Press,1995,ISBN 0-198534-91-4
Assuring Correctness in a Safety Critical Software Application.L. A. Winsborrow and D.J.Pavey. High Integrity Systems,Vol,1,No.5,pp453-459,1996
来源:科技新武器