Specification, verification and enforcement of interface contracts with data

“接口契约”是一个正式的定义，它定义了什么构成了一个特定系统的有效交互。例如，运行Facebook等应用程序的Web浏览器向Facebook服务器发送命令，并处理其响应以更新其显示。类似于两个人之间的真实世界契约，接口契约明确定义了浏览器和服务器如何相互匡威：可以发送哪些命令，期望哪些响应，甚至可以将哪些值放入各种命令中。任何一方不遵守合同都可能导致另一方陷入意想不到的状态。同样，未来火星漫游者的航天器系统测试涉及数千条命令和响应的执行。然后搜索这些事件序列，以发现是否违反了暗示组件故障的“合同”。 虽然没有明确地这样称呼，但接口契约存在于各种软件系统中。然而，很少有工具可供开发人员和用户使用，以确保通信“对等体”之间的合同遵守。拟议的研究计划集中在软件工程的形式化方法的应用。特别是，它旨在通过使用数学逻辑对系统生成的有效事件序列进行建模，验证和执行。对这些问题的实际解决方案在广泛的领域中具有直接应用的潜力。在术语中，跟踪验证和监控的综合分析，考虑到接口合同中的顺序和数据依赖性，可以产生有用的开发，调试和测试工具，并提高软件系统的安全性和可靠性。

An "interface contract" is a formal definition of what constitutes a valid interaction with a particular system over time. For example, a web browser running an application such as Facebook sends commands to the Facebook server and processes its responses to update its display. Similar to a real-world contract between two people, the interface contract clearly defines how the browser and the server are expected to converse with each other: which commands can be sent, what responses are expected, and even what values can be put into the various commands. Not following the contract by either side can result in the other side being thrown into an unexpected state. Similarly, the testing of spacecraft systems for the future Martian rovers involves the execution of thousands of commands and responses. These sequences of events are then searched for violations of a "contract" that hints at component malfunction. Although not explicitly called as such, interface contracts are present in a wide variety of software systems. However, very little tools are available for developers and users to ensure contract compliance between communicating "peers". The proposed research program concentrates on the application of formal methods to software engineering. In particular, it aims to model, verify and enforce valid sequences of events generated by systems through the use of mathematical logic. Practical solutions to these problems present a potential of direct application in a wide range of domains. In term, a comprehensive analysis of trace validation and monitoring, taking into account sequential and data dependencies in interface contracts, could produce useful development, debugging and testing tools, and improve the safety and reliability of software systems.