Interface reasoning for interacting systems (IRIS).

社会的平稳运行不仅取决于程序的正确性，特别是控制单个系统的关键和高灵敏度核心组件的程序的正确性，而且还取决于大型，复杂，动态，高度分布式系统的不同信息处理生态系统之间的正确和强大的交互。故障是常见的、不可预测的、高度破坏性的，并且跨越多个组织。在未来几年中，系统相互依赖的规模将以数量级的方式增加。事实上，到2020年，随着云计算、物联网和大数据的发展，我们可能会面临一个拥有2500万个应用程序、310亿个连接设备、1.3万亿个标签/传感器和50万亿GB数据存储的世界（数据：IDC，ICT Outlook：Recovery Into a New World，#DR2010_GS2_JG，2010年3月）。系统之间的强有力的交互对每个人和社会的每个方面都至关重要。虽然在这个世界上完整系统的正确性和安全性无法验证，我们可以希望能够确保特定的系统，如验证的安全，安全，或身份关键模块，正确的接口。尽管最近的成功程序验证，仍然有很少的前景验证这样的生态系统在他们的整体：其规模和复杂性实在太大，社会和管理协调方面的挑战也是如此。甚至能够定义什么是验证在更大的系统中将具有不确定作用的东西也是一个严峻的挑战。很明显，这些信息处理生态系统运行的最关键方面在于它们的交互：即使是完美指定和实现的单个系统也可能被用在它们不想要的环境中，导致它们之间不可靠、不安全的通信。因此，我们认为支持这种交互的接口是确保系统按预期运行的关键机制。然而，验证/建模技术在确保程序、协议和策略（以及驱动大型系统的软件）的低级别功能的可靠性方面非常有效，基本上不适用于对此类大型系统及其接口的推理。我们打算通过研究在系统生态系统中指定和验证接口的技术，组织和社会挑战来探索这一缺陷。在此过程中，我们将推动验证技术的使用，提高大型系统的可靠性。复杂系统生态系统及其接口是当今存在的最复杂和最关键的信息生态系统之一，具有高度动态性，并不断发展。我们的目标是了解构成这些生态系统的组件之间的接口是如何工作的，并根据其预期用途对其进行验证。这项研究将通过一系列不同的主题进行，涵盖接口至关重要的系统主题，包括关键代码，通信和安全协议，分布式系统和网络，安全策略，业务生态系统，甚至扩展到建筑物和网络的物理架构。这些主题代表了在不同的抽象和关键层次上对接口的正确性进行指定和推理的问题。每个抽象和关键程度的接口都可以独立地进行研究，但我们相信，有可能发展出一个相当普遍的、统一的关于接口的指定和推理的解释。任何一个抽象层次都不可能给出所有的答案：我们期望主题的工作将以复杂的方式发展和相互作用。

The smooth functioning of society is critically dependent not only on the correctness of programs, particularly of programs controlling critical and high-sensitivity core components of individual systems, but also upon correct and robust interaction between diverse information-processing ecosystems of large, complex, dynamic, highly distributed systems. Failures are common, unpredictable, highly disruptive, and span multiple organizations.The scale of systems' interdependence will increase by orders of magnitude in the next few years. Indeed by 2020, with developments in Cloud, the Internet of Things, and Big Data, we may be faced with a world of 25 million apps, 31 billion connected devices, 1.3 trillion tags/sensors, and a data store of 50 trillion gigabytes (data: IDC, ICT Outlook: Recovering Into a New World, #DR2010_GS2_JG, March 2010). Robust interaction between systems will be critical to everyone andevery aspect of society. Although the correctness and security of complete systems in this world cannot be verified, we can hope to be able to ensure that specific systems, such as verified safety-, security-, or identity-critical modules, are correctly interfaced.The recent success of program verification notwithstanding, there remains little prospect of verifying such ecosystems in their entireties: the scale and complexity are just too great, as are the social and managerial coordination challenges. Even being able to define what it means to verify something that is going to have an undetermined role in a larger system presents a serious challenge. It is perhaps evident that the most critical aspect of the operation of theseinformation-processing ecosystems lies in their interaction: even perfectly specified and implemented individual systems may be used in contexts for which they were not intended, leading to unreliable, insecure communications between them.We contend that interfaces supporting such interactions are therefore the critical mechanism for ensuring systems behave as intended. However, the verification/modelling techniques that have been so effective in ensuring reliability of low-level features of programs, protocols, and policies (and so the of the software that drives large systems) are, essentially, not applied to reasoning about such large-scale systems and their interfaces. We intend to explore this deficiency by researchingthe technical, organizational, and social challenges of specifying and verifying interfaces in system ecosystems. In so doing, we will drive the use of verification techniques and improve the reliability of large systems.Complex systems ecosystems and their interfaces are some of the most intricate and critical information ecosystems in existence today, and are highly dynamic and constantly evolving. We aim to understand how the interfaces between the components constituting these ecosystems work, and to verify them against their intended use. This research will beundertaken through a collection of different themes covering systems topics where interface is crucially important, including critical code, communications and security protocols, distributed systems and networks, security policies, business ecosystems, and even extending to the physical architecture of buildings and networks. These themes are representative of the problem of specifying and reasoning about the correctness of interfaces at different levels of abstraction and criticality.Interfaces of each degree of abstraction and criticality can be studied independently, but we believe that it will be possible to develop a quite general, uniform account of specifying and reasoning about them. It is unlikely that any one level of abstraction will suggest all of the answers: we expect that the work of the themes will evolve and interactin complex ways.