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.