Temporal HAL-API Dependencies (THADs) can be useful to capture an interesting class of correctness properties in embedded software development. They demand a moderate effort for specification (which can be done via program annotations) and verification (which can be done automatically via software model checking). In this sense, they have the potential to form an interesting sweet spot between generic properties (that demand virtually no specification effort, and that are typically addressed by static analysis) and application-specific properties as addressed by full-fledged formal methods. Thus, they may form a gateway to wider and more economic use of formal methods in industrial embedded software development.
翻译：时序HAL-API依赖（THADs）可用于捕捉嵌入式软件开发中一类重要的正确性属性。其规约（可通过程序注解实现）与验证（可通过软件模型检查自动完成）所需工作量适中。在此意义上，THADs有望在通用属性（几乎无需规约工作，通常通过静态分析处理）与完整形式化方法处理的应用特定属性之间，形成一个具有潜力的平衡点。因此，它们可能成为在工业嵌入式软件开发中更广泛、更经济地应用形式化方法的切入点。
相关内容
微信扫码咨询专知VIP会员