TY - A2的主席,Autilia盟——Shaukat n . AU -本s . AU - Srinivasan s . k . AU - Jabeen s . PY - 2020 DA - 2020/07/14 TI -提高效率的目标代码验证使用静态抽象对象代码SP - 6791891六世- 2020 AB -的主要挑战之一的形式验证嵌入式系统软件的复杂性和显著大尺寸实现。当嵌入式系统是一个执行复杂算法的复杂医疗设备时，这个问题就变得至关重要。在基于改进的验证中，规范和实现都表示为转换系统。在细化映射的帮助下，实现转换系统的每个行为都与规范转换系统匹配。细化映射只能从实现中投影那些负责标记系统当前状态的值。当细化映射应用于对象代码级别时，大量指令将映射到规范转换系统中称为结巴指令的单个状态。我们使用静态口吃抽象(SSA)的概念，它过滤常见的口吃指令的多个段，并用合并替换每个段。SSA算法减少了嵌入式软件的实现状态空间，从而减少了WEB优化中手工验证所涉及的工作量。该算法已正式证明其正确性。在起搏器目标代码上实现SSA，以评估抽象代码在验证过程中的有效性。 The results helped to establish the fact that, despite code size reduction, the bugs and errors can still be found. We implemented the SSA technique on two different platforms and it has been proven to be consistent in decreasing the code size significantly and hence the complexity of the implementation transition system. The results illustrate that there is considerable reduction in time and effort required for the verification of a complex software control, i.e., pacemaker when statically stuttering abstracted code is employed. SN - 1058-9244 UR - https://doi.org/10.1155/2020/6791891 DO - 10.1155/2020/6791891 JF - Scientific Programming PB - Hindawi KW - ER -