ITR/SY: Modular Interface Violation Checking Using Formally-Specified Contracts

摘要建议#0113181 SitaramanClemson大学软件工程的一个基本目标是通过组装组件来实现软件系统的可预测和模块化构建。任何基于组件的方法都是在参与组件相互尊重合同的基本前提下工作的。如果违反这一前提，后果可能既危险又代价高昂，因为问题可能要到整合时间才会浮出水面。更糟糕的是，系统可能会在测试用例上正常运行，尽管违反了内部接口约定。内部违规导致的未检测到的故障最终可能只会在部署后显示为基于组件的系统和嵌入式系统的事故。该项目提供了一种模块化方法来检测和隔离内部合同违规。该方法允许使用形式规范在适当的抽象级别进行检查。它允许有选择地“打开”或“关闭”检查，以促进有效的回归测试，并且除了针对参数化和面向对象组件的功能外，它还解决了违反性能契约的问题。为了尽量减少违规检查过程中的错误，该项目将使用并实验评估自动化、正式验证、模型检查和测试技术的替代组合。

AbstractProposal #0113181SitaramanClemson UniversityA fundamental goal of software engineering is to enable predictable and modular construction of software systems by assembling components. Any component-based approach works on the basic premise that participating components respect each other's contracts. If this premise is violated, the consequences can be both dangerous and expensive, because the problems may not surface until integration time. Even worse, a system may behave properly on test cases, though internal interface contracts are violated. Undetected failures from internal violations may be revealed ultimately only as accidents to component-based and embedded systems after deployment.This project offers a modular approach for detecting and isolating internal contractual violations. The approach allows checking at suitable levels of abstraction using formal specifications. It permits checking to be turned "on" or "off" selectively to facilitate effective regression testing, and it addresses violations of performance contracts in addition to functionality for parameterized and object-oriented components. To minimize errors in the violation checking process, the project will use and experimentally evaluate alternative combinations of automation, formal verification, model checking, and testing techniques.