Formal Methods for Contracting

• Applicant: Professorin Dr.-Ing. Ina Schaefer
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems
• Term: from 2013 to 2020
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 206480214

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.

• DFG Programme: Research Units
• Subproject of: FOR 1800: Controlling Concurrent Change (CCC)
• International Connection: France
• Cooperation Partner: Sophie Quinton, Ph.D.