Formal Methods for Contracting

引入标准化的硬件抽象层和应用程序开发的运行时环境（例如用于汽车的AUTOSAR）允许创建灵活的软件基础设施。设备之间的通信和节点作为动态资源的利用（即使它们并不总是可用）进一步扩展了当前和未来应用程序的灵活性。互联性和通信也意味着嵌入式系统不一定要由一个中央实例控制，而是由几个不同的设备控制。由于应用程序、运行时环境（操作系统）和平台是独立开发的，因此出现了对方法的需求，该方法允许在部署之后继续进行很大程度上独立的开发。在CCC研究小组的背景下，B2项目将开发一种合同形式和相应的方法，允许在运行时修改和集成系统的组件。这种形式将能够适应开放网络、动态变化的平台以及分布式、去中心化的控制，这需要应用程序、运行时环境和平台之间灵活的契约接口。此外，我们需要一个合同谈判机制，用于添加和更改正式可验证的合同。对于合同谈判，我们也不能忽视优化。由于嵌入式系统上的资源是稀缺的，限制它们的使用是很重要的。因此，在可能的情况下，必须重用先前谈判阶段的现有结果。我们将研究哪些观点是合理的，以及如何实现增量谈判。特别是通过传感器将不确定性引入到嵌入式系统的计算中。我们将分析不确定性如何影响合同谈判。因此，详细地说，项目B2将处理(1)开发一个支持多个观点（安全性、安全性、可用性、功能正确性）的合同形式，同时仍然考虑应用程序需求和平台属性；(2)建立一个完整的合同机制，对每个观点(3)进行不同的分析，不仅要考虑需求，还要考虑系统参数的优化；(4)开发组合式和增量式方法，提高合同机制的效率。

The introduction of standardized hardware-abstraction layers and runtime environments for application development (e.g. AUTOSAR for automotive) allows to create flexible software infrastructures. Communications between devices and the utilization of nodes as dynamic resources, even when they are not always available, further extend the flexibility of current and future applications. Interconnectedness and communications also mean that the embedded system does not necessarily has to be controlled by a central instance, but by several different devices. Because applications, runtime environment (operation system), and platform are developed independently, a demand for a methodology arises, wich allows to continue the largely independent development after the deployment. In the context of the CCC research group the B2 project will develop a contract formalism and corresponding methods allowing to modify and integrate components of a system at runtime. The formalism will be able to adapt to open networks, dynamically changing platforms, and distributed, decentralized control, which requires flexible contract interfaces between applications, runtime environment and platform. Additionally, we need a contract-negotiation mechanism for adding and changing contracts which is formally verifiable. For the contract negotiation we also cannot neglect optimization. As resources on embedded systems are scarce, it is important to limit the usage of them. Therefore existing results of previous negotiation phases have to be reused where possible. We will examine for which viewpoints an incremental negotiation in reasonable and how it can be realized. Especially through sensors uncertainty is introduced into calculations in embedded systems. We will analyze how uncertainty affects the contract negotiation. So in detail, project B2 will deal with (1) the development of a contract formalism supporting several viewpoints (safety, security, availability, functional correctness), while still considering the applications requirements and platform properties; (2) the development of a complete contract mechanism with different analysis for every viewpoint (3), not just under consideration of requirements, but also taking optimization of system parameters into account; (4) the development of compositional and incremental methods to improve the efficiency of the contract mechanism.