Mohammed Foughali

A Two-Step Hybrid Approach for Verifying Real-Time Robotic Systems

Due to the severe consequences of their possible failure, robotic systems must be rigorously verified against (i) behavioral properties, such as safety and (ii) real-time properties, such as schedulability, while taking into account the real hardware (e.g. number of cores) and operating system (e.g. scheduling policy) specificities. Formal verification and schedulability analysis are popular approaches that may help with such verification, but suffer from limitations such as scalability issues (for the former) and difficulty to generalize to complex robotic tasks (for the latter), when used independently. In this paper, we propose a two-step, efficient solution that combines both approaches. The first step provides a sufficient condition for the schedulability of hard-real-time tasks in a robotic application. Then, the second step automatically generates a formal model of the application, on which other important properties may be verified formally using statistical model checking. The solution is applied to an autonomous drone case study.

I. INTRODUCTION

A. Context & Addressed Problem

Robotic software, inherently complex, is majoritarily component-based (e.g. ROS [START_REF] Quigley | ROS: an open-source Robot Operating System[END_REF], Orocos [START_REF] Soetens | Realtime hybrid task-based control for robots and machine tools[END_REF] and G en oM3 [START_REF] Mallet | Genom3: Building middleware-independent robotic components[END_REF]): a number of functional components collaborate while interacting with the hardware. Each functional component implements complex algorithms, often organized in tasks, to perform some computations. Computations results are communicated between components to close the perception-action loop and fulfill the robot's missions.

With many robotic applications being time-critical and running on embedded platforms, robotic tasks must satisfy real-time properties, e.g. schedulability, while sharing limited resources. In addition, it is important that the robot behaves safely and correctly, i.e. that behavioral properties, such as safety and liveness, are verified. Considering the complexity of robotic components and their communication, verifying real-time and behavioral properties is a particularly hard research problem as explained hereafter.

Scenario-based testing, often used by roboticists, is unfortunately unreliable (Pecheur [4] gives an example of a fullyear test failing to detect a bug in a NASA experiment). We must thus rely on more rigorous approaches such as formal methods and schedulability analysis. Formal methods are mathematically sound and can deal with both behavioral and real-time properties, but their use in robotics is impeded by scalability issues. Indeed, if the formal technique is exhaustive (e.g. model checking), the state-space explosion problem is observed in real-world robotic systems, i.e. their state spaces are intractable because of their sheer com- 1 VERIMAG, Université Grenoble Alpes, CNRS, Grenoble, France mohammed.foughali@univ-grenoble-alpes.fr plexity. On the other hand, if the formal technique is non exhaustive, such as Statistical Model Checking (SMC) [START_REF] Legay | Statistical model checking: An overview[END_REF], the properties can no longer be evaluated with certainty, but with some probability, which is not sufficient in critical missions (e.g. if a task in a component is hard real-time (HRT), its schedulability must be verified with certainty). Finally, the literature on formal verification of robotics ignores hardware and OS constraints which restricts the results validity (Sect. V). Likewise, the applicability of schedulability analysis to robotic systems is limited. First, its theoretical results are hardly generalizable to robotic tasks because the latter models are much more complex than the task models used in the real-time systems literature (Sect. II). Second, schedulability analysis leaves other important properties such as liveness and safety unattended.

B. Proposition & Overall Contribution

We propose a novel two-step verification approach that combines formal methods and schedulability analysis, where neither of the two is sufficient alone (Sect. I-A). Our approach enables verifying both real-time and behavioral properties while taking into account the actual specificities of the robotic platform (mainly the number of cores and a scheduling policy). Furthermore, we provide a high level of automation, which makes our approach suitable for robotic programmers with no particular knowledge in formal methods or schedulability analysis.

Step one focuses on guaranteeing schedulability with certainty. We develop a schedulability test for HRT robotic tasks, which belong to a (mixed-) critical application, under a fixed-priority (FP) preemptive policy. If the original application, or a modified version achievable by e.g. modifying tasks deadlines, together with the number of cores on the robotic platform satisfy this test, then schedulability of HRT tasks is guaranteed. This will be the basis of step two, where we verify, up to a high probability, other important properties less crucial than schedulability. Such verification is done with SMC on formal models that we automatically generate from the robotic application, the number of cores and the FP scheduler (altogether proven to satisfy schedulability for HRT tasks in step one). Our approach is applied to a real autonomous drone system, developed using the robotic framework G en oM3, and the verification in step two is carried out using the formal framework UPPAAL-SMC [START_REF] David | Uppaal SMC tutorial[END_REF].

C. Outline

The rest of this paper is organized as follows. In Sect. II, we present the verification problem: we (i) introduce robotic task models, and exemplify through presenting 978-1-7281-4403-0/20/$31.00 ©2020 IEEE G en oM3 and the autonomous drone case study, then (ii) give examples of crucial properties in robotics, and analyze the problems preventing their verification with formal methods or schedulability analysis independently. In Sect. III, we detail our approach. Sect. IV shows and discusses the results of applying our approach to the drone case study. Finally, we compare our work to the state-of-the-art in Sect. V and conclude with possible axes of future work (Sect. VI).

II. THE VERIFICATION PROBLEM

A. Robotic Software Specificities

A robotic software, which we call a system, is made of communicating components (Sect. I-A). To account for timining constraints, a component encapsulates periodic tasks, in charge of its complex algorithms. The latter are organized within services. Because services are heavy and share memory resources, they are broken into small pieces of code, each attached to a state in a Finite-State Machine (FSM), hence the popularity of FSMs in robotics. Thus, there are four "levels" in a system (from the lowest to the highest): pieces of code, services (FSMs), tasks and components.

Though not unanimous in robotics, the above organization is used by most component-based robotic frameworks designed for real-time applications, with subtle differences (e.g. while MAUVE [START_REF] Gobillot | A design and analysis methodology for component-based real-time architectures of autonomous systems[END_REF] and Orocos [START_REF] Soetens | Realtime hybrid task-based control for robots and machine tools[END_REF] confound components with tasks, i.e. a component is a task, G en oM3 preserves both levels). Note that, since there is no standard terminology for most levels, the one we use is that of G en oM3.

1) G en oM3: G en oM3 [START_REF] Mallet | Genom3: Building middleware-independent robotic components[END_REF] is the robotic framework used in this paper. We provide a generic informal description of G en oM3 with a focus on concurrency and real-time aspects.

A more formal example using timed-automata is given in Sect. III-A. Note that this description is simplified for readability and to remain in the scope of this paper (e.g. control tasks and aperiodic tasks are excluded). a) Organization: The organization of a component is shown in Fig. 1, where we can see the three component "levels" described above. Pieces of code are called codels. Each codel, attached to a state of a service FSM, has a Worst Case Execution Time WCET. By abuse of terminology, FSM states are simply called codels. Each task t , featuring a period, is in charge of a set of services S t . We say that each service s ∈ S t is a service of t , and t is the task of s (s cannot belong to any S t with t = t). To perform their computations, codels share the Internal Data Structure IDS of the component. Finally, ports are used to communicate with other components, and are thus accessible by the codels in all components that use them.

b) Behavior: We briefly explain how a component evolves in a top-down fashion (from tasks to codels), following the scheduler-agnostic semantics developed in [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF].

The component is piloted by an external client that requests services. Each task t , at each period, executes only the services previously requested by the client (among services in S t ) sequentially. When a service finishes executing, the task informs the client by sending a report. While communication between clients and tasks is taken into account in our verification (Sect. III), it is abstracted in the rest of this paper for readability and simplicity.

Each service FSM has at least two codels: start (at which the first execution begins) and ether (the termination point). A service execution ends when either (i) codel ether is reached (service is terminated) or another codel c is reached after taking a pause transition, i.e. a transition labeled pause (see the abstract FSM in Fig. 1), we say then the service is paused and refer to c as a pause codel. In the latter case, the service is resumed, at the next period of its task, starting from c. c) Concurrency: Tasks (in a system), each of which executes its requested services sequentially (see previous paragraph), are run as parallel threads (assuming enough cores are available). To maximize parallelism, access to shared memory is handled at the codels level: memory resources (ports or fields of the IDS) that a codel needs for its execution are statically defined, so two codels in conflict (using at least a same port or a same IDS fragment) may not execute in parallel (simultaneous readings are allowed). Thus, while executing its requested services, a task needs to wait when one of such services reaches a codel in conflict with another codel, in another service being executed by another task concurrently. Following this lowlevel concurrency model, a codel may be either thread safe (TS) (not in conflict with any codel) or thread unsafe (TU) (otherwise). Because of ports sharing, codels in conflict may belong to different components (example in Sect. III-A).

d) Specification & Templates: While we content with graphical illustrations of G en oM3 systems, the latter are actually specified textually. Each component is written in a dotgen (.gen) file, in which tasks, services and codels are specified. A system may be then built by #-including the dotgens of the different components in another dotgen.

Templates transform G en oM3 (dotgen) specifications into Tool Command Language (Tcl) structures for automatic generation purposes. The robotic programmer can access all information in the dotgen (e.g. tasks periods, FSM and codels WCET), manipulate them and generate a text file in any format accordingly. We have used this mechanism in previous work to automatically generate formal models [START_REF] Foughali | Formal verification of the functional layer of robotic and autonomous systems[END_REF]. In Sect. III, we give examples of templates developed to automatize the two-step approach presented in this paper. e) Case Study: To validate our approach, we use the Quadcopter case study from LAAS-CNRS. Fig. 1 shows its G en oM3 organization in which some names are modified for simplicity. The system contains five components collaborating to achieve autonomous aerial navigation. We give a high-level description (in terms of components and ports) on how these components collaborate (the interested reader may refer to [START_REF] Foughali | Formal verification of the functional layer of robotic and autonomous systems[END_REF] for more details on each component).

Component MIKROKOPTER processes data from the Inertial Measurement Unit (IMU) and the propellers sensors and uses them to write the current IMU and velocity to ports IMU and Velocity, respectively. Component OPTITRACK processes data from the Optitrack motion capture system and writes it to port Mocap. Component POM reads the IMU and captured position from, respectively, ports IMU (MIKROKOPTER) and Mocap (OPTITRACK), to which it applies an Unscented Kalman Filter UKF to compute the estimated position of the drone that it writes to port Pose. Such position is fed to (i) MANEUVER, which uses it to compute an intermediary goal position that it writes to port Goal and (ii) NHFC, which uses it, together with the current Velocity (from MIKROKOPTER), to compute and update, in port Cmd, the velocity to reach the intermediary goal position (from Goal in MANEUVER). Finally, the perception-action loop closes as MIKROKOPTER reads the updated velocity in Cmd (NHFC) and applies it to the drone propellers.

B. The Verification Challenge

If the drone software above fails, the drone may crash, inducing economic costs and/or human injuries. We give examples of crucial properties that must be verified to avoid such failure, and explain why their verification is particularly challenging.

1) Properties of Interest: The drone system has three critical components: MIKROKOPTER, NHFC and POM. That is, tasks in these components are HRT: each must always finish executing within its period, otherwise the drone may crash. It follows that the schedulability property must be proven always true for these tasks, for all possible scenarios.

In the remaining components (less critical), tasks are allowed to miss their deadlines. However, it is still important to verify that they are e.g. exempt of starvation, that is being, at some point, delayed forever by critical tasks monopolizing resources. For e.g. tasks in MANEUVER, such starvation would make the drone hover forever without fulfilling its mission (as it may not navigate to a final goal position).

2) Difficulties: Now, in order to verify these properties, using model checking (or SMC) or schedulability analysis independently proved insufficient in robotics in general and on this drone system in particular. a) With model checking / SMC: Model checking does generally not scale with complex robotic applications. For instance, we show in [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF] that, although it performs well on the stationary flight application (i.e. component MANEUVER is excluded), model checking with state-of-the-art tools fails to scale on the navigation application involving all the five components (Fig. 2), with eight tasks and over 20 services broken into more than 80 codels. In the same work [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF], we use SMC to verify properties up to a high probability. Though SMC provides better guarantees than scenariobased testing, it is not suitable for the schedulability property of HRT tasks which must be proven with certainty.

Another problem of model checking (and generally formal verification) in robotics is that extending formal models with scheduling algorithms usually penalizes their scalability because of (i) preemption and/or (ii) the necessity to create large models to handle schedulers [START_REF] Foughali | Bridging the gap between formal verification and schedulability analysis: The case of robotics[END_REF], [START_REF] Foughali | On reconciling schedulability analysis and model checking in robotics[END_REF]. For the drone navigation application, the integration of schedulers in formal models (which already do not scale as explained above) produces new formal models that still do not scale, even when preemption is not allowed.

b) With schedulability analysis: From a real-time analysis point of view, we focus on three levels in G en oM3 (and generally robotic) systems: the tasks level, the services level and the codels level (component are abstracted as tasks map to cores). Robotic tasks models are thus more complex than those usually considered in real-time analysis: a robotic task executes a sequence of jobs (codels) at each period rather than one job whose WCET is known. A particular problem is the computation of the WCET of tasks, which is practically intractable. Indeed, besides the fact that a TU codel (Sect. II-A1c) may remain infinitely blocked waiting for resources (robotic frameworks do not guarantee the absence of starvation), the sequence of codels to execute in services by a task may differ from a period to another depending on e.g. which services are requested (Sect. II-A1b). Another problem is, even if such sequences WCET are somehow obtained, theoretical results of schedulability analysis in the literature are still unusable because the preemption model in robotics is also different (more in Sect. III-A). Finally, schedulability analysis provides no guarantees on other properties excluding schedulability.

III. A TWO-STEP HYBRID APPROACH

Our approach combines both formal verification, by means of SMC, and schedulability analysis to achieve scalable rigorous verification of crucial properties in robotics. We divide properties into two types: Type I covers properties that must be verified with certainty (schedulability of all HRT tasks), while Type II comprises properties that may be verified with a high probability (e.g. absence of starvation in less critical tasks). On that basis, a key idea is the following. Since model checking does not scale, then we may use SMC for Type II properties, but only once properties of Type I are verified with certainty. Thus, we first check whether we can guarantee properties of Type I using schedulability analysis. This is the first step of our approach, which takes into account the actual number of cores on the robotic platform and a scheduling policy (Sect. III-A). If step one is conclusive, an UPPAAL-SMC model of the considered application, number of cores and scheduler (already proven to satisfy properties of Type I in step one) is generated. On such formal model, we verify by means of SMC properties of Type II, which concludes the second step of our approach (Sect. III-A). If step one is inconclusive, we give a possible direction on how to pass it (Sect. IV-C).

A. Step One: Schedulability Analysis

Our approach is based on Response Time Analysis (RTA). First, we compute tasks WCETs, taking into account delays caused by mutual exclusion over memory (Sect. III-A1). Then, we compute tasks Worst Case Response time (WCRT) considering the concurrency over cores (Sect. III-A2).

1) Computing tasks WCET: In the following, we explain more where the difficulty of computing task WCET (Sect. II-B2) comes from, using the UPPAAL formal model of the G en oM3 task main (component MIKROKOPTER) of the drone (Fig. 2) shown in Fig. 3. This model, automatically generated, is proven correct w.r.t G en oM3 semantics [START_REF] Foughali | On the Semantics of the GenoM3 Framework[END_REF], [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF]. The model is simplified for readability purposes.

Each timed automata (TA) in UPPAAL, made of locations and edges connecting them, and possibly having a clock x, is called a process. Time invariants (in purple) may be associated with locations, and edges may have guards (in green) and operations (in blue). Processes are arranged to fit with the "layers" vision given in Sect. II-A1: the task layer, composed of processes timer and manager, the services layer, where each underlying G en oM3 service FSM is mapped to an UPPAAL process, and the codels layer, where codels are locations in services processes. Fig. 3 shows that task main has two services: Init and Apply.

Shared variables and functions are used by processes to communicate. Array tab_t holds the names and "statuses" of all services of task t . Each of its cells contains two fields: n, a service name and st, the service status that may be either R (requested by a client) or V (for "Void", otherwise). The timer of t gives at exactly each period a signal, through variable tick_t, to the manager to start execution, by taking the edge start → manage. The operation of such edge Urgency does not belong to any component and is added to enforce urgencies, i.e. prevent unnecessary lazy waits (the receiver (?) edge is always ready). searches, through function next(), for the index of the next requested service in tab_t (having status R) starting at index i_t (initially 0) and stores the result in i_t (the size of tab_t if such service does not exist). At location manage, the manager executes the requested services sequentially: variables lock_t and turn_t are used to pass the control to the next service to execute (computed previously through function next()). When such service finishes execution, either by terminating 1 (e.g. edge end_exec → ether in service Apply) or pausing (e.g. edge run_exec → run_pause in service Init), it computes the index of the next service to execute and gives the control back to the manager. And so, the control passes back and forth between the manager and the requested services until each of the latter has executed once (detected when next() hits the bottom of tab_t), so the manager transits back to start and awaits the next period. Now, at the codels level, a codel c in a service s is represented either by one location c (if it is TS) or two locations c and c_exec (otherwise), plus a location c_pause if such codel is targeted by a pause transition in the underlying G en oM3 specification. The WCET of c is represented with an invariant x ≤ wcet[c_s_t] on location c (c_exec if c is TU) where wcet is an array of all codels WCET indexed with unique identifiers. The array of Booleans mut is used to handle concurrency: it tracks the execution of TU codels in the system. Therefore, guards on edges c → c_exec ensure c does not start executing unless no codel in conflict with c is currently executing, witnessed by the falseness of the corresponding fields in mut. For instance, codel run of service Apply is in conflict with codel recv (in service Connect, executed by the other task comm in MIKROKOPTER), and codel start (in service servo of task control in component NHFC), which explains the guard on the edge run → run_exec in process Apply. If such guard is true, codel run starts executing by taking run → run_exec through which it turns its own field in mut to true to prevent, in turn, codels in conflict with it to execute. This example shows the complexity of G en oM3 (and generally robotic) tasks. From a real-time analysis perspective, we identify two problems. First, the WCET of a sequence of codels (which a task executes) is possibly infinite, because we do not know beforehand how long a TU codel needs to wait to secure the memory resources it needs. Second, even if we bound such waiting times, it is practically infeasible to compute by hand the WCETs of all possible sequences: for instance, summing the WCETs of all codels in all services in a task (assuming we bound and include waiting times in TU codels WCETs) would be a naive solution (such sum would be a coarse overapproximation that will likely prevent finding a feasible schedule). We propose a solution for both problems by, respectively (i) an implementation to bound waiting times for TU codels and (ii) an algorithm to compute the WCET of a task by traversing all possible codels sequences. We explain how solution can be automated.

a) Bounding TU codels WCET: We propose an implementation to enable computing a bound B c on the waiting time (to acquire memory resources, i.e. IDS or ports) of any TU codel c. Then, we get the actual WCET of c by summing its WCET (from the G en oM3 specification) with B c .

The implementation is inspired from multiprocessor memory-sharing protocols. Brandenburg [START_REF] Brandenburg | Scheduling and locking in multiprocessor realtime operating systems[END_REF] reviewed a number of such protocols, mainly categorized into spinbased (busy-wait) and suspend-based, and pointed out that the former are easier to implement and perform better than the latter when durations of critical sections are short. As we explained in Sect. II, FSM in robotics are designed to reduce the times of locking shared resources, which makes spin-based protocols suitable to our case. Actually, the previous reasoning fits with the reality of spinlocks being widely used in robotics (e.g. ROS and G en oM3 systems).

In this paper, we use the MSRP protocol [START_REF] Gai | A comparison of MPCP and MSRP when sharing resources in the Janus multiple-processor on a chip platform[END_REF]. We benefit from the judicious remark made by Brandenburg [START_REF] Brandenburg | Scheduling and locking in multiprocessor realtime operating systems[END_REF] as he clears the confusion that the protocol name may create: in MSRP, the "SRP" part refers to the priority-ceiling-based protocol SRP [START_REF] Baker | Stack-based scheduling of realtime processes[END_REF], which is actually used to handle local resources only on each core/processor, and thus this part of the protocol is not relevant to our case (as all shared resources e.g. ports are global). In contrast, the "M" part deals with global resources (and this is exactly what we will use to bound waiting times): a TU codel c appends itself to a FIFO and its thread is spinlocked until c gets access to shared memory, and spinlocked threads are non preemptible. TS codels are not concerned as they are in conflict with no other codel in the system (Sect. II-A1c). The direct disadvantage of this approach is that all TU codels compete for the shared memory as a whole, which reduces the overall parallelism of the system (it is possible for a TU codel c to be blocked by another TU codel c' in the FIFO even though c and c' are not in mutual conflict).

While we deem this loss in parallelism a fair price to pay for bounding waiting times, we are investigating new FIFOspinlock algorithms to restore it (see future work in Sect. VI).

Let us compute B c of a TU codel c in a service s in a task t . We assume there are n tasks and m cores (m < n). In worst case scenarios, the thread trying to execute c spinlocks after already m -1 threads are in the spinlock FIFO (for accessing shared memory). Since each thread corresponds to a G en oM3 task that (i) is sequential and (ii) spinlocks only when trying to execute a TU codel, the first m -1 entries of the FIFO are occupied by TU codels each in a distinct G en oM3 task, different than t . In the worst case, each t of the m -1 tasks already spinlocked is trying to execute TU codel c with the largest WCET among the TU codels of all services in t . Thus, B c is upper-bounded by the sum of the WCET of codels c . To get that sum, we proceed as follows. (1) For each task t = t, we find, within all its services, the largest WCET of all TU codels. (2) We sort, in a decreasing order, the values found in (1). (3) B c is equal to the sum of the first m -1 values sorted in [START_REF] Soetens | Realtime hybrid task-based control for robots and machine tools[END_REF].

Once B c computed, we sum it with WCET c to get the actual WCET of c (including the maximum time it may wait for memory access). To make codels actual WCETs computations accessible to robotic programmers, we make use of the template mechanism (Sect. II-A1d). We give in listing 1 an example that performs steps (1) and (2) of the algorithm above, then writes (to a file) the list output by (2) for any TU codel in any service in task t . The template generator evaluates everything enclosed in <' '> (resp. <" ">) in Tcl without output (resp. and outputs the result), writes to a file the list after sorting it in a decreasing order. Thus, at the end of these computations, we have the actual WCET of all codels, which we call simply WCET in the rest of this paper (that is, the WCET provided by G en oM3 if c is TS, summed with B c if c is TU). Our approach to compute B c is generic, and may thus be pessimistic in some cases. For instance, if the scheduler is partitioned, some of the m -1 largest elements of wcets_max (listing 1) may belong to tasks allocated to the same core as t , and thus B c is overestimated. However, this generecity brings a valuable advantage. Indeed, since the computation is affinity-independent, the roboticist performs this step only once and, if some HRT tasks do not pass the schedulability test (Sect. III-A2), may try to find a better affinity by reallocating tasks based on the timing constraints already computed (the affinity does not affect such constraints). This is explained further in Sect. IV.

1 <' set wcets_max [list] '> 2 <' foreach comp [dotgen components] { '> 3 <' foreach t_prime [$comp tasks] { '> 4 <' if {t_prime == t} {continue} 5 <' set max_wcet 0 '> 6 <' foreach s [$t_prime services] { '> 7 <' foreach c [$s codels] { '> 8 <' if {[llength [$c mutex]] && ([$c wcet] > $max_wcet)} {'> 9 <' set max_wcet [$c wcet]} '> 10
<' } '> 11 <' } '> 12
b) Deducing tasks WCET: We call each possible (full) codel sequence executed by task t a hyperjob. The largest WCET of all hyperjobs in t is then simply the WCET of t .

Therefore, to compute the WCET of t , we proceed as follows. (1) For each service s in task t , we sum the WCETs of codels involved in each possible path (starting either at codel start or some pause codel, and ending either at ether or some pause codel). ( 2) We find, for each s, the value of the largest among the sums computed in [START_REF] Quigley | ROS: an open-source Robot Operating System[END_REF]. [START_REF] Mallet | Genom3: Building middleware-independent robotic components[END_REF] We sum the values found in [START_REF] Soetens | Realtime hybrid task-based control for robots and machine tools[END_REF]. ( 4) we repeat (1), ( 2), [START_REF] Mallet | Genom3: Building middleware-independent robotic components[END_REF] for all tasks in the G en oM3 system. Thus, this algorithm will give the maximum time to execute the longest possible path in all services in t , which corresponds to the largest WCET of all possible hyperjobs in t (i.e. the WCET of t ).

The above algorithm being classical in model checking, the idea is to benefit from the already existing UPPAAL template [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF] to achieve it. Yet, we know that the overall UPPAAL model of this application does not scale. The good news is, however, we do not need to consider the system as a whole: since WCETs are now known for all codels, we may adapt services processes of task t to allow computing the maximum time of their possible paths (step (1) above) without considering the rest of the system. First, locations c_exec are no longer needed: location c is enough, the invariant bound of which is the WCET of codel c (Sect. III-A1a). That being done, interactions of each service with services outside t cease to exist (since bounds B c are now included in TU codels WCET, all guards and operations involving the mut array are removed). Then, we (i) make all ether and c_pause locations urgent (time cannot progress at them) and add, to each service process of t , a clock y reset to 0 at all edges leaving ether or c_pause locations. This way, y tracks the time of each possible path from location start (or any c_pause location) to location ether (or any c_pause location). We have thus what we need for step (1) of the algorithm above, and may remove all the remaining non-clock guards and operations in the services of t . It follows that there are no more interactions between any service process in t and the rest of the system, which means we can verify each service separately.

Fig. 4 shows the result of these changes to the UPPAAL process of service Apply (Fig. 3). Now, all we need to do is ask UPPAAL for the maximum value of clock y at location ether and each location c_pause using the UPPAAL query pattern sup{p.l} : p.y (with p being the process name and l the location name), store the results and repeat the operation for each service in task t , which corresponds to step (1) of the algorithm above. Then, we perform (2) and (3), then repeat the whole process for all other tasks (step (4)) to get the WCET of all tasks in the G en oM3 system.

2) Analysis: Once tasks WCET computed, we compute their WCRT for RTA analysis. We recall that schedulability tests from the literature are not applicable to robotic tasks even when they take memory-sharing into account. For instance, standard task and scheduling models assume a task executes only one job at each release. This means that, if we use available tests, we should treat each hyperjob as one job and, since such hyperjob is likely to include a TU codel, make it non preemptible (Sect. III-A1a). Consequently, we will most likely end up with a set of non-preemptible tasks, which renders preemptive scheduling useless.

Thus, we need to perform schedulability analysis based on the model in Fig. 5: each hyperjob may be preempted at the end of each codel. The reason for this is rather straightforward: in robotics, elementary pieces of code (codels in G en oM3) are designed by roboticists as the smallest pieces (of the algorithm they belong to) that must be performed with no intermediary perturbations. TU codels present another feature that consolidates the rationale of codels noninterruptibility: their interruption may compromise their memory-dependent computations.

a) Scheduling assumptions:

In this paper, we use a partitioned fixed-priority FP scheduler. There are two main reasons. First, partitioned FP is very popular in domains related to robotics, such as automotive systems (e.g. in AUTOSAR [START_REF] Wieder | On spin locks in autosar: Blocking analysis of FIFO, unordered, and priority-ordered spin locks[END_REF]), since it removes the cost of task migration. Second, global schedulers are known to perform poorly compared to partitioned ones, even though this might result from over-pessimism of tests in global approaches [START_REF] Gracioli | Implementation and evaluation of global and partitioned scheduling in a real-time OS[END_REF].

The task set of the robotic system is the union of HRT and less critical tasks τ = τ h ∪ τ l . There are two priorities: pr h (rep. pr l ), the high (resp. low) priority, assigned to all tasks in τ h (resp. τ l ). The platform features m cores C 1 ...C m (m < |τ|). Let Aff i ⊆ τ be the affinity of core C i , that is the set of tasks allocated to it. Then,

Aff i = Aff il ∪ Aff ih where Aff il = τ l ∩ Aff i (resp. Aff ih = τ h ∩ Aff i )
is the set of low (resp. high) priority tasks allocated to C i . Since the algorithm is partitioned, each task is statically allocated to only one core, that is ∀i, j ∈ 1..m, i = j : Aff i ∩ Aff j = . The size of the queue of C i is equal to the cardinality of its affinity |Aff i |.

b) Computing tasks WCRT: Following the model in Fig. 5, a task is a set of hyperjobs t = {hj 1 ...hj |t| }. A hyperjob is an ordered set of codels hj = {c 1 ...c |hj| }. If a codel c belongs to a hyperjob in t , we may say simply that c belongs to t .

When needed, we use the superscript ( t ) to denote that a hyperjob or a codel belongs to task t , and the double subscript jk to denote that a codel c j belongs to hyperjob hj k . At each period P t , one (depending on the evolution of the system) of hyperjobs in t is to be executed. The WCRT of t defines an upper bound on the time separating the moment a i , at which a hyperjob hj i is activated (arrives in a core queue), and the moment f i , at which it finishes its execution and frees the core, that is WCRT t = max i∈1..|t| (f ia i ) (eq. 1). Let r i ∈ [a i , f i ) be the moment hj i is released, that is a core is given to it and it starts to execute ( f i is excluded because hj i cannot execute in a zero time). By inserting r i in eq. 1 we get WCRT t = max i∈1..|t| (f ir i + r ia i ) which we may upper bound WCRT t ≤ (max i∈1..|t| (f ir i ) + max i∈1..n (r ia i )) (ineq. 2). Now, we know that the left-hand operand of the right-hand side of ineq. 2 is the WCET of t which we already computed in Sect. III-A1. We call the remaining operand the Worst case Waiting Time WWT t = max i∈1..|t| (r ia i ) (eq. 3). Therefore WCRT t ≤ WWT t + WCET t (ineq. 4).

A hyperjob hj of a high-priority task t allocated to core C i (t ∈ Aff ih ) worst position in the prioritized queue of C i is equal to |Aff ih |. The worst waiting time of hj corresponds to this very position (hyperjobs of tasks in Aff ih , having the same priority pr h as t , are already in the queue, so hj has to wait for them to finish). Now, in this worst situation, the worst case is when the hyperjob at the head of the queue cannot start immediately as a low-priority task hyperjob hj is still not preempted (we recall that preemption points are set at the end of each codel, Fig. 5). It follows that the worst waiting time for hj is equal to the sum of the WCET of all |Aff ih | -1 hyperjobs (each belonging to a task t ∈ Aff ih \{t}) in the queue plus the WCET of the codel of hj being currently executed. We maximize such worst waiting time for all hyperjobs in t to get WWT t (see eq. 3). To account for the waiting needed for high-priority hyperjobs, we maximise the WCET of all hyperjobs in each task t ∈ Aff ih \{t} and sum them [START_REF] Quigley | ROS: an open-source Robot Operating System[END_REF]. Then, we add to the value obtained in (1) the waiting for preemption by maximizing the WCET of codels in low-priority tasks t ∈ Aff il [START_REF] Soetens | Realtime hybrid task-based control for robots and machine tools[END_REF]. ( 1) is simply the sum of the WCET of tasks t ∈ Aff ih \{t} and in (2) we add the WCET of the longest codel in tasks t ∈ Aff il , which gives us the following bound for any task t allocated to core C i :

WWT t ≤ Σ t ∈Aff ih \{t} WCET t + max t ∈Aff il l ∈1..|t | k∈1..|h j t l | (WCET c t kl ) (i neq. 5)
We sum WWT t with WCET t to upper-bound WCRT t (see ineq. 4). Finally, we state the schedulability test for HRT tasks ∀t ∈ τ h : WCRT t ≤ P t (ineq. 6). While pessimistic, this test is sufficient: if the maximum time a task t needs from its activation to its end is inferior than its deadline (period), then t is schedulable. We trade off optimism for sustainability: Burns and Baruah [START_REF] Burns | Sustainability in real-time scheduling[END_REF] show that RTA-based FP schedulability tests are sustainable in the sense that they remain valid even if some tasks manage to execute in less than their WCET.

B. Step Two: Formal Verification

If all HRT tasks in the G en oM3 system pass the schedulability test in step one, we may verify other -less critical -properties using SMC, otherwise we should redesign the system (Sect. IV). We automatize the generation of UPPAAL-SMC models by extending the template presented in [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF].

First, we make sure that the WCET computations, made with the help of UPPAAL (Sect. III-A), still hold in UPPAAL-SMC models. This is a simple proof. As shown in [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF], the only difference between UPPAAL-SMC and UPPAAL models is at the level of services, where non-deterministic edges may have custom probabilities. To give an example, let us get back to Fig 3 . In process Init, there are two edges out of location run_exec. In UPPAAL, these edges are equiprobable (chances to take one or the other are equal). In UPPAAL-SMC, one may use custom probabilities (that sum to one) on such edges, a mechanism which we exploited in [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF] to insert experiment-based probabilities. Now, w.r.t the computations made in Sect. III-A, this difference has no 1 impact since, for HRT tasks, we need to explore all paths anyway, no matter how big or small is the probability to take each of them. Second, we need to integrate the FP scheduler in the UPPAAL-SMC model and automatize it in the template. We show how this is done hereafter. a) Integrating the FP scheduler: We add a process C_i to handle the FP scheduling for each core C i on the robotic platform. Fig. 6 shows a generic example of such process, and how the managers processes are modified accordingly (we show only one manager). C _i has three locations: idle (the core is idle), decide (the core queue is dequeued) and busy (the core is being used). On the managers side (of each task in Aff i ), an intermediary location ask (the task is activated but still waiting to get the core) is added.

<' for {set k 1} {$k <= [length $Aff]} {incr k} { '> 2 <' if {[$t name] in [lindex $Aff $k]} { '> 3 <' set index $k '>
Core C i manager of task t (in Aff i ) Fig. 6: Integrating scheduler model C _i and the managers communicate as follows. The manager inserts (function enqueue()) the name of t in Q_i , the prioritized queue of C _i . On the edge idle → decide, C _i dequeues Q_i , and, depending on the dequeued value, updates the shared array of initially false Booleans allow_i, indexed with the names of tasks in Aff i (if the dequeued value is t , it turns allow_i[t] to true). At location decide, C i synchronizes with the manager of the only task t such that allow_i[t] = true (computed in the previous step), through the urgent channel give_i, which allows such manager to move to location manage (at which it starts executing a hyperjob) and moves C _i to location busy. C _i will then wait till the manager finishes executing the hyperjob and releases the core, which is done through the urgent channel free_i. Finally, the model handles also preemption, but this is not shown in this paper for space and readability reasons.

b) Automatization:

The programmer provides the affinity of cores Aff = {Aff 1 ..Aff m } as a Tcl list of lists. Listing. 2 shows how we generate the edge start → ask, in the manager process of task t in the system, in the UPPAAL .xta textual format. The for loop (lines 1-4) finds the i subscript of core C i to which t is allocated. Then, in line 7, the edge start → ask, with the right subscript for channel insert_i (in the synchronization block, keyword "sync"), is generated.

IV. RESULTS

We apply our approach to verify important properties on the drone navigation under a partitioned FP policy and the number of cores on the drone platform. The latter embeds an ODROID-C0 card featuring a four-core processor.

A. Step One

We comply with the notation given in Sect. III-A: m = 4 (number of cores), τ h = {main, comm, io, filter, control} (the set of HRT, i.e. high-priority tasks, those of the critical components MIKROKOPTER, POM and NHFC), τ l = {publish, plan, exec} (the set of low-priority tasks, those of components OPTITRACK and MANEUVER). Following the steps given in Sect. III-A1, we compute the actual WCET of all TU codels in the system and update such WCET accordingly, then compute the WCET of the five HRT tasks in the system (table. I). For each of the remaining three tasks, we identify the codel having the largest WCET (table. II). We recall tasks periods in table III IV).

An issue that arises is how to allocate tasks to cores. It stems from the bin-packing problem, known to be NPhard. In this paper, the way we allocate tasks is inspired by the first-fit decreasing heuristic. We start by allocating m high-priority tasks (in τ h ) to the m cores, then repeat until all tasks in τ h are allocated. Then, we do the same for low-priority tasks (thus allocation is by decreasing priority). The first-fit part is left to after running the schedulability test on HRT tasks (if such test fails). This allocation is not exactly what the original heuristic does, but in our case, it intuitively tends to reduce the WCRT of HRT tasks in the application. Indeed, such WCRT increases with the number of HRT tasks allocated to the core (ineq. 5), and so allocating first HRT tasks minimizes the maximum number of HRT tasks allocated to a core C i , upper-bounded by τ h /m . The (decreasing) affinity we start with is given in table IV.

We are now ready for schedulability analysis: we apply ineq. 5 (using the values from table. I and table. II) for each task t to upper bound WCRT t , then compare the latter with the period P t from table III (ineq. 6). The results (table V), show that all HRT tasks pass the schedulability test except for task io, whose WCRT is 80 µs larger than its period.

At this point, we may try to change the affinity without modifying the decreasing pattern (no more than two HRT tasks per core). Here, the generecity of the approach in Sect. III-A1a allows us to reason only using the timing constraints from tables I and II, which remain valid regardless of the chosen affinity. We notice that, by permuting the allocation of low-priority tasks publish and plan, all HRT tasks pass the schedulability test (table. VI). This new affinity guarantees schedulability for all HRT tasks in the system (table. VII) and will be thus the basis of step two.

B. Step Two

We generate, from the affinity in table VI, the number of cores and the G en oM3 system, an UPPAAL-SMC model.

In the latter, schedulability for HRT tasks (Sect. IV-B), is guaranteed by construction (step one). Now, using UPPAAL-SMC, we guarantee, up to a high probability, that low-priority tasks never starve, a less critical, yet important property (Sect. II-B1). To do so, we reason as follows. We know that in any task manager (Fig. 4), location manage denotes that a hyperjob is being executed. Thus, the absence of starvation means that (i) location manage is reachable and (ii) whenever it is reached, location manage is eventually left (back to location start). (i) is a reachability property while (ii) is a leadsto property which UPPAAL-SMC does not support. This is a limitation of the tool and not intrinsic to SMC.

Fortunately, there is a simple workaround if we augment the manager model (Fig. 4) with a clock x that is reset to 0 whenever any location is left. Thus, if the value of x is upper-bounded, then manage (i) is reachable (otherwise x would be unbounded at start or ask) and (ii) eventually left (otherwise x would be unbounded at manage), which corresponds to the same (i) and (ii) above. We may thus transform the two-step reachability-leadsto property into a safety property as we query the UPPAAL-SMC verifier to estimate the probability of x being bounded by value max_x, e.g. for task plan: Pr[≤ b]([]manager_plan.x ≤ max_x) (with b being a time bound for SMC simulations). We call prob t the probability of satisfying this property by a task t . We set the statistical parameters to a high confidence (α = 0.02) and precision ( = 0.002), which means that the highest probability we can obtain for prob t is 99.8% ± i.e. prob t ∈ [0.996, 1] with a confidence 100% -α = 98%. For each task t , we set max_x to P t and raise it until such highest probability is reached. Table VIII gives the results for all low-priority tasks. In sum, all low-priority tasks are starvation-free with a 99.8% probability as soon as x_max = 7 ms. UPPAAL-SMC takes up to 25 minutes to verify each property, a value that grows exponentially if we try to tighten the precision further: with tending toward zero SMC tends toward classical model checking and thus scalability is threatened as we noticed in [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF].

C. Discussion

We prove, with certainty, the schedulability for all HRT tasks in the application, while proposing a scheduling policy on the drone platform. Also, we prove with a high probability that low-priority tasks never starve for cores. Thus, considering the real robotic platform and the affinity and scheduling algorithm we propose, the G en oM3 system of the drone guarantees the latter does not crash because HRT constraints are not met, and is highly likely to fulfill its navigation missions (Sect. II-B1).

However, it is possible, for other applications, that step one (Sect. III-A) is not conclusive, that is we fail to find an affinity that allows all HRT tasks to pass the schedulability tests. In this case, we may consider redesigning the application by e.g. changing the periods, which is however not always feasible because periods may be dictated by hardware constraints (e.g. sensor frequency).

V. RELATED WORK

A. Rigorous Verification of Real-Time Robotic Applications

Popular robotic environments like ROS [START_REF] Quigley | ROS: an open-source Robot Operating System[END_REF] are not suitable for real-time applications [START_REF] Maruyama | Exploring the performance of ROS2[END_REF]. This is one consequence of the hard research problem of verifying time-constrained robotic systems. Schedulability analysis and formal methods have been explored to tackle this problem.

One of the main issues hindering the use of schedulability analysis is the generalization of tests to robotic task models [START_REF] Gobillot | A design and analysis methodology for component-based real-time architectures of autonomous systems[END_REF]. Some robotic software initiatives try to tackle this issue [START_REF] Soetens | Realtime hybrid task-based control for robots and machine tools[END_REF], [START_REF] Schlegel | Design abstraction and processes in robotics: From code-driven to model-driven engineering[END_REF], [START_REF] Gobillot | A design and analysis methodology for component-based real-time architectures of autonomous systems[END_REF]. In particular, MAUVE [START_REF] Gobillot | A design and analysis methodology for component-based real-time architectures of autonomous systems[END_REF] supports specification, implementation and analysis of realtime constraints. However, such initiatives focus on schedulability analysis and thus leave important properties such as reachability and bounded response unattended.

On the other hand, a major challenge of using formal verification is bridging robotic software, not formally founded, with formal methods. Proposed solutions range from ad-hoc non-reusable formalization [START_REF] Kim | Formal construction and verification of home service robots: A case study[END_REF], [START_REF] Molnar | System verification of autonomous underwater vehicles by model checking[END_REF] to formal frameworks for robotics [START_REF] Miyazawa | Automatic property checking of robotic applications[END_REF]. Another difficulty is the lack of scalability of exhaustive verification techniques due to the complexity and size of robotic systems. Non-exhaustive techniques such as SMC, used in [START_REF] Hazim | Testing, verification and improvements of timeliness in ROS processes[END_REF], are not suitable for critical applications where schedulability of HRT tasks must be verified with certainty. Besides, to the best of our knowledge and except for our efforts (Sect. V-B), the literature on formal verification in robotics (including works cited here) ignores hardware and OS scheduling constraints, which restricts the results validity to the unrealistic assumption of all tasks running in parallel at all times.

B. Our previous work

In [START_REF] Foughali | Toward a correct-and-scalable verification of concurrent robotic systems: insights on formalisms and tools[END_REF], [START_REF] Foughali | On reconciling schedulability analysis and model checking in robotics[END_REF], [START_REF] Foughali | Bridging the gap between formal verification and schedulability analysis: The case of robotics[END_REF] we proposed automated support to verify various properties of robotic applications under different scheduling policies by means of model checking. Such support is not suitable for the drone navigation application because of scalability issues. In [START_REF] Foughali | Statistical model checking of complex robotic systems[END_REF], we proposed an automated approach based on SMC to verify, up to a high probability, a number of properties. This approach is not suitable either for the drone system because SMC guarantees are not enough for critical properties such as the schedulability of HRT tasks.

C. Comparison to related work

In this paper, we combine both schedulability analysis and formal verification to achieve a rigorous verification of complex robotic systems. Unlike related work, we cover both schedulability and other important properties, while taking into account hardware and OS constraints, on robotic systems that do not scale with model checking. Furthermore, we provide an automated support to enable using our approach with no prior of either schedulability analysis or formal verification.

VI. CONCLUSION

We describe an automated two-step approach to rigorously verify complex (mixed-) critical robotic applications. It combines schedulability analysis and formal verification and is suitable for robotic applications that do not scale with model checking. Our approach is automated for nonexpert users and validated on a real drone case study.

We give two examples of future work directions. First, as said in Sect. IV, UPPAAL-SMC does not support leadsto properties and nesting operators in general. Though we often find alternatives to formulate the properties we want to verify, this limitation may be disabling for non experts. We are investigating strengthening our approach with automated modeling in BIP-SMC [START_REF] Mediouni | SBIP 2.0: Statistical model checking of stochastic real-time systems[END_REF], supporting full Bounded LTL and Weighted MTL logics with nesting. Second, the "global memory" FIFO spinlock that we borrow from MSRP leads to a loss in parallelism (Sect. III-A1a). We are working on a new shared-memory-locking algorithm inspired from group locks [START_REF] Block | A flexible real-time locking protocol for multiprocessors[END_REF], where locking overheads need to be carefully considered.

Fig. 1 :Fig. 2 :

 12 Fig. 1: A generic G en oM3 component.

Fig. 3 :

 3 Fig. 3: Simplified UPPAAL model of task main in component MIKROKOPTER. Process

<' lappend wcets_max $max_wcet '> 13 <' } '> 14 <Listing 1 :

 13141 ' } '>The list is <"[lreverse [lsort wcets_max]]"> Generating largest WCET of TU codels per task. and outputs the rest as is. Line 4 excludes task t , and line 8 conditions considering codel c only when it is TU through the non-emptiness of the field [$c mutex], a ready-to-use list containing all codels in conflict with c. The last line

Fig. 4 :

 4 Fig. 4: Modified process of Apply for WCET task computation.

Fig. 5 :

 5 Fig. 5: hyperjob model.

4 < 8 ... Listing 2 :

 482 ask {guard tick_<"[$t name]">; sync insert_<"$index">; assign tick_<"[$t name]">:= false;}, Generating an edge for manager of task t .

  .

	HRT task	WCET (ms)
	main	0.51
	comm	0.47
	io	0.68
	filter	0.55
	control	0.52

TABLE I :

 I WCET of HRT tasks.

	Task	WCET of longest codel (ms)
	publish	0.3
	plan	0.4
	exec	0.4

TABLE II :

 II Longest-codel WCET in low-priority tasks.

TABLE III :

 III Tasks periods.

	Core	Affinity
	C 1	{main, comm}
	C 2	{io, plan}
	C 3	{filter, publish}
	C 4	{control, exec}

TABLE IV :

 IV Initial affinity.

	HRT task	WCRT (ms)
	main	0.98
	comm	0.98
	io	1.08
	filter	0.85
	control	0.92

TABLE V :

 V WCRT of HRT tasks considering the initial affinity (table

TABLE VI :

 VI New affinity (by permuting tasks in blue in the initial affinity in tableIV).

	HRT task	WCRT (ms)
	main	0.98
	comm	0.98
	io	0.98
	filter	0.95
	control	0.92

TABLE VII :

 VII WCRT of HRT tasks considering the new affinity (table VI).

TABLE VIII :

 VIII Verification results (step two).

In this case, there is an additional operation: V is assigned to the service status in tab_t to prevent t from executing it again at its next period.


Remun Koirala

Benoît Denis

Bernard Uguen

Davide Dardari

Henk Wymeersch

Simultaneous Localization and Mapping in Millimeter Wave Networks with Angle Measurements

Keywords: SLAM, loopy belief propagation, data association

In this paper we propose a belief propagation (BP) based simultaneous localization and mapping (SLAM) approach suitable for millimeter wave (mm-Wave) networks. This approach leverages angle of arrival (AoA) and angle of departure (AoD) information with respect to multiple scatterers. Considering measurements from multiple base stations (BSs) and scatterers, seen as multiple sources, we solve out the data association problem from a centralized BP perspective, while jointly estimating the positions of both the mobile and scatterers. Simulations show that the proposed approach outperforms conventional distributed BSwise BP methods in terms of estimation accuracy.

I. INTRODUCTION

With the increasing traffic congestion in the microwave frequency band, the interest has been burgeoning towards exploring the yet underused large bandwidths available in the millimeter band spanning from 30GHz to 300GHz [START_REF] Rappaport | Millimeter wave mobile communications for 5G cellular: It will work![END_REF]. However, at such high frequency, the transmission suffers from high path loss, further signal attenuation caused by environmental factors (e.g., rain, fog) and even more importantly, high susceptibility to blockages [START_REF] Al-Ogaili | Millimeter-wave mobile communications for 5G: Challenges and opportunities[END_REF], [START_REF] Niu | A survey of millimeter wave communications (mmwave) for 5G: opportunities and challenges[END_REF]. In order to combat such effects, millimeter wave (mm-Wave) systems utilize a large number of antennas to concentrate the signal power in a particular direction with beamforming [START_REF] Sun | MIMO for millimeter-wave wireless communications: beamforming, spatial multiplexing, or both?[END_REF].

The advantages of exploiting a large bandwidth and a large number of antennas at both transmitter and receiver however are pertinent not only to mm-Wave communications but also to localization [START_REF] Bartoletti | 5G localization and context-awareness[END_REF]. These features allow for high temporal and angular resolution, enabling accurate delay and angle (angle of departure (AoD) and angle of arrival (AoA)) estimation. In addition, the mm-Wave propagation channel is sparse by nature meaning that there are only few multipath components. Consequently, in mm-Wave system, it is possible to estimate the delays, AoAs and AoDs of the main multipath components [START_REF] Abu-Shaban | Error bounds for uplink and downlink 3D localization in 5G millimeter wave systems[END_REF]. Thus, one can leverage the location-dependent information conveyed by each component to aid the localization process [START_REF] Mendrzik | Harnessing NLOS components for position and orientation estimation in 5G millimeter wave mimo[END_REF]. Beyond, knowing the positions of the scatterers generating these multipath contributions, in addition to localizing the user, offers a unique opportunity to map the physical environment.

With regards to tracking the location dependent variables of both line-of-sight (LOS) and non line of sight (NLOS) components, the authors in [START_REF] Shahmansoori | Position and orientation estimation through millimeterwave MIMO in 5G systems[END_REF] and [START_REF] Shahmansoori | Tracking position and orientation through millimeter wave lens MIMO in 5G systems[END_REF] present an estimator, exploiting the mm-Wave channel sparsity, relying on simultaneous orthogonal matching pursuit (SOMP) and support detection (SD) algorithms. Similarly, the authors in [START_REF] Ulmschneider | Multipath assisted positioning in vehicular applications[END_REF] and [START_REF] Gentner | Positioning using terrestrial multipath signals and inertial sensors[END_REF] present an algorithm for simultaneous localization and mapping (SLAM) based on the multiple location estimates of the user and the scatterers at different time instances. In [START_REF] Mendrzik | Joint localization and mapping through millimeter wave MIMO in 5G systems[END_REF], the authors present a message passing based solution for estimating the position and orientation of the user and position of the scattering point in both presence and absence of LOS components. The authors show that even in the absence of LOS path, the position of the scatterers can be reliably estimated. Likewise, in [START_REF] Frohle | Cooperative localization of vehicles without inter-vehicle measurements[END_REF], the authors provide a belief propagation (BP) based approach to track features in the environment in a dynamic vehicular scenario. The authors in [START_REF] Williams | Convergence of loopy belief propagation for data association[END_REF] propose a BP based algorithm to solve the data association problem (associating measurements to the correct source) and present a low complexity implementation of the corresponding solver. Common to all methods that rely on time-based measurements is the need for tight synchronization [START_REF] Mendrzik | Joint localization and mapping through millimeter wave MIMO in 5G systems[END_REF], [START_REF] Koivisto | Joint device positioning and clock synchronization in 5g ultra-dense networks[END_REF]. Localization using only angular information avoids this bottleneck. Cooperative localization using only AoA information was proposed in [START_REF] Wu | Cooperative localization with angular measurements and posterior linearization[END_REF]. Similarly, in [START_REF] Wielandt | Indoor multipath assisted angle of arrival localization[END_REF], the authors investigate indoor localization with only AoA measurements.

In this paper, we present a BP based SLAM approach in order to jointly localize the user and the scatterers relying only on angle measurements, without a-priori knowledge of the positions of either the user or the scatterers. In the process, we also solve the data association problem concerned with the measurements and their corresponding sources 1 . The processing is done in a centralized way without needing to send the measurements to each base station (BS), in contrast to more conventional distributed BP approaches [START_REF] Frohle | Cooperative localization of vehicles without inter-vehicle measurements[END_REF]. One major motivation for adopting a centralized approach in the very context lies in its lower communication overhead. The distributed method indeed requires sharing of particle clouds among the different BSs, while our method just requires sharing of raw measurements and estimates.

II. SYSTEM MODEL

Consider a 2 dimensional (2D) scenario with N BSs and a single user as illustrated in Fig. 1. The positions of the BSs are assumed to be known, located at x 1 , x 2 , • • • , x N in a common coordinate system. Likewise, the user is assumed to be positioned at s 0 with a known orientation 2 α. In the scenario, we also assume L scattering points (and hence L + 1 total possible paths between a BS and the mobile user), each with positions s 1 , s 2 , • • • , s L . Both the positions of the user and the scatterers are unknown. Contrarily to [START_REF] Mendrzik | Harnessing NLOS components for position and orientation estimation in 5G millimeter wave mimo[END_REF] (where range measurements are also considered), here we assume that each BS i can measure the AoD and AoA pair of Li different paths 3 . We also assume that L is known, there are no false alarms 4 , i.e. Li ≤ L + 1, and the measurements can be in any order with respect to the L + 1 total paths.

Z (i) = [z (i) 1 , • • • , z (i) l , • • • , z (i) Li ], (1)
where l ∈ {1, 2, • • • , Li } denotes the measurement index of ith BS corresponding to a set of estimates of AoD ( θ) and AoA ( φ). We also assume that we have the measurement covariance matrix (Σ

(i)
l ) corresponding to the measurements of AoD and AoA between the i-th BS and the l-th scatterer. 2 For simplicity, we consider that the orientation of the user is known. The absolute heading can be extracted from some orientation estimators, for instance, inertial measurement unit (IMU) and magnetometer in the mobile phone [START_REF] Ulmschneider | Multipath assisted positioning in vehicular applications[END_REF].

3 Note that it is not necessary that a BS has AoD and AoA measurements corresponding to every path in the system. Hence, we use different notations for the total number of paths (L) and the total number of paths measured by the i-th BS ( Li ). 4 This consideration excludes the possibility of any measurements not associated with the user, N BSs and L scatterers. For the problem formulation including the possibility of false alarm, see [START_REF] Williams | Convergence of loopy belief propagation for data association[END_REF].

We consider that all the measurements z (i) l are independent. Mathematically,

z (i) l = [ θ(i) l , φ(i) l ] ∼ N [θ (i) l , φ (i) l ] T , Σ (i) l . ( 2
)
The measurements for all the N BSs can be grouped together as Z = [Z (1) ,

• • • , Z (N ) ].
The main objective of this paper is to determine the positions of the user and that of all the scattering points from angle measurements, and thus the main task is to calculate the posterior distribution p(s k |Z), where k ∈ {0, 1, • • • , L}. However, since the order of the measurements at each BS is random, in the process of calculating the posterior distribution, we also need to solve the data association problem, where we associate each measurement with the corresponding path.

III. FACTOR GRAPH FORMULATION A. Data Association Auxiliary Variables

For the purpose of data association, following a similar approach to [START_REF] Frohle | Cooperative localization of vehicles without inter-vehicle measurements[END_REF], we introduce the sets

M = ⊗ N i=1 {1, • • • , Li } with its cardinality P = N i=1 Li , a k ∈ M and b m ∈ {0, 1, • • • , L}, ∀m ∈ M.
Each element of the set M, referred to in this paper as a measurement vector, is a vector of length N containing all the possible permutations of measurement indices; a k indicates which measurement vector corresponds to the source k. Reciprocally, b m indicates which source corresponds to a measurement vector. Both a and b can be mapped one-to-one, meaning that the knowledge of either of the variables is sufficient to know the other. Mathematically, this relation is expressed as

ψ(a k , b m ) = 0 a k = m, b m = k or a k = m, b m = k, 1 otherwise.
(3) Contrary to [START_REF] Frohle | Cooperative localization of vehicles without inter-vehicle measurements[END_REF], where the data association is performed in a distributed way at each BS, we assume that the association in our case is done in a centralized way and hence, unlike in [START_REF] Frohle | Cooperative localization of vehicles without inter-vehicle measurements[END_REF], the association variable a in our work is not scalar.

B. Factor Graph of Joint Distribution

Our objective is to find the marginal probability of s k while also sorting out the data association problem. We have a posterior distribution formulation as follows:

p(s 0:L , a, b|Z) ∝ p(Z|s 0:L , a, b)Ψ(a, b) L k=0 p(s k ), (4)
where, p(s k ) is the prior distribution on the position of the sources, a and b contain all the association variables a k and b m , and ψ(a, b) can be formulated similarly to [START_REF] Frohle | Cooperative localization of vehicles without inter-vehicle measurements[END_REF], [START_REF] Williams | Convergence of loopy belief propagation for data association[END_REF] from (3):

Ψ(a, b) = L k=0 m∈M ψ(a k , b m ). (5)
The measurement likelihood p(Z|s 0:L , a, b) can be formulated as:

p(Z|s 0:L , a, b) = N i=1 p(Z (i) |s 0:L , a, b), (6a)
∝ L k=0 N i=1 p z i [a k ]i |s 0 , s k , (6b)
∝ L k=0 v(a k , s 0 , s k ). (6c)
where, the expression v(a k , s 0 ,

s k ) = N i=1 p z i [a k ]i |s 0 , s k represents the joint AoD-AoA distribution considering all the BSs and p z i [a k ]i |s 0 , s k is Gaussian distributed, as per (2): p(z i [a k ]i |s 0 , s k ) ∝ exp -[ θ(i) [a k ]i , φ(i) [a k ]i ] -h(s 0 , s k ) Σ (i) [a k ] i , (7)
where ||x|| A = x T Ax and h(s 0 , s k ) is a nonlinear function transforming the location of the user s 0 in the case of direct path and both the user s 0 and the scatterer s l in the case of non-direct path to the corresponding AoD and AoA variables. Note that from equation (6b), one does not have the dependence on b, as the equation (6a) is conditioned on the knowledge of both a and b and since a and b are injective-only, knowing one is enough to recover the other. The corresponding factor graph of the posterior distribution is given in Fig. 2.

IV. MESSAGE PASSING VIA BP A. BP for Marginalization

We find the marginal p(s k |Z) using the BP message passing algorithm on the factor graph [START_REF] Kschischang | Factor graphs and the sum-product algorithm[END_REF], starting from the root nodes p(s k ) to the leaf node 5 . BP proceeds by passing messages between variables and factors defined by µ v→f (v) and µ f →v (v), respectively, where v is a variable and f is a factor. The marginal p(s k |Z) can then be found as

p(s k |Z) ∝ µ s k →f (s k ) × µ f →s k (s k ), (8)
for any connected factor f . 5 Note that the factor graph in Fig. 2 consists of loops in between the variables a and b. In such loopy cases, BP can still be used by passing the messages until the latter converge. Even though such convergence can not be guaranteed, it has been shown that this kind of method often arrives at a reasonable estimate [START_REF] Ihler | Loopy belief propagation: Convergence and effects of message errors[END_REF].

B. Message Passing Schedule

We now show the message passing steps from the root nodes f k through the nodes back to the leaf node f k . The root node f k or p(s k ) contains the a-priori distribution of the position of s k . In the following, we consider the indices 1 ≤ k ′ ≤ L and 0 ≤ k ≤ L. 1 In the first step, we pass the a-priori distributions to the corresponding position variables.

µ f k →s k (s k ) = f k (s k ). (9)
2 In the second step, we have no message from µ v k →s0 yet, so we initialize µ v k →s0 = 1, ∀k. Hence, the messages from s k to v k can be written as:

µ s0→v k (s 0 ) = f 0 (s 0 ) L k ′ =k µ v k ′ →s0 (s 0 ) = f 0 (s 0 ), (10a) µ s k ′ →v k ′ (s k ′ ) = f k ′ (s k ′ ).
(10b) 3 Next, we compute the outgoing messages from the factor node v k to the variable node a k .

µ v0→a0 (a 0 ) = v(a 0 , s 0 )µ s0→v0 (s 0 ) ds 0 (11a) µ v k ′ →a k ′ (a k ′ ) = v(a k ′ , s 0 , s k ′ )µ s k ′ →v k ′ ds k ′ ds 0 . (11b)
From equation (6c), we can see that v k is already formulated as the product of distributions over all the BSs. Hence, in this step, the messages can be passed in a centralized way, unlike in [START_REF] Frohle | Cooperative localization of vehicles without inter-vehicle measurements[END_REF] where the factor graph is formulated in such a way that the messages need to be passed through each BS separately. 4 Then, we move the message forward to the data association loop. For notational simplicity, we represent the factor node ψ(a k , b m ) by ψ k,m . We start by initializing the messages µ (0)

ψ k,m →a k (a k ) = 1.
We can then execute multiple iterations. The message in the p-th iteration can be written as [START_REF] Williams | Convergence of loopy belief propagation for data association[END_REF]:

µ (p) a k →ψ k,m (a k ) = µ v k →a k (a k ) m ′ =m µ (p-1)
ψ m ′ ,k →a k (a k ), (12a) µ (p) ψ k,m →bm (b m ) = a k ψ k,m µ (p) a k →ψ k,m (a k ), (12b)
µ (p) bm→ψ k,m (b m ) = k ′ =k µ (p) ψ k ′ ,m →bm (b m ), (12c)
µ (p) ψ k,m →a k (a k ) = bm ψ k,m µ (p) bm→ψ k,m (b m ).
(12d) 5 After the data association loop, we have the message from a k to v k as:

µ a k →v k (a k ) = m µ ψ k,m →a k (a k ). ( 13
)
The next step is to calculate the messages µ v k →s k (s k ) and µ v k ′ →s0 (s 0 ). We omit argument for space reasons:

µ v0→s0 (s 0 ) = a0 v(a 0 , s 0 )µ a0→v0 (a 0 ), (14a)
µ v k ′ →s0 (s 0 ) = a k ′ v k ′ µ a k ′ →v k ′ µ s k ′ →v k ′ ds k ′ , (14b) µ v k ′ →s k ′ (s k ′ ) = a k v k ′ µ a k ′ →v k ′ µ s0→v k ds 0 , (14c)
where, µ s0→v k (s 0 ) = a0 v(a 0 , s 0 )µ a0→v0 (a 0 )ds k ′ . 6 Finally, the posterior beliefs can be computed as:

p(s 0 |Z) ∝ µ f0→s0 (s 0 ) k µ v k →s0 (s 0 ) (15a) p(s k ′ |Z) ∝ µ f k ′ →s k ′ (s k ′ )µ v k ′ →s k ′ (s k ′ ). (15b)

C. Particle Implementation

As the integrals in the previous section cannot be solved in closed form, we approximate them using Monte Carlo integration. Thereby we represent the messages as lists of weighted particles. We have to consider that the number of particles are enough to provide an accurate representation of the probability distributions and the weights are normalized such that their sum is 1. To compute the products in (15a)-(15b), we evaluate all messages only in the particles generated from the priors.

D. Centralized vs Distributed Approach

For benchmark purposes, we compare our proposed method against a distributed BS based SLAM method equivalent to that in [START_REF] Frohle | Cooperative localization of vehicles without inter-vehicle measurements[END_REF] 6 . For the distributed method, we introduce the set M i = {1, 2, • • • , Li }, ∀i for each i-th BS. We define a k,i m i ∈ M i indicating which measurement m i corresponds to the source k at the i-th BS. Similarly, we define b mi,i k ∈ {0, 1, • • • , L} defining which source corresponds to the measurement m i at the i-th BS. Note that contrarily to a k , b m and m in our proposed centralized methods, in this distributed method, a k,i , b mi,i and m i are all scalars and the relation between a i and b i , the vector of data association variables, is in fact bijective. We further define

Ψ(a, b) = N i=1 Li k=0 mi∈Mi ψ(a k,i , b mi,i ). (16)
where,

ψ(a l,i , b mi,i ) = 0 a k,i = m i , b mi,i = k or a k,i = m i , b mi,i = k 1 otherwise. (17)
Hence, following a formulation similar to the posterior distribution as (4), we can build a factor graph as illustrated in Fig. 3. We can compute the beliefs and accordingly the marginal similarly to the the previous section.

notational convenience, v k,i represents v(a k,i , s 0 , s k ) and ψ k 1 ,k 2 = ψ(a k 1 ,i , b k 2 ,i ) ∀i.

V. NUMERICAL RESULTS

In this section, we describe the simulation setup and parameters and then show the simulation of our proposed method. To benchmark our result, we then compare with a model inspired by the distributed BP approach in [START_REF] Frohle | Cooperative localization of vehicles without inter-vehicle measurements[END_REF].

A. System parameters and simulation setup

We consider a scenario with N = 3 BSs, L = 2 scatterers and a user where all the BSs can measure all three paths (i.e. Li = 3, ∀i). We consider the locations of BSs are known with x 1 = [0, 0], x 2 = [0, 100], x 3 = [100, 100], whereas the user and the scatters are uniformly distributed within an area of 100 m × 100 m area.

We assume that the measurement covariance matrix is a diagonal matrix with the variance of estimating AoD σ 2 θ equal to the variance of estimating the AoA σ 2 φ for all the measurements. Similarly, while simulating the BP algorithm, we consider N s0 = N s k ′ = 2500 particles (50 per dimension) to represent the distributions of the user and the scatterers.

In our simulations, we assume no prior knowledge of the positions of either the user or the scatterers and hence, we consider they are uniformly distributed within the deployment area. Hence, to replicate p(s 0 ) as particles, we can draw N s0 sample points of s 0 from the specified domain and assign the corresponding probability as weights, in this case a constant (and accordingly for p(s k ′ )).

B. Numerical results and discussion

In Figs. 4 and5, we plot the marginal distributions of the user and the scatterers with blue and orange scatter points, as formulated in equations (15a) and (15b) respectively. Since, as said earlier, we are dealing with particles rather than the continuous distribution, the size of blue and orange circles represents the weights associated with the corresponding particles. We also plot the true positions of the BSs, the scatterers and the user for comparison. Between the two figures, we can clearly see that the particle clouds in our proposed method can separate the two scatterers and the user unlike the distributed BP. The reason is that in our method, as we can deduce from equation (6b), only the particles with non zero probabilities according to equation ( 2) with respect to all the BSs are passed on from the factor v to the variable a in the factor graph. Hence, in this step, before the data association loop, we do some sort of initial filtering with respect to all the BS. On the contrary, in the distributed method, the filtering is done with respect to only one single BS before the data association loop, and then further filtering is done later during the collection while passing the message from v k to s k . Filtering before the loop reduces the propagation of any error during the data association loop.

Following this discussion, in Fig. 6, we plot the empirical cumulative distribution function (CDF) of the root mean squared error (RMSE) between the true and estimated posi- tions of the user and scatterers. We calculate the RMSE by taking the distance between the true and the mean particle position. As we can see, the proposed centralized method performs better than the distributed method especially when it comes to estimating the position of the scatterer due to the limited error propagation in the data association phase.

Comparing the communication overhead between the two approaches, the main difference lies in the fact that in the distributed method, the message between the variable node s k and the factor node v k,i involves exchanging clouds of particles representing the distribution of all the scatterers to and from all the BSs. The overhead cost of such message communication is very high. In contrast, in the proposed centralized method, the only message exchange from the different BSs include the raw AoD and AoA measurement pairs to the centralized unit which is much smaller than the previous.

Regarding the complexity analysis between the two approaches, in the distributed method, we pass O N L 2 messages, while in the proposed centralized approach O L N +1 messages. Hence, the centralized approach has better performance and low communication overhead, but at a higher complexity cost. The distributed method exhibits less complexity, but requires exchange of particle clouds among BSs.

VI. CONCLUSIONS

In this paper, we proposed a BP based method to solve the problem of mm-Wave SLAM by using only angular measurements in a system with multiple BSs and scatterers and a user node. To reach this objective, we firstly formulated the corresponding posterior distribution and then the factor graph including the problem of data association. By running the message passing algorithm in the graph, numerical results demonstrated that even without any a-priori distribution on the positions of the user and the scatterers, one can achieve relatively high accuracy. In comparison with methods from the literature where the data association problem is solved in a distributed manner separately at different BSs, we show that our centralized data association approach provides a better estimation accuracy, mostly in terms of scatterers positioning. As a future work, we would like to consider a model including uncertainty in the user orientation and false alarms, which would provide an even more realistic assessment of the problem.

Fig. 1 .

 1 Fig. 1. Example system model with 3 BSs positioned at x 1 , x 2 and x 3 and 1 user positioned at s 0 with orientation α along with two scatterers at s 1 and s 2 and the AoD and AoA of the LOS paths with respect to BS1.

Fig. 2 .

 2 Fig. 2. Factor graph representation of the posterior distribution in equation (4). In the graph, we have introduced short form notation f k to represent p(s k ), v k to represent v(a k , s 0 , s k ) and mp, p = 1, • • • , P represents the p-th element of the set M. The factor and variable nodes are represented inside squares and circles respectively.

Fig. 3 .

 3 Fig.3. Factor graph with distributed BP for performance comparison. For notational convenience, v k,i represents v(a k,i , s 0 , s k ) andψ k 1 ,k 2 = ψ(a k 1 ,i , b k 2 ,i ) ∀i.

Fig. 4 .

 4 Fig. 4. Marginal distribution with σ 2 θ = σ 2 φ = 1 deg 2 with the proposed method. The diamonds, squares and circle represent the true positions of the 3 BSs, 2 scatterers and the user respectively.

Fig. 5 .

 5 Fig. 5. Marginal distribution with σ 2 θ = σ 2 φ = 1 deg 2 with the distributed method [13]. The diamonds, squares and circle represent the true positions of the 3 BSs, 2 scatterers and the user respectively.

Fig. 6 .

 6 Fig. 6. CDF plot comparison of the RMSE error between the proposed centralized and the distributed BP based methods with 1 deg 2 variance.

The term "source" can refer to either the user or the scatterers.

In the literature, it is common to consider such distributed methods especially for the data association problem[START_REF] Williams | Convergence of loopy belief propagation for data association[END_REF],[START_REF] Meyer | Message passing algorithms for scalable multitarget tracking[END_REF]

ACKNOWLEDGMENT

This work was supported, in part, by the European H2020 project SECREDAS, which is funded through the specific ECSEL Joint Undertaking research and innovation program (GA No. 783119), and by the Swedish Research Council under grant No. 2018-03701.


Drawing on Elias Canetti's classic Crowds and Power [1] , Claire Jowitt notes how much the figure of the captain ruling the seas has provided a "powerful collective vision and symbol" of English self-identity over the past few centuries. Such has been the case at least since the time of the great Elizabethan explorers and privateers like Martin Frobisher, Francis Drake, or Thomas Cavendish [2] .

But captain among captains to the point of being more commonly referred to by that title than by his first name, James Cook stands out as possibly the most enduring embodiment of that national, imperial, and colonial stereotype of seaborne heroic manhood. "Bestriding the European map of the Pacific like a colossus" in the words of Nigel Rigby [3] , Cook the master navigator holds a controversial position in the history of the making of that map. On the one hand, his name glorifies British exploits in a golden age of scientific discovery, artistic achievement, and imperial expansion, but on the other hand, he also stands for a potent symbol of the territorial dispossessions and colonial ideology that followed in the wake of his voyages of exploration.

Revisiting Cook and his protean legacy 250 years after the first of his three Pacific voyages therefore implies primarily to pause and reflect on a complex British imperial past which has resulted in a challenging present. It also implies to reassess our very practices of remembering and rewriting narratives of what the eighteenth century viewed as "Enlightenment", a memorial operation which is about "making a present of the past" or "performing" it in the anthrohistorical sense given to that term by Greg Dening [4] . Considering Cook's legacy from the vantage point of continental Europe allows this special issue of the journal Astrolabe and the Paris conference which was its starting point to approach it in a more dispassionate way perhaps than other initiatives around the globe over the past few months, which diversely honoured or denounced the explorer's epoch-making cross-cultural

encounters. Yet even in viewing Cook from our supposedly more objective outsiders' angle, we too need as inheritors to the legacy of Bougainville or La Pérouse to remember how the story of the English and British challenge to the rival imperial powers of France or Spain was to some extent, in the sobering words of William Frame and Laura Walker, "a squabble among thieves over lands belonging to non-European peoples". In our journey with and along the legacy of Captain Cook, we are particularly grateful to the Hakluyt Society, under whose aegis Beaglehole published the first comprehensive, critical edition of the journals between 1955 and 1967. Engaging with our times' changing practices of commemoration around a controversial figure and a complex history, the Society has shown in its support to our project its readiness to ever encourage and endorse new critical approaches to both the methods and the results of the discovery voyages which it publishes.

  Introduction Captain Cook after 250 Years: Re-exploring the Voyages of James Cook (avril 2020) INTRODUCTION Captain Cook after 250 years: Re-exploring The Voyages of James Cook (Avril 2020) Introduction Ladan NIAYESH

  the complexity and diversity of approaches to Cook in our time rather than compromising over them, we have taken stock of the expertise of scholars from different geographical and methodological horizons, inviting them to engage in crosscultural and cross-disciplinary conversations in each of the four sections of this volume. The first section, entitled "Explorers and Conquerors", recontextualises Cook in his own time by looking at rival protagonists such as Joseph Banks in Anna Agnarsdóttir's contribution, concealed agendas such as the quest for the Northwest Passage in Pierre-François Peirano's article, and the explorer's early American followers studied by Dane Morrison. The second section, on "Transmissions and Translations" focuses on the diverse fortunes of Cook's journals, which had a journey of their own, from Hawkesworth's alterations to the manuscript of the first voyage analysed by Jean-Stéphane Massiani, to the uses of the journals as log-books in Odile Gannier's essay, and the repurposed early French translation of Démeunier critically reviewed by Antoine Eche. The third section, devoted to "Artistic Representations and Heritage", bridges the temporal gap between Cook's time and our own, with a transhistorical approach to the culture of knowledge and artistic dissemination surrounding Cook-related artefacts. Here, recent examples of museum exhibitions around Cook commemorations are critically evaluated by John Mullen, while John McAleer adopts a diachronic approach to evolving practices of display around landmark Cook collections. Giving the topic a visual edge, Vanessa Alayrac-Fielding considers the "reimaging" in our time of the colonial and scientific testimonies left by artists who embarked on each of Cook's three journeys. The fourth and final section, "James Cook Revisited", blows the postcolonial whistle in both Sandhya Patel's and Ben Ferguson's presentations of biographical debates on Cook in our time, from white New Zealander J. C. Beaglohole's quasi-hagiographic stance in the early 1970's to Sri Lankan Gananath Obeyesekere's openly postcolonial take and Barry Lopez's firing the first shots of what Cook can mean for the twenty-first century.

  Notes1. ^EliasCanetti, Crowds and Power, trans. Carol Stewart, New York and London, Continuum, 1962, p. 171-172. 2. ^Claire Jowitt, "The Hero and the Sea", XVII-XVIII, 74, 2017, http://journals.openedition.org/1718/888 (last accessed 17 April 2020). 3. ^Nigel Rigby, "'Men of Captain Cook': Pacific Voyages 1785-1803", in Captain Cook and the Pacific: Art, Exploration and Empire, ed. John McAleer and Nigel Rigby, New Haven, Yale University Press, 2017, p. 169. 4. ^Greg Dening, Performances, Carlton South, University of Melbourne Press, 1996, p. xiv. 5. ^William Frame and Laura Walker (eds.), James Cook: The Voyages, Montreal, McGill and Queen's University Press, 2018, p. 12. Ladan NIAYESH, « Introduction », Astrolabe [En ligne], Captain Cook after 250 years: Re-exploring The Voyages of James Cook (Avril 2020), mis en ligne le 24/04/2020, URL : https://astrolabe.msh.uca.fr/captain-cook-after-250-years-re-exploring-voyagesjames-cook-avril-2020/dossier/introduction

	Pour citer cet article:
	Référence électronique