SHF: Medium: Contract-Based Black-Box Assurance

交通、医疗、航空和太空探索等不同领域的系统越来越依赖于带有嵌入式软件的第三方组件。由于缺乏对组件实现和设计的可见性，用于验证组件是否如广告所示的传统技术是不可行的；需要新的替代方案。这项研究通过开发和评估(1)发现和捕获组件必须满足的约定(应该做的和不应该的)的技术，以及(2)可用于指导和评估组件测试的彻底性的严格的度量驱动的标准来解决这类“黑盒”组件的保证。中心假设是：(1)新的测试覆盖充分性标准可以在组件的契约及其目标代码上定义；当满足时将确保关键系统所需的置信度级别的标准，以及(2)对象代码符号执行技术可以被开发用于组件行为的自动发现以及用于验证合同的一致性。这项研究的预期进展是：(A)适用于基于合同的测试的新的合同定义和发现技术，(B)合同和软件目标代码的覆盖标准，(C)增强的目标代码符号执行技术，以及(D)对该方法在现实系统上的经验评估。这项工作的预期更广泛的影响是：(A)所进行的经验研究的观察结果为管理机构和标准组织的努力提供了指导；(B)商业工具供应商在其软件开发工具中采用这些技术，从而有助于降低测试关键系统的非常高的成本；(C)由这些新技术实现的昂贵的人工测试过程的广泛自动化提供了正式指定和模拟要求的强大动力，从而极大地提高了软件开发项目各方面的质量；以及(D)开放获取工具、案例、实验基础设施、数据和开发的课程材料，促进了软件工程研究、教育和工业实践的发展。

Systems in diverse domains such as transportation, medicine, aviation and space exploration, increasingly rely on third-party components with embedded software. Due to the lack of visibility into the components' implementation and design, traditional techniques for verifying that the components perform as advertised are not feasible; novel alternatives are needed. This research addresses the assurance of such "black-box" components by developing and evaluating (1) techniques to discover and capture contracts - the do's and the don'ts - that the component must satisfy to operate safely in its intended environment, and (2) rigorous metric-driven criteria that can be used to guide as well as to assess the thoroughness of the component testing.The central hypotheses are that (1) novel test coverage adequacy criteria can be defined over the component's contracts as well as its object code; criteria that when satisfied will ensure the level of confidence needed for a critical system, and (2) object-code symbolic execution techniques can be developed for both automatic discovery of component behaviors as well as for verifying conformance to contracts. The expected advances from this research are: (a) new contract definition and discovery techniques suitable for contract-based testing, (b) coverage criteria for contracts and object-code of software, (c) enhanced object-code symbolic execution techniques, and (d) empirical evaluation of the approach on realistic systems. The anticipated broader impacts of this work are that: (a) observations from the empirical studies conducted provide guidance for regulatory agencies and standards organizations in their efforts; (b) commercial tool vendors adopt these techniques in their software development tools and thus help reduce the very high costs of testing critical systems; (c) extensive automation of the costly manual testing processes enabled by these new techniques provide a powerful incentive to formally specify and model requirements, thereby greatly improving quality in all aspects of software development projects; and (d) open-access to tools, case examples, experimental infrastructure, data, and curricular materials developed, advances the state of software engineering research, education and industrial practice.