Rafik Henia

Alain Girault

Christophe Prévot

Sophie Quinton

Laurent Rioux

Quantifying the Flexibility of Real-Time Systems

INTRODUCTION

The life cycle of many safety or mission critical real-time systems, such as avionic systems, satellites or software defined radios, is superior to 10 years whereas the supporting ICT technologies have a much faster evolution rate. This mismatch between system life cycle on one side and software life cycle on the other side is a challenge for performance engineers. It is therefore essential for commercial offers to allow technology evolutions and upgrades of the architecture and functions after the initial system deployment. Besides, this must be done while preserving the satisfaction of timing performance requirements over the entire system lifetime.

Our objective is to develop novel techniques to quantify the ability of a real-time system to cope with future software evolutions, while remaining schedulable. We propose to define the flexibility of a system as its ability to schedule a new software function and show how this concept can be used to anticipate at design time schedulability bottlenecks that may prove problematic, after deployment, for system evolution. In this paper we focus on an evolution scenario where a single task is added to an existing system running on a single-core processor. Our task model here is restricted to independent periodic tasks with implicit deadlines and the scheduling policy is static priority preemptive. Of course our goal is to generalize our approach to more complex systems.

The research area that is most closely related to our problem is sensitivity analysis [START_REF] Racu | Applying sensitivity analysis in real-time distributed systems[END_REF][START_REF] Bini | Sensitivity analysis for fixed-priority real-time systems[END_REF][START_REF] Dorin | Schedulability and sensitivity analysis of multiple criticality tasks with fixed-priorities[END_REF][START_REF] Punnekkat | Sensitivity analysis of real-time task sets[END_REF]. Sensitivity analysis is used [START_REF] Bate | Incorporating scenarios and heuristics to improve flexibility in real-time embedded systems[END_REF] to provide guarantees on the schedulability of a system in case of uncertainty on the system parameters, or [START_REF] Bini | Sensitivity analysis for fixed-priority real-time systems[END_REF] given a non schedulable system, to find a set of changes that lead to a schedulable system.

Most related work on sensitivity analysis addresses changes of one type of parameter, e.g., changes of task worst-case execution times (WCETs) or changes of periods -but not both. In [START_REF] Bini | Sensitivity analysis for fixed-priority real-time systems[END_REF] for example, the authors analyze the sensitivity of a system to changes in the arrival frequency of all tasks, or in the WCET of all tasks. In [START_REF] Punnekkat | Sensitivity analysis of real-time task sets[END_REF], the authors are interested in sensitivity analysis of systems with shared resources, for which they study the impact of an increase of the WCETs on system schedulability.

Dealing with different parameters (i.e. periods and priorities) is the approach used in [START_REF] Racu | Sensitivity analysis of complex embedded real-time systems[END_REF]. Here the authors define the sensitivity using evolutionary algorithms and a stochastic approach. It will be interesting to compare our results with this method.

In contrast with the above mentioned approaches, we do not allow parameters of the deployed system to be modified in according with industrial practice. But we need to handle at the same time changes in the period, priority and WCET of the task to be added. As a result, the set of possible system configurations that need to be checked is much smaller than in classical sensitivity analysis and we hope to be able to handle much more complex systems that what state-of-the-art sensitivity analysis can handle.

Other papers like [START_REF] Zhu | Optimizing extensibility in hard real-time distributed systems[END_REF][START_REF] Bate | Incorporating scenarios and heuristics to improve flexibility in real-time embedded systems[END_REF][START_REF] Davis | Robust priority assignment for fixed priority real-time systems[END_REF] deal with flexibility related to task allocation, priority assignment or scenario based optimization. In [START_REF] Davis | Robust priority assignment for fixed priority real-time systems[END_REF], the authors use concepts similar to ours to define an optimal or a robust priority assignment. In [START_REF] Zhu | Optimizing extensibility in hard real-time distributed systems[END_REF], the authors deal with task allocation and priority assignment to maximize the extensibility of each task chain, where extensibility is the maximum execution time it is possible to increase the WCET before missing the deadline. In [START_REF] Bate | Incorporating scenarios and heuristics to improve flexibility in real-time embedded systems[END_REF] the flexibility of a system is defined according to scenarios. To define the flexibility it is necessary to define possible scenarios of change.

Related work that deals with flexibility is used to define at design time what is the best task allocation or priority assignment. But most of the time in an industrial context, the designer cannot take into account only timing constraints and some functionalities have fixed parameters. Moreover we are interested in system evolution when most parameters of the system are already defined. It is at this point unclear if our problem (adding a task) can be precisely encoded into existing methods dealing with increased execution times.

As a summary, by restricting ourselves to a simple change scenario with industrial relevance, we hope to come up with an approach that can provide guidance for the evolution of complex systems, which cannot be covered by existing sensitivity analysis techniques. Finally, to the best of our knowledge, no existing work discusses the notion of limiting task, i.e. the task which will miss its deadline first. The final aim is to help the designer by giving him information to allow a system to evolve while respecting timing constraints.

SYSTEM MODEL

Unless otherwise specified all the parameters defined in the following have positive integer values. In particular, we assume a discrete time clock.

We consider a uni-processor real-time system S consisting of a finite set of n independent tasks scheduled according to the Static Priority Preemptive (SPP) scheduling policy. Each task τi, i ∈ [1, n], is defined by a tuple (πi, Ti, Ci) where πi is the priority, Ti the period, and Ci an upper-bound on the worst case execution time (WCET). Each task τi has an implicit deadline Di = Ti, meaning that a given activation of τi must finish before the next activation of τi.

We assume that different tasks have different priorities and use as convention that πi < πj means that τi has a higher priority than τj. For the purpose of our evolution scenario, we also suppose that for any two tasks τi and τj with πi < πj, it is always possible to define a new task τnew with πi < πnew < πj. This is done without loss of generality as priorities are only used to define a total order on tasks.

For each τi in S, hp(i) is the set of tasks of S that have a higher priority than τi, while lp(i) is the set of tasks of S that have a lower priority than τi.

The execution of a task τi is triggered periodically with period Ti and each activation of τi generates a new instance. A task instance is defined by its activation time, possible preemption delays, and finish time. Preemption delays are due to the task instance being blocked by higher priority task instances. Each instance of τi finishes at the latest after having being scheduled (i.e., not counting the preemption delays) for Ci units of time.

PROBLEM STATEMENT

We are interested in system evolutions that may happen after system delivery. We focus here on a simple evolution scenario where a new task τnew defined by (πnew, Tnew, Cnew) is added to a schedulable system S, thus yielding the system Snew = S ∪ {τnew}. From now on, τnew will denote the task (πnew, Tnew, Cnew) and Snew will denote the system S ∪ {τnew}.

We wish to answer the following question: Given a schedulable system S and a task τnew with unknown parameters: how can we quantify the flexibility of S, that is, its ability to accommodate τnew while remaining schedulable?

To address these issues, we start below by formalizing the notions of evolution and flexibility of a system. Definition 1. Evolution: An evolution of a system S is a task τnew where πnew belongs to [min i πi-1, max i πi+1]\{πi}i and (Tnew, Cnew) belongs to N + × N + , such that the CPU load after the evolution does not exceed 100%:

Cnew Tnew + i Ci Ti ≤ 1
Definition 2. Valid evolution: S being a schedulable system, an evolution τnew is valid for S if Snew is schedulable.

We denote by FS the set of all valid evolutions for system S. Note that if τnew is in FS, then for any 0 < C new < Cnew, the task (πnew, Tnew, C new ) is also in FS. Moreover for any T new > Tnew, the task (πnew, T new , Cnew) is also in FS. The flexibility of a system quantifies its ability to schedule a new task. We focus in this paper on the flexibility w.r.t. Cnew. The notion of flexibility w.r.t. Tnew is left for future work. Definition 3. Flexibility: Let S be a schedulable system. The flexibility of S is the partial function flex S from N + ×N + into N + such that (πnew, Tnew, flex S (πnew, Tnew)) is in FS and flex S (πnew, Tnew) is maximal.

The function flex returns, for all (πnew, Tnew), the value of the maximum WCET such that S ∪ {(π, T, flex S (π, T ))} is schedulable. This function is partial as such an WCET may not exist. In the rest of the paper, we first focus on methods for computing flex and then we will show how we can use it for system design.

SLACK ANALYSIS

Let us first briefly recall the standard analysis used to establish the schedulability of systems of independent periodic tasks on a single processor under the SPP policy [START_REF] Joseph | Finding response times in a real-time system[END_REF].

The response time of an instance of a task τi is the delay between its activation and its finish time. The worst case response time of τi (WCRT) is the maximum response time over all instances of τi; it is denoted ri. A system is schedulable if ri ≤ Ti for any task τi.

A critical instant of τi is an activation scenario that maximises the response time of τi. A task is said to be schedulable if and only if its WCRT is smaller than its (implicit) deadline: ri ≤ Ti. For the systems we consider, a critical instant of τi occurs whenever an activation of a task instance occurs simultaneously with the activation of all higher-priority tasks. The WCRT of τi can thus be obtained by computing:

ri = Ci + τ j ∈hp(i) ri Tj Cj (1)
To quantify the flexibility of a system, we start by introducing the slack of a task, which takes into account all the preemptions from higher priority tasks [START_REF] Davis | Scheduling slack time in fixed priority pre-emptive systems[END_REF]. Definition 4. The slack of a task τi is the maximum value it is possible to increase Ci while keeping τi schedulable.

The slack Sl i of a task τi can be computed using the algorithm presented in [START_REF] Davis | Scheduling slack time in fixed priority pre-emptive systems[END_REF].

Theorem 1. Let S be a schedulable system and τnew a task. Snew is schedulable if:

∀τi ∈ lp(new), Ti Tnew Cnew ≤ Sl i (2)
and rnew ≤ Tnew

Proof sketch of Theorem 1. We have to prove that, for each τi ∈ S ∪ {τnew}, we have ri ≤ Ti. Since S is schedulable, this holds for each τ h ∈ hp(new). For τnew itself, this holds directly by Eq. (3). And for each τ ∈ lp(new), the preemptions of the tasks in hp( ) are already taken into account in the slack Sl , hence there only remains to take into account the preemptions of τnew on τ , which is precisely the goal of Eq. ( 2). This gives a sufficient but non necessary condition because the slack Sli is a lower bound on the slack available for τi. The reason the criterion is not necessary is that the preemption delays induced by τnew may be overapproximated.

FLEXIBILITY ANALYSIS

Recall that the flexibility of a system is quantified through the function flex . We now show how to approximate flex using the above sufficient schedulability condition for Snew. Definition 5. For a given period Tnew and priority πnew of τnew, denote

• CS the largest WCET of τnew such that S is schedulable after evolving,

• Cτ new the largest WCET of τnew such that τnew is schedulable after evolving.

Theorem 2. S being a system and τnew an evolution, let C max S be the largest WCET allowed by Eq. (2) i.e. a lower bound of CS. Let C max τnew be the largest WCET allowed by Eq. (3) i.e. a lower bound of Cτ new . Then

C max Snew = min {C max S , C max τnew } is a lower bound of flex S (πnew, Tnew).
Proof sketch of Theorem 2. Theorem 1 gives a guarantee on the schedulability of Snew depending on τnew which is a sufficient non necessary condition. As a consequence, Theorem 2 based on Theorem 1 is also a sufficient and non necessary condition, i.e., a lower bound of the largest Cnew that guarantees the schedulability of Snew for fixed πnew and Tnew -which is given by flex S .

We can compute both C max S and C max τnew using Theorem 3. Theorem 3. Let S be a schedulable system and τnew a task. Then we have C max S and C max τnew :

C max S = min τ i ∈lp(new)     Sl i T i Tnew     (4)
and

C max τnew =     Tnew - τ j ∈hp(new) Tnew Tj Cj     (5)
Proof. Eq. ( 2) implies that, for all task τi in lp(new), we have Cnew ≤ Sli/ T i Tnew . Since Cnew must be in N + , it follows that Cnew ≤ min

τ i ∈lp(new)
Sli/ Ti Tnew hence Eq. ( 4). We found the largest Cnew by computing the largest Sl new . Again, since Cnew must be in N + , this leads to Eq. ( 5).

Intuitively, if τnew has high priority, then it will be easy to schedule but it will have a stronger impact on S. And this impact will be greater if the period Tnew is small. In contrast, a task τnew with a low priority will have a smaller impact on the other tasks and it will be harder to schedule with a small period.

Note that the function flex S is partial. Both Conditions ( 4) and ( 5) on the flexibility of τnew imply that some tuples (πnew, Tnew) lead to non schedulable systems. These tuples imply that at least one task in Snew will have not enough time to be executed. This is the case in a system if we add τnew with a high priority and a small period.

LIMITING TASK OF THE SYSTEM

We now focus on the fact that for a priority πnew and a period Tnew, C max S is limited by one, or possibly several tasks in lp(new). We call the lowest priority task among them the limiting task. Definition 6. The limiting task of S w.r.t. a priority πnew and a period Tnew, denoted τ , is the lowest priority task τ such that: = arg min

τ i ∈lp(new)     Sl i T i Tnew     (6)
Note that our definition of limiting task is based on the sufficient condition in Theorem 1. As a result, it is a good indicator of where the bottlenecks for software evolution are, but it is not an exact criterion (yet).

We are particularly interested in the fact that some tasks never limit C max S , whatever the priority and period of τnew. Theorem 4. Consider the system S. The tasks that will never limit the system are all the tasks τi such that:

∃τj ∈ S s.t. τj ∈ lp(i) ∧ Tj ≤ Ti
Proof sketch of Theorem 4. Tasks for which there exists another task of lower priority (hence with more preemptions) and lesser or equal period (hence with less or the same available time to finish) can never be the limiting task.

A good strategy to increase the flexibility of the system is to decrease the interference of higher priority tasks on the limiting task τ , i.e., to increase its slack. One source of complexity here is that the limiting task is not necessarily the same for different values of Tnew and πnew.

We therefore identify the values of the period Tnew upon which τ may change. The set of these values is:

T = t ∈ N + | ∃τi ∈ S, Ti t = Ti t -1 (7)
This corresponds to the values of Tnew for which the number of preemptions of τnew on τi, with i ∈ lp(new), changes. It follows that τ remains constant in any interval [T i new , T j new [ where T i new and T j new are two consecutive periods in T . It is thus sufficient to compute the limiting task of S w.r.t. each priority πnew and period of Tnew ∈ T using Eq. ( 6).

CASE STUDY

Let us now show how the concepts presented in this paper are applied on an example. Consider a system: S = {(2, 10, 1), (4, 5, 1), (6, 15, 1), (8, 10, 2), (10, 30, 2)} Case 1: Priority and period of τnew are known Suppose that we want to add a task τnew to S, with πnew = 1 and Tnew = 5. By applying Theorem 3 and Definition 6 we determine that C max S = 1 and τ5 is the limiting task of S. This means that τnew should not have an execution time larger than 1 otherwise τ5 may miss its deadline.

Case 2: C max

S as a function of Tnew

Let us now assume that we know nothing about τnew and we want to quantify the flexibility of S.

Table 1 shows the values of C max S obtained for the possible values of πnew and τnew. Whenever any WCET larger than 0 would make one task in S unschedulable we put ⊥. Note that we group periods of τnew for which the number of preemptions of tasks in S does not change, based on the computation of T . In addition, if πnew ≥ 11 then τnew will have no impact on the system so we do not represent C max new . Similarly, Table 2 shows C max τnew for possible values of πnew and Tnew (we leave out periods larger than 15). Finally, based on Table 1 and Table 2 we easily obtain Table 3 which shows the possible values of C max Snew . The concepts introduced in this paper allow the system designer to: (1) understand when an evolution will be constrained by the need to preserve the schedulability of the system, and when it will be constrained by the need to schedule a a a a a a (2) identify, through the concept of limiting task, which task in the system will "break" first in case of a software update.

Tnew πnew 1 3 5 7 9 [2, 3[ ⊥ ⊥ ⊥ ⊥ ⊥ [3, 4[ 1 1 1 1 1 [4, 5[ 1 1 1 1 1 [5, 6[ 1 1 1 1 1 [6,

CONCLUSION

In this paper we have defined the flexibility of a system as its capability to schedule a new task. We also presented an approach to quantify the flexibility of a system. More importantly, we show that it is possible under certain conditions to identify the task that will directly induce the limitations on a possible software update. If performed at design time, such a result can be used to adjust the system design by giving more slack to the limiting task. We illustrate how these results apply to a simple system.

We plan to extend our work in several main directions. First, we want to replace our sufficient conditions for by necessary and sufficient conditions so as to provide more relevant information to the system designer.

Second, we want to study further the notion of limiting task and propose a solution to compare the flexibility of different systems. Our objective is to come up with a set of guidelines for the designer to help him factor in flexibility at design time. Such guidelines must be simple to understand by someone with limited expertise in schedulability analysis, and they must take into account the fact that many design choices are fixed.

Finally, we intend to study more complex systems. We are in particular interested in systems with jitter, sporadic a a a a a a bursts, task chains, multiple processing resources, etc. When compared to the general sensitivity analysis problem, the problem we consider has many fixed parameters. This is why we expect to be able to provide useful results even for such complex systems.

Table 1 :

 1 C max

	8[		2	2	2	2	2
	[8, 10[	2	2	2	2	2
	[10, 15[	3	3	3	3	3
	[15, 30[	3	3	4	4	5
	[30, +∞[	3	3	4	4	11
	S		for different values of πnew and Tnew
	a Tnew a a 2	a πnew 3 a a 1	5 ⊥	7 ⊥	9 ⊥	11 ⊥
	3		2	1	⊥	⊥	⊥
	4		3	2	1	⊥	⊥
	5		4	3	2	⊥	⊥
	6		5	3	2	⊥	⊥
	7		6	4	3	1	⊥
	8		7	5	4	2	⊥
	9		8	6	5	3	1
	10		9	7	6	4	2
	11		9	6	5	1	⊥
	12		10	7	6	2	⊥
	13		11	8	7	3	1
	14		12	9	8	4	2
	15		13	10	9	5	3

Table 2 :

 2 C max τnew for different values of πnew and Tnew the new task;

Table 3 :

 3 C max Snew for different values of πnew and Tnew

	Tnew	πnew 1	3	5	7	9	11
	2	⊥	⊥	⊥	⊥	⊥	⊥
	3	1	1	1	⊥	⊥	⊥
	4	1	1	1	1	⊥	⊥
	5	1	1	1	1	⊥	⊥
	6	2	2	2	2	⊥	⊥
	7	2	2	2	2	1	⊥
	8	2	2	2	2	2	⊥
	9	2	2	2	2	2	1
	10	3	3	3	3	3	2
	11	3	3	3	3	1	⊥
	12	3	3	3	3	2	⊥
	13	3	3	3	3	3	1
	14	3	3	3	3	3	2
	15	3	3	4	4	5	3


Sönke Holthusen

Sophie Quinton
email: sophie.quinton@inria.fr

Ina Schaefer
email: i.schaefer@tu-bs.de

Johannes Schlatow
email: schlatow@ida.ing.tu-bs.de

Martin Wegner
email: wegner@ibr.cs.tu-bs.de

Using Multi-Viewpoint Contracts for Negotiation of Embedded Software Updates

In this paper we address the issue of change after deployment in safety-critical embedded system applications. Our goal is to substitute lab-based verification with in-field formal analysis to determine whether an update may be safely applied. This is challenging because it requires an automated process able to handle multiple viewpoints such as functional correctness, timing, etc. For this purpose, we propose an original methodology for contract-based negotiation of software updates. The use of contracts allows us to cleanly split the verification effort between the lab and the field. In addition, we show how to rely on existing viewpoint-specific methods for update negotiation. We illustrate our approach on a concrete example inspired by the automotive domain.

Introduction

Critical embedded systems currently offer limited support for software updates. In the automotive domain, this leads to outdated software being used on mechanically durable vehicles. Adaptable vehicle electronics could be used, e. g., for increasing safety via software patches, or to limit costs by a better usage of computational resources. In a different context, aerospace computing platforms are currently migrating from fixed, ground-verified configurations to re-configurable platforms, and from functionally separated solutions to integrated systems with the capability to change during operations. These two examples illustrate the fact that we need to support flexible adaptation of safety-critical embedded systems via continuous change after deployment.

At the moment software updates in critical embedded systems are prepared via intensive verification and tests performed in the lab. Unfortunately, this lab-based verification process is becoming increasingly difficult, in particular because of complex platform dependencies between changing applications-for example through timing, fault handling, security mechanisms, etc. Every particular system configuration is different and there are just too many of them to perform exhaustive a priori verification, even using abstraction techniques. For this reason, our goal is to use in-field formal analysis to determine whether a specific update in a given system configuration may be safely applied.

Although promising, in-field verification of software updates for safety-critical embedded systems is also challenging because it requires an automated process able to handle multiple viewpoints such as functional correctness, timing or security, with access to limited resources. For this purpose, we propose a contract-based methodology. Such an approach is particularly well-suited to cleanly split the verification effort between the lab (pre deployment) and the field (post deployment). In addition, it lends itself to our original approach whose specificity is to address multi-viewpoint verification based on a combination of existing viewpoint-specific methods. Our work is motivated by the project Controlling Using Multi-Viewpoint Contracts for Negotiation of Embedded Software Updates Concurrent Change (CCC) 1 , which addresses new methods to develop and control embedded system platforms integrating changing applications under high requirements to real-time, safety, availability, and security. The methodology is currently being implemented as a complete tool chain. We strive to present our current results both at a high level of abstraction, so that our results can be reused or adapted to other contexts, and at a lower level of abstraction so that our theory matches the practical needs of the CCC project. This dual approach is reflected in this paper. This paper is organized as follows. Section 2 introduces the general methodology that we propose. Section 3 then presents the actual context in which we develop this approach. In Section 4 we show the effectiveness of our methodology on a concrete example in the automotive domain. Finally, Section 5 discusses the state of the art and Section 6 concludes.

Contracting for software update negotiation

We present here our general approach to in-field negotiation of software updates.

Problem statement

Let us state first that, independent of verification, software updates require a component-based approach. The overall objective of in-field negotiation is then to guarantee that conformance to system requirements is preserved during the update. It is however likely that establishing conformance monolithically will not be feasible in practice; hence the use of contracting, which clearly splits responsibilities between a component and its environment so as to make design and verification easier. As a result, our methodology assumes that the following primitives are given.

Component framework. We suppose a given notion of component so that one can specify requirements and verify that a given system conforms to them.

• component: In this paper we address software updates so the term component refers to software components. How these components are specified depends on the actual framework, but at this point we do not make any assumption about them. A set of components form what we call a software model.

• system model: A software model alone is not sufficient to describe a system if one wants to verify non-functional properties. Therefore, we define a system model as a triple made of:

a software model; a platform model, which is not subject to change;

a configuration that describes all runtime parameters relating components and platform which may be changed during negotiation.

• system requirements: The whole verification problem supposes that there exists some formal representation of the expected behavior of a system, which we suppose given as a set of requirements. In addition, we need a formal relation between systems and requirements, that we call conformance, to allow establishing that a given system conforms to its specified requirements.

Contract theory. We further assume primitives relating to contracting.

• contract: A contract for a component K is a pair (A, G) consisting of an assumption A on the system in which K will execute and a guarantee G on the way K will behave in such a system.

• contract satisfaction: Components and contracts are related via a contract satisfaction relation. Intuitively, a component satisfies a contract C = (A, G) if, assuming that A holds, then G holds, too.

• compatibility of contracts: This concept is derived from the above primitives. A set of contracts is compatible with respect to a platform model if there exists a feasible configuration, i. e., a configuration such that, in any system made of components satisfying the given contracts, if assumptions on the environment of the system hold then all assumptions and therefore all guarantees hold.

Contract compatibility is the cornerstone of the contract-based approach as it does not require the actual components to be available, only their contracts. Because of that, we use from now on the term software model to refer to the set of contracts abstracting the components. Besides, note that an additional verification step is in principle needed after compatibility has been established in order to derive conformance to system requirements from assumptions and guarantees. In our case, system requirements are always expressed directly as assumptions or guarantees so we will largely ignore this step in the rest of the paper.

In a context where a component framework and a corresponding contract theory have been developed, we can now formulate our problem as follows.

Definition 1 An update request is a pair (changeType, C ) where

• changeType describes the change to undertake which is one of the following {add, remove, update};

• C is the contract attached to the component undergoing change.

The objective of the negotiation process is to determine whether the update request can be granted and if that is the case then for which configuration.

Definition 2 A negotiation process is a function taking a system model sys = (software, platform, config) and an update request (changeType, C ) as parameters and returning an answer: either no, or yes along with a feasible configuration c. This means that negotiation is a synthesis problem: we need to synthesize a configuration that makes all contracts compatible.

Design and verification flow

The use of contracts effectively splits the verification process between the lab and the field, as we show in the following.

In the lab. At design-time (see Figure 1), during software development and test in the lab, additional data for helping the in-field negotiation process are prepared and formalized as contracts. They will typically include properties of the software components which can only be obtained using involved verification methods, e. g., requiring manual intervention such as theorem proving, or intensive computation, for example in the case of model checking. Assumptions on the environment in which the system will function may also be specified. Contract satisfaction is then established in the lab, as both the component and its contract are available. This step is performed for every component independently and saves the effort to verify every possible combination of components and possibly versions of components. In the field. After deployment, whenever an update is requested, formal verification is performed to determine whether the update may take place without risking a violation of system requirements. This step precedes the actual update and the system architecture is designed to ensure that it does not disrupt the running system. A negotiation process takes place, aiming at finding a system configuration which will guarantee that all system requirements will be satisfied after the update. This is the challenge of the approach as this synthesis and verification phase must be performed automatically, with limited memory and in reasonable time. Updates will typically be performed while the system is suspended (e. g., overnight while the car is parked) so that the time constraint exists but is less tight than the memory constraint.

Partially Manual Analysis Component

To succeed, the component in charge of the negotiation, which we call the Negotiation Controller (NC), can rely on the contracts that have been prepared at design time. A first specificity of our approach is that we do not try to tackle all viewpoints together as in e. g., [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF]. Instead, we rely on viewpoint-specific analysis engines, each of which uses a model that is best adapted to the particular viewpoint it is dealing with. This also means, we do not encode the search for a configuration into one big constraint-solving problem including all viewpoints. We reduce the possible variables for the main problem to a minimum, while the viewpoints can solve viewpoint-specific problems on their current partial configuration. Besides, the brute-force approach that involves checking all possible configurations until a feasible one is found is not viable due to the size of the configuration space. To tackle this, a second specificity of our approach is that we rely on added capabilities of the viewpoint-specific analysis engines. Indeed, our experience is that these engines, although used in general for checking one given configuration, can be extended to provide information about sets of configurations. Our strategy is therefore to start from an over-approximation of the set of feasible configurations and iteratively update this set based on the results provided by the analysis engines. More precisely we proceed as shown in Figure 2.

1. The NC computes a set of configuration candidates which is represented as a set of constraints.

2. The NC then picks one candidate and triggers the viewpoint-specific engines so that they check if that candidate configuration is feasible w. r. t. the considered viewpoint -and as such a witness to the software model being compatible with respect to the platform model.

3. If the configuration is not feasible, one engine returns a set of additional constraints to the NC. If the configuration is feasible for all viewpoints then the update can be accepted.

4. The last two steps repeat until the NC can no longer find a candidate or if a feasible configuration has been found.

In the rest of this paper, we show in more detail how we follow this approach in a specific, applied context.

Software Model

Software update negotiation in the CCC project

In this section, we present the architecture that we are currently developing to support negotiation in the context of the CCC project. Our goal in this section is to define all the concepts used in Definition 2, namely: a software model represented as a set of contracts, a platform model and a notion of configuration -and to show how we use them to perform contract negotiation.

Platform architecture. Similar to integrated architectures like AUTOSAR [START_REF]AUTOSAR Website[END_REF] or ARINC 653, our approach offers a clear separation between software/application and hardware/platform components through a Runtime Environment (RTE). We use the Genode OS Framework [START_REF]Genode Website[END_REF] as RTE, which allows for the design of component-based systems where access control is applied via so-called capabilities. Our architecture complements the RTE with a so-called Multi-Change Controller (MCC) which acts as negotiation controller. Similar to the EPOC [START_REF] Neukirchner | The EPOC architecture -enabling evolution under hard constraints[END_REF] project, the MCC is divided into a model domain, in which analyses are performed without actually modifying the system, and an execution domain, in which the update is implemented. In this paper, we focus on the model domain.

Component framework. Our software is built as a set of functions made of components. For convenience, we only consider here functions with a single component so most of the time, we will abstract functions away. Components are interconnected via services: components can offer services to each other, or require services from one another. Matching between offered and required services is made via comparison of the corresponding service interfaces, which describe the services' expected type of communication.

Communication between components can be performed synchronously via Remote Procedure Calls (RPCs) or asynchronously using signals. More precisely, RPCs allow passing arguments to the component being called, but the caller cannot continue its execution until the callee has finished handling the request. In contrast, signals can be used asynchronously, only notifying the callee and ending the communication afterwards.

Components are implemented as one or more threads such that each thread can be activated by: (1) another component requiring a service via an RPC or a signal; (2) another thread of the same component; or (3) a timer.

Requirements. Although the scope of the CCC project is larger, we consider in this paper the following viewpoints.

• functional dependencies: This viewpoint addresses issues related to the structural information presented above, e. g., to guarantee that all required services are indeed provided.

• timing: The timing viewpoint is typically concerned with establishing that a function reacts to an input within a specified delay.

• functional correctness: Functional correctness focuses on control flow properties, e. g., expressing that a given service cannot be called before some initialization step has been performed.

All the above system requirements can be expressed at the component or function level so we specify them directly in our contracts. Conformance to these requirements is thus established if contract compatibility is guaranteed.

Contract framework. To express assumptions and guarantees related to our three viewpoints we have developed a contract language capturing all the relevant information. Rather than using a formal definition, in the following we choose to describe our language through an example.

Functional dependencies. Listing 1 shows the contract for a component T, which requires a service ob-ject_recognition (line 3) and provides a service trajectory_calculation (line 4). The names of the required and provided services are IDs, linking to a more detailed service description in a global repository. Knowing the required and provided services of all components, functional dependencies can be resolved [START_REF] Schlatow | An extensible autonomous reconfiguration framework for complex component-based embedded systems[END_REF].

Timing. The timing requirement is specified at lines 20-22 and states that the RPC call to object_recognition must complete within 100 time units. In addition, to enable timing analysis [START_REF] Henia | System level performance analysisthe SymTA/S approach[END_REF], contracts must contain enough information to extract a task graph [START_REF] Henia | Integrating formal timing analysis in the realtime software development process[END_REF]. A task graph is a directed graph in which nodes represent tasks and edges represent the asynchronous (or synchronous) activations/calls and returns. For that purpose the thread structure as well the nature of communication (RPC or signal) must be known.

In our example, the component is made of two threads called trajectory_calculation_get and trajectory_calculation_init. The former is triggered via RPC (line 7 in the listing). When activated it first proceeds with executing some local processing task which takes between 1 and 5 time units to complete on a computing resource of type CPU_type_1 (lines 8 to 10). It then performs an RPC call to use a service (line 11) and finally executes another task before completing (lines 12-13). Functional correctness. Finally, the functional requirement is specified at lines 23-25. It requests that the trajectory calculation must always be initialized before it is used. Such control flow properties can be easily checked on a control flow graph extracted from the contracts.

Note that our contracts do not explicitly distinguish assumptions from guarantees. In addition, a significant part of the guarantees hold independent of the assumptions and can thus be regarded as part of a specification rather than a contract. We have chosen this presentation to improve readability. In the contract for component T, the assumptions correspond to the three viewpoint-specific requirements. The most notable guarantees regard worst-case execution time bounds, which can only be formally established using involved verification techniques including abstract interpretation [START_REF] Wilhelm | The worst-case execution-time problem -overview of methods and survey of tools[END_REF]. System model. Let us synthesize the information presented above to define our system model. Remember that a system model is made of a software model, a platform model and a configuration.

• software model: this is the set of contracts used as an abstraction layer on top of components. Note that only the components that are actually part of the chosen configuration will be loaded when a new configuration is set up.

• platform model: for contract negotiation we need some abstraction of the platform as well. The only non-functional viewpoint that we address here is timing, so information about the available processing resources and their scheduling policy is sufficient, as will be detailed later. As already mentioned, we assume that the platform model is fixed.

• configuration: this describes how the selected software components are connected to each other and to the hardware. It consists of a set of connections (functional dependencies) between offered and required services, a mapping of tasks to the platform resources, and priorities assigned to tasks.

Denote software the set of software contracts that make up the software model. The set of services (and whether they are required or offered by a given component) as well as the set of tasks that correspond to a given component can easily be extracted from the component's contract.

Denote platform the set of processing resources that constitute the platform model. In our case all resources have the same scheduling policy, namely static-priority preemptive, so the only additional information we need about them is their type in order to guarantee an appropriate mapping of tasks. Definition 3 A configuration config is a tuple (C, SC, M, Π ) where:

• C ⊆ software represents the set of selected components, i. e., components which must be loaded and run on the platform.

• SC is a set of service connections, i. e., of triples (c 1 , s, c 2 ) with c 1 , c 2 ∈ C representing a connection between two components c 1 and c 2 via a service s .

• M is a function associating to each task the resource onto which it is mapped.

• Π is a total priority order on tasks.

Note that not all these configurations are well-formed as we discuss below.

Negotiation process. In this section we formally define how the configuration space is constrained during the contract negotiation. The objective of the negotiation process is to find a feasible configuration. To achieve this the MCC picks a configuration from a set of candidates called the configuration space and runs it through the viewpoint-specific analysis engines to determine whether it is feasible.

Initially the configuration space contains all well-formed configurations (see below). It is then iteratively restricted based on the feedback provided by the viewpoint-specific analysis engines.

It has been shown in [START_REF] Schlatow | An extensible autonomous reconfiguration framework for complex component-based embedded systems[END_REF] that the functional dependency resolution problem can be formulated entirely as a set of constraints, so there is no need for a specific, dedicated analysis engine. Such constraints include in particular:

1. For all (c 1 , s, c 2 ) ∈ SC, c 1 = c 2 and the service s is indeed required by component c 1 and offered by component c 2 .

2. For every selected component c 1 ∈ C requiring a service s, there is a unique selected component

c 2 ∈ C such that (c 1 , s, c 2 ) ∈ SC.
Regarding mapping and priority assignment, not all configurations are well-formed either as the following constraints must be met:

3. A task τ can only be mapped onto a resource r if r is of the type for which execution time bounds are provided in the contract corresponding to τ.

4. Tasks from the same thread must have the same priority.

Definition 4 A configuration (C, SC, M, Π ) is well-formed if and only if it satisfies the four above mentioned conditions.

In contrast, functional correctness may require intricate analysis which is best kept separate from the main set of constraints. Whenever a configuration is rejected by the functional correctness analysis engine checking control flow properties, a new constraint is added to restrict SC. Such constraint will typically forbid any configuration in which c 1 is selected and (c 1 , s, c 2 ) is a service connection if it has been established that c 1 is "misusing" the service offered by c 2 . Note that this removes a fairly large set of configuration candidates, namely all possible mappings and priority assignments for each SC eliminated.

Finally, timing analysis is the most challenging part of our negotiation scheme. Encoding the response-time analysis as an ILP (integer linear programming) problem has been done [START_REF] Wieder | Efficient partitioning of sporadic real-time tasks with shared resources and spin locks[END_REF], but at the cost of either a prohibitive complexity or pessimism, meaning that configurations which may be feasible are discarded. Our strategy is to perform timing analysis using state of the art timing analysis tools such as e. g., pyCPA [START_REF]pyCPA Website[END_REF] but to better exploit the provided result. Suppose for example that timing analysis cannot guarantee that a given task τ will meet its deadline in the worst case. This means that for the current mapping any configuration that keeps the same priority for τ and higher-priority tasks will violate τ's timing requirement. A full theory of how such constraints can be generated is in progress and out of the scope of this paper but it is particularly interesting to remark that such issues have been relatively ignored so far in the real-time systems research community.

Application to an automotive example

Let us now illustrate our approach to contracting for update negotiation on an example taken from the automotive domain. We consider a car in which a function for parking assistance is deployed and show how it can be updated to add a function for lane detection. We first describe the software components we use and their relevant properties before elaborating on the negotiation process.

System model and viewpoints before the update

The component P for parking assistance depends on trajectory_calculation, a service for calculating a trajectory for the car (i. e., a list of vectors to steer the vehicle). That service, which is provided by component T, itself needs an object_recognition service to determine which objects must be avoided. Suppose that two components offering this service are available (O 1 and O 2 ), with O 2 additionally offering a service object_masking for masking objects.

Initial configuration. Assume that during deployment all the above components have been uploaded onto a unique hardware resource called CPU1. Figure 3 shows how functional dependencies are solved in the current configuration. Note that only P, T and O 2 are selected -meaning that the code and contract of O 1 are available but not currently in use in the system. The rest of the configuration, namely task mapping and priority assignment will be discussed later. Initial requirements. Let us describe our system requirements. Listing 2 shows the contract for component P. Note that two keywords have not been introduced before, namely initialization and time. The former refers to an initial operational mode that precedes the normal mode in which all other calls are performed. The latter term is used to introduce an activation pattern which describes how often a given thread is activated based on a timer. In our case, thread park_assist is activated periodically every 200 time units with a possible jitter of at most 5 time units.

The contract for T has already been introduced in Listing 1. Due to space constraints the contracts for components O 1 and O 2 are omitted. In addition to functional dependency constraints, there are only two timing requirements and one control flow property to verify:

1. Each activation of the park_assist thread must complete within 150 time units -this requirement is specified in Listing 2. 3. trajectory_calculation_get must not be called before at least one call to trajecto-ry_calculation_init has been made. The last two requirements are from the contract for component T.

Timing viewpoint. The task graph presented in Figure 4 shows two task chains corresponding to the normal mode of operation of P and its initialization mode, respectively. This graph has been obtained by unfolding the task graphs inside the thread description with the concrete task graphs of called threads. This means the RPC to trajectory_calculation.init() in Listing 2 is replaced by the corresponding task graph from the contract for component T (Listing 1). Furthermore, the call of object_recognition.get() is replaced by the corresponding task. This continues until all RPCs are replaced by tasks. Note that O 2 has a task which is never activated (namely the task corresponding to the object_masking service) and is thus omitted in the task graph. Because our platform model consists of only one resource, all tasks are mapped to CPU1. In presence of several operational modes timing analysis is performed separately for each mode [START_REF] Sha | Mode change protocols for priority-driven preemptive scheduling[END_REF]. Therefore in the normal mode of operation only the first chain of tasks is considered. Our two timing requirements translate at the task level into latency constraints: one from a call to task p1 to the end of p2; the other from a call to tc1 to the end of tc2. We will detail how such requirements are verified in the description of the negotiation process.

Control flow graph. In our example we have chosen a very simple functional correctness requirement, which can be directly derived from the semantics of the keyword initialization in our contract language. We therefore omit the description of the control flow graph that can be derived from the contracts and focus on the more intricate timing aspects of our example.

Update scenario

Our objective is to add to the system a component L implementing lane detection, for which it requires services for object_recognition, object_masking as well as a service for steering provided by a component S which is also to be uploaded. We omit the contract for S but show the contract for L in Listing 3: component L is made of a single thread which sequentially calls services object_recognition, object_masking and steering while performing some internal computation in between calls.

Contract negotiation

Now we can show how our negotiation process is performed to allow the addition of the lane detection function.

Functional Dependency. The first step of contract negotiation aims at finding the set of partial configurations guaranteeing that every service required by a component in the software model is provided by another component in that model. In our case we need to account for the services required by the component to be added to the software model, namely L (note that S does not require any service). Functional dependency is thus solved on the software model consisting of components P, T, O 1 , O 2 , S and L. Figure 5 illustrates the result, as we explain now. Full lines between offered and required services represent links for which there is no alternative. For example, T is the only component offering service trajectory_calculation required by P, making the connection between the two mandatory. In contrast, the object_recognition service required by T can be provided by O 1 and O 2 , which we denote using dashed lines. Any configuration which matches one of those represented in Figure 5 will guarantee compatibility at the functional dependency viewpoint. For the sake of simplicity we will assume that the service interfaces for object_recognition prevent O 1 and O 2 from offering that service to more than one component. In that case there are only two possible solutions left.

Functional correctness. The part of the control flow graph which is relevant for the requirement imposed by T does not change after the update so the functional correctness viewpoint does not need to constrain the configuration space: any configuration which satisfies the functional dependency constraints also passes the functional correctness test.

Timing. The last, more elaborate viewpoint we consider for our example is timing. A simple load analysis, performed, e. g., using pyCPA2 , will reject the functional configuration shown in Figure 6. The reason is that the task chain corresponding to the lane assist function is activated every 100 time units. If or1 is part of this chain, then that chain requires 90% of the available CPU time. However, the park assist chain has a 15% load (i. e., 30 time units every 200 time units). This means that no matter what the priority assignment is, the processor will be overloaded. The only option consists in swapping or1 and or2 in the functional configuration.

Our objective is now to find a priority assignment that satisfies the specified latency constraints. Remember that tasks inherit their priority from the threads to which they belong. In addition, we do not assign the same priority to multiple threads as this typically only adds more pessimism to the analysis result.

Let us focus on the end-to-end latency requirements imposed by P and L, which are respectively 150 Figure 6: Task graph for one of the two possible functional configurations.

and 75 time units. The constraint on P is relatively loose and in fact it will be satisfied even if the park assist function is blocked by the complete lane assist task chain. Therefore, giving higher priority to the tasks involved in the lane assist function will always provide a feasible configuration. Interestingly, it is also possible to establish that the lane assist chain cannot afford to be blocked by the or1 task. In that case, a constraint stating that or1 must have lower priority than all the tasks involved in the lane assist function can be added to restrict the configuration space.

Discussion

The main purpose of our example was to illustrate how the contract negotiation process works, and in particular how incompatibility in one viewpoint can result in additional constraints to the configuration space. Therefore we kept the example quite simple. Moreover, note that the methodology is not yet fully implemented: the functional dependency analysis exists but it is not connected to the timing analysis engine at the moment. We currently mainly focus on providing useful timing analysis feedback.

Related work

Design of complex systems of components using contracts, or interfaces, has been widely studied since it was introduced by de Alfaro and Henzinger in [START_REF] De Alfaro | Interface automata[END_REF]. A great variety of interface theories have been developed, which mostly focus on incremental design. There has been active research lately on contract theories dealing with multiple viewpoints. For example, Reineke et al. focus on issues such as consistency between viewpoints [START_REF] Reineke | Basic problems in multi-view modeling[END_REF]: if two viewpoints have some degree of overlap, how is it possible to guarantee that they do not contradict each other? Perssone et al. give a high-level classification of model-based approaches to multi-view systems, which also discusses additional challenges of multi-view modeling [START_REF] Persson | A characterization of integrated multi-view modeling in the context of embedded and cyber-physical systems[END_REF]: traceability of information between views, reuse, automation, change propagation and extendability. In [START_REF] Panunzio | A component-based process with separation of concerns for the development of embedded real-time software systems[END_REF] Panunzio et al. give a more applied contribution as they propose a component model for separation of concerns backed by case studies originating from the European Space Agency. However, none of these results address dynamicity.

Another line of work related to this paper regards languages for contracts. The BCL language [5] has now been used in many safety-critical industrial applications. An alternative is the contract language from [START_REF] Cimatti | Contracts-refinement proof system for component-based embedded systems[END_REF] which is based on temporal logic. Note however that our interest is less in the language aspects than in the methodology.

Changing constrained systems are in the focus of the FRESCOR project [START_REF] Sojka | Modular architecture for real-time contract-based framework[END_REF], in which contracts are used to ensure Quality of Service on the network-layer. However, the project focuses on bandwidth and latency constraints usually found in multimedia applications. In this context contracts may be broken (at times), enabling the test of novel configurations during runtime. This is not acceptable when updates have an impact also on safety-critical functions such as driver assistance systems in a car. The EPOC project [START_REF] Neukirchner | The EPOC architecture -enabling evolution under hard constraints[END_REF] proposed for the first time a contract-based admission control framework for safety-critical systems, but it was restricted to timing aspects and could not handle multiple viewpoints.

Conclusion

It has become increasingly difficult to test and verify software updates for embedded systems, in particular because of the complex platform dependencies which exist between software components. In this paper we have presented a methodology to split the necessary effort between lab and field.

Performing in-field formal analysis to determine whether an update may be safely applied is challenging because it requires an automated process able to handle multiple viewpoints such as functional correctness, timing, etc. We have proposed an original methodology based on contract negotiation which enables this. In particular, instead of addressing all viewpoints together we rely on viewpoint-specific analysis engines, each of which uses a model that is best adapted to the particular viewpoint it is dealing with. A second specificity of our approach is that we rely on added capabilities of these viewpointspecific analysis engines.

Finally, we have illustrated the benefits of our approach on a realistic scenario from the automotive domain, which we unfold from the specification of contracts until a safe update has been found.

Figure 1 :

 1 Figure 1: In the lab a contract and a proof for satisfaction is generated.

Figure 2 :

 2 Figure 2: With the contracts from the software model and the available hardware resources from the platform model, the contract negotiation takes place in field.

Listing 1 :

 1 An example contract.

Figure 3 :

 3 Figure 3: Resolution of functional dependencies chosen during deployment. Boxes represent components, circles and semicircles represent services that are offered and required, respectively. Service names are abbreviated to their acronym.

Listing 2 :

 2 The contract of P 2. A call to object_recognition_get must return within 100 time units.

Figure 4 :

 4 Figure 4: The task graph before the update. Note that or2 corresponds to the task performing the ob-ject_recognition service in component O 2 .

Figure 6 Listing 3 :

 63 shows the task graph corresponding to one of the possible functional configurations. The second possible task graph The contract of L is obtained by swapping tasks or1 and or2. The values indicated next to the tasks are their worst-case execution time and therefore a property of the task and not of the task graph.

http://ccc-project.org/

https://pycpa.readthedocs.org