Pierre Bieber

Frédéric Boniol

Youcef Bouchebaba

Julien Brunel

Claire Pagetti

Olivier Poitou

Thomas Polacsek

Luca Santinelli

Nathanaël Sensfelder

A model-based certification approach for multi/many-core embedded systems

This article presents the first year results of the PHY-LOG project that aims at providing a model-based certification framework for aeronautics systems designers when developing multi/many-core-based architectures. After a brief reminder of the certification objectives, we present an overview of the PHYLOG approach. We then detail two points of the methodology: (1) a certification oriented meta-model for multi-and many-core platforms, and (2) an interference prediction method based on this meta-model. This method is then illustrated on a sub-part of the many-core Kalray MPPA R -256.

I. INTRODUCTION

Certification activities consist in providing detailed documentation and justifications that explain why the development of a specific product is trustworthy and fulfills a given standard's requirements. Such a comprehensive documentation not only contains the results, but also the input data, the hypotheses, the techniques applied, etc. This process is well covered by the current aeronautics practices. However, for the next generation of multi/many-core-based architectures, the means of compliance will evolve due to architecture specifics.

A. Context

The last decade has seen the emergence of multi-core and many-core architectures, i.e. chips integrating several cores interconnected by either a shared bus (for multi-core processors) or a networks on chip (for many-core processors). Although these architectures may allow a huge gain in terms of performance, they also face important challenges to their integration in safety critical environments. As an example, due to the intensive resource sharing and lack of documentation, it is very difficult to ensure time predictability [WEE + 08], [START_REF] Wilhelm | Embedded systems: Many cores -many problems[END_REF], one of the key elements of certification expectation.

In order to tackle multi-core aeronautics certification-related issues, several projects have been funded. One of the first was MULCORS [START_REF] Jean | MULCORS-Use of Multicore Processors in airborne systems[END_REF] which clearly identified the need of changing and adapting the current certification standard. Since then, several attempts at precisely defining such new standard have been done, such as the Multi-core Certification Review Item (MCP-CRI) [START_REF]The Use of Multi-Core Processors in Safety-Critical Applications -CRI[END_REF], the CAST Position Paper #32 [START_REF]Position Paper on Multi-core Processors -CAST-32[END_REF], and the FAA white paper [JMR + 16].

B. Objectives

The objective of the article is to explore a model-based approach, to help both the applicant to answer the MCP-CRI requirements and the certification authority to assess the arguments provided by the applicant. Indeed, the standards mentioned previously describe high level requirements, but no means with which to ensure them nor ways to demonstrate the compliance of an integrated system (multi-core processor + applicative software). Thus, as is, the proposed approach does not intend to replace the MCP-CRI, but instead to offer a methodological framework to assist certitication. This work was done within the PHYLOG DGAC project and the results are those of the first year.

In previous works [BBD + 16], [START_REF] Polacsek | Validation, accreditation or certification: a new kind of diagram to provide confidence[END_REF], we proposed a model-based framework to simplify the certification of aeronautics systems, to cope with inflation of documentation, to improve the coverage of requirements, and to ease the use of formal methods as means of verification. In PHYLOG, we reuse and improve those ideas to specifically address multi/manycore issues.

In the sequel, we present the main objectives exposed by the new standards (section II). We present, in section III, an overview of the methodology developed during PHYLOG project. We then detail two points of the PHYLOG methodology: (1) a certification oriented modeling language for MCP platforms (section IV), and (2) an interference prediction method based on the formal modeling presented above. A detailed example on how to apply the modeling language and the interference prediction method is given in section VI.

II. REMINDER OF CERTIFICATION OBJECTIVES

The Multi-core Certification Review Item (MCP-CRI) [START_REF]The Use of Multi-Core Processors in Safety-Critical Applications -CRI[END_REF], also published as the CAST-32A position paper, provides a set of guidances for software planning and verification on multi-core chips, with a particular emphasis on timing considerations and error handling.

A. Main objectives of MCP-CRI

These guidances are structured in 5 high level objectives.

a) Software planning: According to this objective, the applicant shall provide a model of the multi-core architecture. He has to identify the specific processor, the number of active cores, the software architecture, the dynamic software features, etc. He also has to argue whether the platform provides robust partitioning or not. And finally he has to detail the methods and the tools used for the development and verification of all the software components hosted on the platform (including hypervisors and operating systems).

b) Planning and setting resources: The second objective deals with the final configuration (i.e., the stable configuration reached after the boot step). The applicant has to detail all the configuration settings, including the execution frequency of the activated cores, which of the peripheral devices are activated, how the caches, memories, and interconnects are configured and allocated, etc. Consequently, the applicant shall identify the shared resources and shall describe a usage domain for each of them (how the resources are shared and how to prevent resource capabilities from being exceeded). Complementarily, the applicant shall also argue that the critical configuration settings are static and are protected against inadvertent changes at run-time.

c) Interference Channels and resource usage: This is the main objective. Due to resource sharing, coupling exists at the platform level, which can cause interferences between the applications. These interferences can lead to unexpected delays or loss of data. In order to prevent potential unpredictable behaviors, the applicant has to identify all the interference channels in the final configuration, and he has to argue that they are properly mitigated by adequate means. Afterwards, the applicant shall argue that the resource demand does not exceed the resource availability in the final configuration (when taking into account the resource usage and the mitigation means).

d) Software verification: Due to interference channels, the applications hosted by a multi-core platform could suffer from unexpected delays. The applicant shall thus verify that all the software components (including the operating systems and hypervisors) operate correctly and do not miss any deadlines when running in parallel in the final configuration. The MCP-CRI distinguishes two cases: (a) either the platform provides robust partitioning mechanisms, or all the interferences are properly avoided or mitigated, then the verification and the timing analysis can be done for each application in isolation; (b) otherwise, the platform and all its application components have to be considered in the same verification step. In the latter case, the applicant is not allowed to proceed incrementally. e) Error detection and handling: Due to the complexity of executing in parallel several software components competing for the same resources, specific errors and failures may happen (e.g., memory violation). They need to be detected and handled at run-time. For that purpose, additional mechanisms may need to be developed and verified. This last objective requires the applicant to detail the error handling solution integrated in the platform (including the use of a safety net external to the multi-core chip), and to argue that all the errors and failure conditions are properly managed.

B. Refinement of the CRI objectives

Previous works have revisited the MCP-CRI certification objectives, in particular the timing interferences. The authors of [JMR + 16] propose more detailed definitions for interference channels, interference sources, and interference targets, and they propose a process to reduce the number of

Conf

Modeling the final configuration, i.e., modeling the platform, including the software and the hardware components, the additional mitigation means, the execution model, etc. The model shall describe normal and abnormal behaviors Interf1

Determining the interference channels, i.e., identifying all the residual interference channels while considering the additional mitigation means added to avoid or limit conflicts on shared resources Interf2

Arguing the interference channels are innocuous, i.e., arguing that the interference channels identified by objective Interf1 either never happen, have a negligible effect, or are upperbounded such that all the deadlines of all the software components are still satisfied and no data is lost Error Arguing errors and failures are managed, i.e., arguing that abnormal behaviors are properly mitigated by internal means or by an external safety net, including that the configuration settings are protected against inadvertent changes at run-time interferences. The aim of [START_REF] Agirre | On the Tailoring of CAST-32A Certification Guidance to Real COTS Multicore Architectures[END_REF] is to adapt the MCP-CRI certification objectives to COST MCP architectures. For that purpose, they group these objectives into three high level principles:

• Determining the final configuration: determining which configuration is the final one, and showing that it is protected against inadvertent changes at run-time; • Managing interference channels: identifying all the interference channels in the final configuration, defining the means to either avoid interference by design or to upper-bound them such that the deadlines of the software components are satisfied; • Verifying the use of shared resources: showing that the software components do not exceed the use of available resources. The idea of [START_REF] Agirre | On the Tailoring of CAST-32A Certification Guidance to Real COTS Multicore Architectures[END_REF] is that following these three high level principles should help answering the MCP-CRI objectives. We also follow this idea. In the PHYLOG approach, we intend to cover all the MCP-CRI objectives, including the safety concern. We extend this classification into four high level objectives, as shown in the table I. Our thesis is that answering these four objectives in a correct, complete, and consistent way should ease the providing of certification files compliant with the MCP-CRI requirements.

III. MODEL-BASED CERTIFICATION APPROACH: OVERVIEW

Following this thesis, the PHYLOG project aims at building a reference framework for the certification of multi-and many-core architectures. The goal is to formalize certification requirements and to provide a way to build coherent and readable augmentations. According to the classification table I, the framework and its associated methodology involve 3 steps:

1) a modeling step (answering Conf);

2) an analyzing step (answering Interf1);

3) an argumentation step (answering Interf2 and Error).

A. The modeling step

Providing a complete and consistent description of an architecture is the first certification issue. A common way to achieve this goal is to describe the equipment in a textual manner. However, such method lacks formalization and verification means. The first idea suggested by PHYLOG is to follow a formal language-based approach. The proposed language, called PML (for PHYLOG Modeling Language) shall offer the capabilities to model the fundamental concepts of multi/many-core processors involved in the MCP-CRI (e.g., shared resources, hardware configuration, interference channels, mitigation means, etc.). In that sense, it differs from other architecture languages such as AADL or SySML, for it is not a design oriented language, but a certification oriented language. PML is based on 4 concerns (depicted in the MCP-CRI):

1) hardware platform (e.g., cores, MMU, interconnect, etc.), 2) software platform (e.g., OS, hypervisor, etc.), 3) applicative software, 4) deployment.

To be able to fully support the users -both the industrial applicant and the certification authority -, we need reasoning capabilities on this high level language. To this end, PML is translated to a logical framework, called WEIRD [BBD + 16], that offers the expected reasoning capabilities.

PML, WEIRD, and the PML implementation in WEIRD are presented in section IV.

B. Interference prediction and interference analysis

As said previously, interferences between applications are one of the main concerns of the MCP-CRI. The certification objective Interf1 requires the ability to predict all the possible interferences in the final configuration, and to show that they are innocuous with respect to the applications requirements. This activity is decomposed into two sub-steps: (a) interference prediction, and (b) interference analysis.

1) Interference prediction: The aim of this first sub-step is to predict all the "residual" interference channels. By "residual", we mean the interference channels which are not avoided by partitioning means (such as an hypervisor). We consider three types of interference: (a) hardware interference, i.e., conflict when accessing the same hardware component (e.g., interconnect, memory, etc.), logical interference, i.e., conflict when accessing the same logical component (e.g., semaphore, OS service, driver, etc.), and (c) data interference, i.e., conflict when reading or writing the same data. To predict those conflicts, we follow the transaction-driven approach proposed in [JMR + 16]. From a description of the transaction domains, i.e., the description of the paths followed by transactions issued by software and hardware components through the architecture, we compute all the situations where two (or more) transactions can overlap on the same resource. Such a situation leads to a potential interference.

One of the benefits of using a formal logical framework is to be able to compute all these potential interferences exhaustively and automatically. This point will be detailed in section V.

2) Interference analysis: Once an interference is predicted, the interference analysis aims at assessing if the interference can really happen, and what are its effects with respect to application requirements. A final configuration is said to be interference-free if all of the residual interferences are negligible.

Note that the prediction and the analysis sub-steps shall be done for both the normal conditions (without any failure), and the abnormal conditions (hardware failure). The prediction sub-step can be done automatically by using a constraint programming method. However, the second sub-step is discharged to specific analysis methods that are outside of the PHYLOG framework.

C. Argumentation

Argumentation is the third key issue required by objectives Interf2 and Error. When inquiring the certification of a system, the inquirer must provide a certification file. According to [MoD03], this should be "A reasoned, auditable argument created to support the contention that a defined system will satisfy the requirements". The exact nature of the elements is not detailed, but graphical representation or models are increasingly becoming part of this certification file. For the safety aspects, [START_REF][END_REF] explicitly requires safety cases, from which our work is inspired.

The goal of the PHYLOG Argumentation step is to represent graphically the different means of compliance used to justify the satisfaction of the requirements. The Argumentation step organizes the various elements (formal and informal) that contribute to the justification of the requirements. The argumentation step of PHYLOG is inspired by GSN [START_REF] Kelly | The Goal Structuring Notation A Safety Argument Notation[END_REF]. It is also inspired by Toulmin works for the underlying principles [START_REF] Toulmin | The Uses of Argument[END_REF], and from existing work on assurance cases in the aeronautical domain [START_REF] Holloway | Explicate '78: Uncovering the implicit assurance case in do-178c[END_REF], [START_REF] Polacsek | Validation, accreditation or certification: a new kind of diagram to provide confidence[END_REF].

A generic argumentation step relies on the following concepts (figure 1):

• Claim: the property to be justified (will often link to a requirement), • Evidence: the facts that will be used to justify the claim (analysis results, test results, expert knowledge, bibliographical reference. . . ), • Strategy: combination of different evidences in order to justify a claim, this is the model counter-part of "Mean of Compliance". • Usage Domain: domain on which the method is usable • Rationale: justifies the use of the method in this particular context Argumentation patterns are then proposed as a partial instance of this generic step, specifying subconcepts, known entities, and their necessity status depending on the strategy or strategy family. Argumentation patterns can be of different natures: generic (for example, "Using a tool" that will make it mandatory to explicit the usage domain and add a corresponding support to show its respect) or domain specific (like "Showing that the Worst Case Delay caused by an interconnect interference is less than X"). An argumentation is then built as

D. Certification requirements revisited

Another benefit of the proposed model-based approach is that the certification objectives table I can be associated to more precise certification requirements expressed and checked on the models. These requirements are classified in three families, each of which is divided in two sub-groups:

• Consistency requirements:

-ConsReq1: the architectural model provided at the Modeling step shall satisfy consistency rules such as "all applicative software shall be allocated to a unique core", "all hardware resources shall be described by exactly one normal behavior and at least one failure behavior", etc. -ConsReq2: the argumentation model provided at the Argumentation step shall satisfy consistency rules, with respect to the argumentation patterns, such as "all argumentation steps using the "verification tool" strategy shall exhibit the usage domain of the tool", etc.

• Completeness requirements:

-ComplReq1: the behaviors associated with each component from the architecture model shall be validated by a corresponding claim in the argumentation model. For instance, if an interconnect device is modeled as a set of parallel lines without interference, this description shall be considered as an assumption in the modeling step, which shall be validated by an appropriate justification in the argumentation step. This justification can be supported either by technical documents from the MCP manufacturer, by experiments, or by expert judgements, etc. -ComplReq2: all the residual interference channels identified by the interference prediction step shall be associated with a claim in the argumentation model, arguing that either the interference never happens or that it has no undesirable effect.

• Correctness requirements:

-CorrReq1: the method used to predict residual interference channels shall be safe, meaning that if an interference channel could happen, then it must be predicted.

-CorrReq2: all the interference analysis discharged to external means shall be safe, meaning that if the external means claim that the interference never happens or has no undesirable effect, then it must always be the case. The ConsReq1 and ConsReq2 lists given above are not exhaustive. Those lists may depend on the under consideration MCP and can be negotiated between the industrial applicant and the certification authority. Nevertheless, once decided, the consistency and completeness requirements can be proven automatically using the WEIRD logical framework.

IV. MCP MODELING

As expressed in the previous section, modeling is the first key issue. The idea is to gather in an understanding model all the knowledge about the MCP configuration needed for the certification purposes. Such an approach provides a way to "query" and reason about the resulting information base. For that purpose, we have defined a certification-oriented modeling langage (called PML) for MCP platforms.

A. PML: main concepts

The aim of the modeling phase is to capture and to formalize the concepts needed for the certification argumentation, and, more precisely, the concepts involved in the arguments showing that (i) the interferences due to resource sharing either are properly mitigated, or have a negligible effect on the behavior of the software applications.

As suggested by MCP-CRI, PML is organised in 4 chapters: (1) hardware platform, (2) software platform, (3) applications, and (4) integration. In this hierarchy, the terminal components are of three types: This distinction between active, reactive, and passive components will be useful for the interferences computation. An interference is an event caused by a "collision" or an "overlap" on the same shared HW component between two transactions issued by two active components and propagating through reactive components. The shared component where the interference occurs can be either active, reactive or passive.

Note that, in order to be as generic as possible, that is, to be able to address existing or future multi-core and many-core processors, the meta-model of the HW platform chapter does not offer business concepts such as "core", "interconnect", etc. Introducing business concepts would lead (1) to a great number of concepts, and (2) to a lack of genericity. We chose to capture only abstract concepts from which the concrete components can be modeled. For instance, as explained previously, a memory will be described as a Hardware Composite component, composed of a controller (considered as reactive), and several banks (considered as passive).

2) Software platform chapter: Figure 3 presents the metamodel of the software platform chapter. This chapter describes Examples of Virtualiser software are hypervisors and operating systems. Examples of bare software include specific software such as DPAA controllers. As for hardware components, a platform software is said active if it can initiate transactions to hardware elements. Otherwise, it is considered as reactive. For instance, an hypervisor is an active component: it has is own data, and it can issue events through the architecture (e.g., events for scheduling the compute partitions). By the same reasoning, the DPAA software controller is an active component. It can issue IO traffic through the interconnect to the memory. Conversely, a non intrusive trace recorder which snoops the activity of the platform is considered to be a reactive software (provided that it has been proved as being non intrusive).

From an interference point of view, active software running on a hardware/virtual resources can issue transactions through the architecture. As such, they can provoke interferences. 3) Application chapter: Figure 4 presents the concepts involved in the application chapter. Similarly to the hardware chapter, the application chapter is a tree structure. It is composed of application components, which are either terminal elements, or elements which themselves break down into subapplications. The objective is to allow description of complex applications composed of several threads running in several partitions or on several cores. An application that contains sub-applications is called an Application Composite.

In this hierarchy, we distinguish three types of terminal application software:

• Software Application, whose execution is supported by an operating system. • Bare Application over Virtual Resource, which runs in bare mode (i.e., without the support of any operating system) in a virtual resource (for instance a compute partition managed by an hypervisor). • Bare Application over Hardware resource, which runs in bare mode directly on hardware resources. Note that the OS personality component refers to OS developed (or provided) by application providers. Such OS personalities are not provided at platform level. OS provided by the platform are described in the software platform chapter as Platform Bare Component or Software Virtualiser Component.

4) Deployment chapter: The last chapter addresses the configuration of the whole equipment. It describes the Virtual Resources created and managed by the hardware/software virtualiser components. It also details on which resources (including virtual resources) are hosted the software components and the application components. And finally, it describes the transaction paths followed by transactions issued by active components through the architecture. A transaction domain is a directed acyclic graph of transaction paths from active to reactive and passive components. The HW platform involved in this example is composed of two cores, an interconnect, a memory controller, and two memory banks. All these elements are considered to be terminal. The cores, the interconnect, and the controller are reactive, whereas the memory banks are passive components. Two software applications (A0 and A1) run on the platform. Each one is hosted by one core and one bank (cores and banks are not shared between the two applications). We suppose that A0 and A1 run in bare mode (there is no platform software). Finally, we suppose that each application accesses the memory through a dedicated transaction way (one per application). Each way is composed of four transactions paths (one for each traversed component, including the applications). The transaction way for A0 (resp. A1) is depicted in red (resp. blue) in figure 5.

The PML model of this example is described in listing 1.

p t h , c o r e 1 p t h , i n t 0 p t h , i n t 1 p t h , c t r l 0 p t h , c t r l 1 p t h , b a n k 0 p t h , b a n k 1 p t h : T r a n s a c t i o n P a t h ; A0 pth h o s t e d B y A0 A1 pth h o s t e d B y A1 c o r e 0 p t h h o s t e d B y c o r e 0 c o r e 1 p t h h o s t e d B y c o r e 1 i n t 0 p t h h o s t e d B y i n t e r c o n n e c t i n t 1 p t h h o s t e d B y i n t e r c o n n e c t c t r l 0 p t h h o s t e d B y c t r l c t r l 1 p t h h o s t e d B y c t r l b a n k 0 p t h h o s t e d B y bank0 b a n k 1 p t h h

B. Formalisation

Querying and reasoning about the information imply that this information must be formally modeled. To support this approach, we relied on WEIRD, a specification language for expert modeler [BBD + 16]. WEIRD provides basic constructions to define concepts, entities, relations between model elements (with the special case of applications), and functions (between model elements and primary types as integer or boolean), as well as a rather rich expression language to describe some model elements and to query the model for assessments.

WEIRD also offers a modularity mechanism: WEIRD specifications can be separated into related worlds. When focusing on meta-modeling, this modularity will be used to separate the different concerns of a domain specific modeling language. We will use worlds to differentiate each PML chapter.

The most interesting aspect of WEIRD with respect to our concern is that the WEIRD semantics are expressed in terms of propositional logic. They allow the specification of formal queries as first order formulae, and mathematical reasoning over both the queries and the model.

In order to illustrate the WEIRD implementation of the PML chapters, let us first consider the hardware platform chapter. The implementation of this chapter is a WEIRD world called "PML-HWPlatform" (partially) shown in listing 2. Each PML concept is implemented as a WEIRD "concept" (a WEIRD concept being equivalent to a type with a sub-typing relation denoted "<:"). Each relation in the PML meta model is then directly implemented as a relation between the corresponding concepts in the WEIRD world. The translation of the toy example in listing 1 is then straightforward (cf. listing 3). It is described as a WEIRD world. It inherits from the PML chapters (relation derives in listing 3), and introduces the concrete elements of the toy example as new entities (e.g., core0, core1 and interconnect are three instances of the ReactiveHardware concepts).

p t h , c o r e 1 p t h , i n t 0 p t h , i n t 1 p t h , c t r l 0 p t h , c t r l 1 p t h , b a n k 0 p t h , b a n k 1 p t h : T r a n s a c t i o n P a t h known t r a n s a c t i o n P a t h H

C. Certification requirements revisited (again)

As said previously, one of the benefits of using a formal logical framework is to allow formal verification of certification requirements. In order to illustrate this ability, let us consider two examples of consistency requirements:

• CR1: "there is no empty composite component"

• CR2: "any hardware composite component is not part of itself " CR1 and CR2 are quantified requirements. They can be formalized as WEIRD assertions, as shown in listing 4. CR1 is decomposed in two sub-requirements, one related to hardware composite components, and the second one related to application composite components. CR11 assumes that for any hardware composite component h, there exists at least one component r (terminal or not) related to h with the relation isPartOf, meaning that r is a sub-component of h.

CR2 is more interesting. Indeed, it uses the transitive closure of the relation isPartOf (noted ˆisPartOf ). CR2 means that for any hardware composite component, (h, h) is not in the transitive closure of isPartOf. In other words, any h is not sub-component of itself nor of any sub-component of itself.

WEIRD being a logical language, such requirements are checked with an automatic solver.

V. INTERFERENCE PREDICTION

Interference prediction is a second key issue when dealing with MCP certification. Let us call "potential interferences" the interferences predicted by the prediction activity, and "actual interferences" the interferences that actually occur in the platform. For a given MCP, let us call I P the set of "potential interferences" and I A the set of "actual interferences". The prediction activity must be:

• correct, meaning that I A ⊂ I P (assuming that the platform model is correct, at least all the actual interferences are predicted), • as accurate as possible, i.e., the number of potential interferences which are not actual interferences must be as small as possible. A way to answer the correctness issue is to identify a tight (in order to answer the accuracy requirement) sufficient condition for deciding if a configuration may lead to an interference.

A. What is interference?

As defined in [JMR + 16], an interference is the disruption of the behavior of an active element A due to the activity of active elements B 1 . . . B n . This disruption is caused by an unexpected behavior of a resource R used by A. The unexpected behavior can be a change of the state of R (e.g., the resource was available and it becomes unavailable, or its value is changed, etc.). The effect of the disruption can be a delay in the activity of A, or a modification of its outputs.

Let us make three remarks:

1) First, note that interferences are not necessarily related to software applications. Any active element can suffer from interferences. 2) Second, an interference involves n + 1 active components, and at least one resource: the victim of the interference (A), the n components which have caused the interference (B 1 . . . B n ), and the resource where the interference occurs (R). 3) Third, this definition is not limited to "simultaneous collision" between transactions. Indeed, interferences can occur in scenarios without "collisions". For instance when an application B modifies the content of a shared cache by loading its own data and removing data from another application A. When, later, A will try to read its data, it will have to load the data from the memory, that will lengthen its execution time. In such cases, we talk about "delayed collision". Following these remarks, let us propose the following condition:

Interference condition: let A and B be two active components, let t A and t B two transactions issued by A and B respectively. Let a 1 , a 2 . . . , a n the resources crossed by t A , and let b 1 , b 2 . . . , b m the resources crossed by t B . a i and b j can be concrete hardware resources or virtual resources (a memory partition for instance). Then, we state that a potential interference may occur between A and B if ∃i, j such that a i and b j are hosted by the same hardware resource.

Note that this condition does not mention time. It covers interferences due to "simultaneous collisions" and interferences due to "delayed collisions". One can thus observe that if A can interfere on R with B 1 , and A can also interfere with B 2 on R, then A can potentially interfere with both B 1 and B 2 on R. That means that if we are able to predict binomial interferences (i.e., interference involving two active components on one resource), then we can predict any n-nomial interference (i.e., interference involving n active components on one resource) by overlapping binomial interferences.

This shows that it is sufficient to compute binomial interferences by using the interference condition above.

B. Potential interference computation using WEIRD

Having a sufficient condition to infer potential interferences, the next step is to infer them from a PML model.

To achieve this, we use the facts system of the WEIRD logical framework. A "fact" is an expression of the form: for (typed) variables such that the "selection expression" holds, add "knowledge" to the model. A fact system can be used to encode rules that automatically complete a model. A simple example is a fact encoding that a binary relation r is symmetric by adding the symmetrical case every time a couple is inserted in r by the user. For instance, to encode that the relation physicallyConnected of the PML hardware platform meta-model is symmetric, we add the following fact to the WEIRD implementation:

fact any (e1, e2) in physicallyConnected | true =⇒ (e2, e1) in physicallyConnected.
Similarly, we encode the interference condition with the two WEIRD facts shown in listing 5. The first fact infers knowledge used by the second fact. It says: Then, the second fact encodes the interference predicate at resource level: if (t a1 , t a , t b , t b1 ) is a potential binomial interference between transactions, then (a 1 , r, a 2 ) is the resulting potential interference at resource level, where a 1 (resp. a 2 ) is the resource which hosts the path t a1 (resp. t b1 ), and r is the shared resource which hosts both t a and t b .

C. Application to the toy example

Let us consider the toy example once more. Applied on this example, the previous facts produce the new knowledge:

[Facts] --Fact Interference1 added knowledge:

((A0_pth, int0_pth, int1_pth, A1_pth) in transactionInterference) ((A0_pth, ctrl0_pth, ctrl1_pth, A1_pth) in transactionInterference) [Facts] --Fact Interference2 added knowledge:

((A0, interconnect, A1) in resourceInterference) ((A0, ctrl, A1) in resourceInterference)

As expected, two interferences are predicted between A0 and A1: the first one on the interconnect, and the second one on the controller.

VI. CASE-STUDY

As a more complex case-study than the toy example discussed in the previous section, let us consider the many-core processor Kalray MPPA R -256 [START_REF] Corporation | The MPPA hardware architecture[END_REF] (see also [START_REF] Perret | Predictable Execution on Many-Core Processors[END_REF] for a clear and detailed presentation of the Kalray MPPA R -256 architecture).

A. Kalray MPPA R -256

The Kalray MPPA R -256 is a many-core processor featuring 288 cores on a single chip. It is organized in 16 compute clusters and 4 I/O clusters serving as interfaces for managing communications with out-of-chip components and hosting the global memory of the processor. All the clusters are connected on a dual NoC (Network on Chip) enabling point-to-point communications (one NoC for data communication (D-NoC), and a second one for control messages (C-NoC)). In this casestudy, we only consider one compute cluster connected to the D-NoC. A compute cluster features: (1) 16 cores, (2) one additional core denoted as Resource Manager (RM) in charge of managing the cluster's local resources, (3) one DMA unit to manage data transfer from and to the dual NoC, (4) a shared memory organised in 16 independent banks, (5) a fullduplex access point to the NoC (NoC Router), and (6) a Debut and Support Unit (DSU). The DMA unit is divided in two parts: a sending part (DMATx) and a receiving part (DMARx). Similarly, the NoC Router is composed in two parts: the first one connected to the D-NoC, and the second one connected to the C-NoC. Each part is composed of two FIFOs (one output FIFO to the D-NoC, and one input FIFO from the NoC). In this case-study, we only consider a restricted version of the MPPA compute cluster composed of 4 PEs, 8 Banks, 1 RM, 1 DMA and 1 D-NoC Router as depicted in Figure 6. As such, a compute cluster can be seen as a quad-core processor. However, conversely to classic multi-core processors, transactions between HW elements (PEs, DMA and RM) and the shared memory are supported by a hierarchical arbitrer, as depicted in Figure 7. For each Bank i (i = 1 . . . 8), transactions to the bank are interleaved as follows: • PEs accesses are arbitrated in a Round-Robin fashion.

• RM and DMATx accesses are arbitrated in Round-Robin.

• The two resulting transactions (from PEs and from RM or DMATx) are then arbitrated in Round-Robin. • Finaly, the resulting transactions from this last Round-Robin arbitrer is interleaved with memory requests from DMARx. However, contrary to the previous arbitration policies, requests from DMARx are treated with full priority over other memory accesses. As a consequence, requests from PEs, RM or DMATx are systematically stalled while the DMA writes input data to the memory. This is done to avoid congestion at the entry point of the cluster.

From a global point a view, the scheme depicted in Figure 7 is replicated for each bank as shown in Figure 8. That means that two different masters (among PEs, the RM and the two DMA parts) can access two different banks in parallel, without suffering from interferences. Note that, in addition to communication through shared memory, the master elements of a compute cluster (PEs, RM, DMA) can also interact by sending events:

• PEs and RM can send events to each other to achieve a synchronisation barrier; • PEs can send events to DMATx and DMARx in order to configure the Tx and Rx channels.

B. Modeling

To model a Kalray MPPA R -256 compute cluster, we follow the same approach previously shown for the toy example in section IV-A5. Each HW component (PE, RM, DMATx, DMARx, FIFO, Bank, Arbitrer, etc.) becomes a WEIRD entity. The full WEIRD model contains 51 hardware components, 90 physical connections between hardware components, 196 transaction paths, and 206 logical connections between transaction paths 1 .

C. Interference prediction

We have studied two compute cluster configurations: a "full" configuration, and a "final configuration.

a) "Full" configuration: In the first experiment, we consider a "full" configuration, i.e., a configuration in which all transactions are allowed between the masters elements (PEs, RM, and DMA) and the shared memory. Event sending between PEs, the RM and the DMA is also fully allowed. The interference prediction method computes a set of 876 potential interferences. Let us call I F ull this set. The computation of I F ull took about 37 minutes using about 6Go memory on a 2.3 Ghz Core i7 processor with 16Go memory.

Interferences of I F ull are mainly due to: (1) collisions inside each hierarchical arbitrer between transactions from PEs, the RM, and the DMATx, (2) collisions inside each master element between the own activity of the master element and events sent by other master elements, and (3) collisions inside each bank of the shared memory. As expected, input transactions from the D-NoC do not suffer from any interference when crossing the hierarchical arbitrers to the banks. The prediction method takes into account the fact that packets from the DMARx have full priority over other packets (from PEs, RM, DMATx). However, I F ull contains 44 interferences in which input transactions are potentially victim of disruptions due to other transactions. These interferences occur:

• at the entry of each bank; despite the fact that DMARx requests have a higher priority than other request, they have to wait before entering the bank if the memory is serving another request arrived just before it (from PEs, the RM or DMATx); in that case, the DMARx requests could be delayed by at most by one memory transaction from another master. • in the DMARx component, each time a PE sends an event to DMARx (for instance to access the Rx registers). b) "Final" configuration: In the second experiment, we consider a "final" configuration, representative of an embedded application, in which:

• each PE is associated with two private banks (PE1 with bank1 and bank2, PE2 with bank3 and bank4, etc.) as suggested in [START_REF] Perret | Predictable Execution on Many-Core Processors[END_REF] (configuration achieved by appropriate MMU settings); • only the RM is allowed to send events to the PEs;

• DMARx is only allowed to write input data in (and then to access) bank1, bank3, bank5 and bank7; • and DMATx is only allowed to read output data from (and then to access) bank2, bank4, bank6 and bank8.

1 The full model is available at: http://w3.onera.fr/phylog

The interference prediction method returns a set I Final of 51 potential interferences. The computation of I Final took about 35 minutes using about 6Go memory. As expected, I Final ⊂ I Full . I Final is the set of the remaining interferences not avoided by the "final" configuration and that must be addressed by the certification argumentation. As expected in this configuration, DMARx no longer suffers from disruptions due to events sent by PEs. However, input transactions from the D-NoC still suffer from 4 interferences (input-fifo, bank i , PE i ) ∈ I Final i = 1 . . . 4 (one interference at the entry of each bank with the PE "owner" of the bank).

VII. DISCUSSION AND CONCLUSION

The aim of the approach presented above is to automatically generate of the list of interferences that can potentially occur in a multi-core equipment. According to the MCP-CRI, each one of those interferences is a key certification issue. It has to be addressed by a dedicated argumentation showing that the interference never happens or has a negligible effect on the behavior of the applications hosted by the equipment. For instance, let us consider again the Kalray MPPA R -256 case-study developed in the previous section. The set I F inal returned by the prediction interference analysis contains 51 potential interferences. The certification files should thus contain 51 argumentation trees, one for each potential interference.

However, the approach still suffer from several limits. Combinatorial explosion. The first limit to overcome is the combinatorial explosion encountered when computing the intersection of the transaction ways. For instance, to consider a real Kalray MPPA R -256 cluster composed of 16 PEs and 16 banks. This would exceed the capacity of the WEIRD tool suite. To overcome this limitation, future work will include the study of a more efficient implementation of the interference prediction analysis.

Taking into account the real time behavior of the transactions. A second perspective for future work is to consider the temporal behavior of the transactions. For example, let us consider again the "final" configuration of the Kalray MPPA R -256 case-study. In this configuration, the input transactions from the D-NoC suffer from interferences at the entry of the banks. Let us now suppose that DMARx is temporally interleaved with each PE i on bank i (as defined by the time triggered execution model proposed in [START_REF] Perret | Predictable Execution on Many-Core Processors[END_REF]). By configuration, PE i and DMARx can both access bank i during non overlapping periodic time intervals. As a result, the 4 interferences (between input-fifo and PE i on bank i ) actually never happens. Taking into account the real-time behavior of the transactions thus leads to a more accurate interference prediction.

Taking into account the faulty behavior of the transactions. The third perspective for future work on the approach presented in this article is thus to pay attention to the effect of component failures on the identified interferences. To do so, we will take inspiration from the Model-Based Safety Assessment (MBSA) approach [START_REF]Model-Based Safety and Assessment -5th International Symposium[END_REF].

Fig. 1 .

 1 Fig. 1. The generic argumentation step

Fig. 2 .

 2 Fig. 2. Meta-model of the hardware platform chapter 1) Hardware platform chapter: Figure 2 presents the concepts involved in the hardware platform chapter. A HW Platform is a tree structure composed of Hardware Platform Components (noted HWP component for short). Each HWP component is either a terminal component, or an element which itself breaks down into sub-elements. For example, many-core processors are generally composed of processingclusters, themselves composed of processing-cores, which are in turn broken down into data-cache, instruction-cache, processing-unit, etc. We call Hardware Composite (noted HC) a HWP component that contains sub-components.In this hierarchy, the terminal components are of three types:

  Active and passive components correspond to what authors of [JMR + 16] have called initiator and target components. More precisely, their definition of a smart initiator (i.e., an initiator with memory) matches the notion of Hardware Composite components explained a few paragraphs below, whereas the non-smart initiators (i.e., initiators without memory) are indeed active components.In addition to these hardware elements, we introduce a more specific hardware component whose aim is to virtualize hardware resources (concept Hardware Virtualiser (noted HV)). Examples of HV component are MMUs, which allow the virtualisation of memory into memory partitions.Note that from this classification, the Freescale CoreNet Coherency Fabric involved in the P40 and T10 families is considered to be a Hardware Composite component. It is composed of two elementary components: (1) a crossbar considered to be a Reactive Hardware component, as it can only transmit transactions between the cores and the peripheral components, and (2) a coherency fabric considered to be an Active Hardware component, as it can initiate coherency transactions between the caches involved in the cores.

Fig. 3 .

 3 Fig. 3. Meta-model of the software platform chapter

Fig. 4 .

 4 Fig. 4. Meta-model of the application chapter

  Fig. 5. Toy example 5) A toy example: In order to illustrate the concepts introduced above, let us consider the toy example shown in figure 5.The HW platform involved in this example is composed of two cores, an interconnect, a memory controller, and two memory banks. All these elements are considered to be terminal. The cores, the interconnect, and the controller are reactive, whereas the memory banks are passive components. Two software applications (A0 and A1) run on the platform. Each one is hosted by one core and one bank (cores and banks are not shared between the two applications). We suppose that A0 and A1 run in bare mode (there is no platform software). Finally, we suppose that each application accesses the memory through a dedicated transaction way (one per application). Each way is composed of four transactions paths (one for each traversed

Listing 1 .

 1 Toy example (in PML) ToyExampleModel : HWPlatform / * Hardware c o m p o n e n t s * / c o r e 0 , c o r e 1 , i n t e r c o n n e c t , c t r l : R e a c t i v e H a r d w a r e ; bank0 , bank1 : P a s s i v e H a r d w a r e ; / * P h y s i c a l c o n n e c t i o n s * / ( c o r e 0 , i n t e r c o n n e c t ) p h y s i c a l l y C o n n e c t e d ; ( c o r e 1 , i n t e r c o n n e c t ) p h y s i c a l l y C o n n e c t e d ; ( i n t e r c o n n e c t , c t r l ) p h y s i c a l l y C o n n e c t e d ; ( c t r l , bank0 ) p h y s i c a l l y C o n n e c t e d ; ( c t r l , bank1 ) p h y s i c a l l y C o n n e c t e d ; SWPlatform / * None * / A p p l i c a t i o n s A0 , A1 : B a r e A p p l i c a t i o n O v e r H a r d w a r e ; Deployment / * S o f t w a r e a l l o c a t i o n * / A0 h o s t e d B y c o r e 0 ; A1 h o s t e d B y c o r e 1 ; / * T r a n s a c t i o n d e s c r i p t i o n * / A0 pth , A1 pth , c o r e 0

  o s t e d B y bank1 ( A0 pth , c o r e 0 p t h ) l o g i c a l l y C o n n e c t e d ; ( c o r e 0 p t h , i n t 0 p t h ) l o g i c a l l y C o n n e c t e d ; ( i n t 0 p t h , c t r l 0 p t h ) l o g i c a l l y C o n n e c t e d ; ( c t r l 0 p t h , b a n k 0 p t h ) l o g i c a l l y C o n n e c t e d ; ( A1 pth , c o r e 1 p t h ) l o g i c a l l y C o n n e c t e d ; ( c o r e 1 p t h , i n t 1 p t h ) l o g i c a l l y C o n n e c t e d ; ( i n t 1 p t h , c t r l 1 p t h ) l o g i c a l l y C o n n e c t e d ; ( c t r l 1 p t h , b a n k 1 p t h ) l o g i c a l l y C o n n e c t e d ;

Listing 2 .

 2 HW platform meta model in WEIRD (partial) w o r l d PML-HWPlatform { c o n c e p t H a r d w a r e P l a t f o r m C o m p o n e n t r e l a t i o n p h y s i c a l l y C o n n e c t e d : H a r d w a r e P l a t f o r m C o m p o n e n t x H a r d w a r e P l a t f o r m C o m p o n e n t c o n c e p t H a r d w a r e C o m p o s i t e <: H a r d w a r e P l a t f o r m C o m p o n e n t r e l a t i o n i s P a r t O f : H a r d w a r e P l a t f o r m C o m p o n e n t x H a r d w a r e C o m p o s i t e i s a c o n t a i n e r c o n c e p t P a s s i v e H a r d w a r e <: H a r d w a r e P l a t f o r m C o m p o n e n t c o n c e p t R e a c t i v e H a r d w a r e <: H a r d w a r e P l a t f o r m C o m p o n e n t c o n c e p t A c t i v e H a r d w a r e <: H a r d w a r e P l a t f o r m C o m p o n e n t c o n c e p t H a r d w a r e V i r t u a l i s e r <: A c t i v e H a r d w a r e }

Listing 3 .

 3 Toy example in WEIRD (extract) w o r l d Toy-Example d e r i v e s PML-HWPlatform , PML-SWPlatform , PML-A p p l i c a t i o n s , PML-I n t e g r a t i o n { e n t i t y c o r e 0 , c o r e 1 , i n t e r c o n n e c t , c t r l e a c t i v e H a r d w a r e e n t i t y bank0 , bank1 : P a s s i v e H a r d w a r e known ( c o r e 0 , i n t e r c o n n e c t ) i n p h y s i c a l l y C o n n e c t e d known ( c o r e 1 , i n t e r c o n n e c t ) i n p h y s i c a l l y C o n n e c t e d . . . e n t i t y A0 , A1 : B a r e A p p l i c a t i o n O v e r H a r d w a r e known ( A0 , c o r e 0 ) i n h o s t e d B y known ( A1 , c o r e 1 ) i n h o s t e d B y e n t i t y A0 pth , A1 pth , c o r e 0

  o s t e d B y ( A0 pth ) = c o r e 0 known t r a n s a c t i o n P a t h H o s t e d B y ( A1 pth ) = c o r e 1 . . . known ( A0 pth , c o r e 0 p t h ) i n l o g i c a l l y C o n n e c t e d known ( c o r e 0 p t h , i n t 0 p t h ) i n l o g i c a l l y C o n n e c t e d . . . }

Listing 4 .

 4 Toy example in WEIRD a s s e r t CR11 = f o r a l l e n t i t y h : H a r d w a r e C o m p o s i t e | e x i s t s e n t i t y r : : H a r d w a r e P l a t f o r m C o m p o n e n t | ( r , h ) i n i s P a r t O f a s s e r t CR12 = f o r a l l e n t i t y a : A p p l i c a t i o n C o m p o s i t e | e x i s t s e n t i t y b : : A p p l i c a t i o n | ( b , a ) i n i s P a r t O f a s s e r t CR2 = f o r a l l e n t i t y h : H a r d w a r e C o m p o s i t e | n o t ( h , h ) i n ˆi s P a r t O f

Fig. 6 .

 6 Fig. 6. Architecture of compute clusters in the Kalray MPPA R -256 (restricted to 4 PEs and 8 Banks)

Fig. 7 .

 7 Fig. 7. Hierarchical SRAM arbitrer of Kalray MPPA R -256

Fig. 8 .

 8 Fig. 8. Intra cluster communication architecture

  for any two different transaction paths t a1 and t b1 , • if t a1 and t b1 are active (i.e., issued by active components), • and if there exist two transaction paths t a and t b respectively reachable from t a1 and t b1 (reachability is encoded by the transitive closure of ˆlogicallyConnected), • and if t a and t b are collocated (i.e., hosted by the same component), • then WEIRD infers the following new knowledge: (t a1 , t a , t b , t b1 ) is a potential binomial interference, which can potentially occur on the resource shared by t a and t b .

	Listing 5. Interference condition in WEIRD (partial)
	/ / F a c t I n t e r f e r e n c e 1
	f a c t any e n t i t i e s
	t a 1 : : T r a n s a c t i o n P a t h ,
	t a : : T r a n s a c t i o n P a t h ,
	t b : : T r a n s a c t i o n P a t h ,
	t b 1 : : T r a n s a c t i o n P a t h
	| ( I s T r a n s a c t i o n P a t h A c t i v e ( t a 1 )
	and I s T r a n s a c t i o n P a t h A c t i v e ( t b 1 )
	and t a 1 ! = t b 1
	and ( ( t a , t b ) i n T r a n s a c t i o n P a t h C o l l o c a t e d ) )
	and ( ( t a 1 , t a ) i n ˆl o g i c a l l y C o n n e c t e d )
	and ( ( t b 1 , t b ) i n ˆl o g i c a l l y C o n n e c t e d )
	==> ( t a 1 , t a , t b , t b 1 ) i n t r a n s a c t i o n I n t e r f e r e n c e
	/ / F a c t I n t e r f e r e n c e 2
	f a c t any e n t i t i e s
	t a 1 : : T r a n s a c t i o n P a t h ,
	t a : : T r a n s a c t i o n P a t h ,
	t b : : T r a n s a c t i o n P a t h ,
	t b 1 : : T r a n s a c t i o n P a t h
	| ( ( t a 1 , t a , t b , t b 1 ) i n t r a n s a c t i o n I n t e r f e r e n c e
	==> ( t r a n s a c t i o n P a t h H o s t e d B y ( t a 1 ) ,
	t r a n s a c t i o n P a t h H o s t e d B y ( t a ) ,
	t r a n s a c t i o n P a t h H o s t e d B y ( t b 1 ) )
	i n r e s o u r c e I n t e r f e r e n c e

•


A M Hashem

H Abuzeid

M Kaus

S Indris

H Ehrenberg

A Mauger

C M Julien

Green synthesis of nanosized manganese dioxide as positive electrode for lithium-ion batteries using lemon juice and citrus peel

Keywords: α-MnO 2, green synthesis, lemon peel, lemon juice, lithium batteries

Green synthesis of nanosized manganese dioxide as positive electrode for lithium-ion batteries using lemon juice and citrus peel

Introduction

Manganese dioxides (MDOs) have attracted great interest because of the variety of their structures and unique properties [START_REF] Wei | Manganese oxide-based materials as electrochemical supercapacitor electrodes[END_REF]. They find potential applications such as catalysts, solar cells and electrochemical capacitors, electrode materials of Li-ion and Li-air batteries [2][3][4][5][6] due to their low cost, earth abundance, environmental friendliness and variable oxidation states [START_REF] Wang | Fabrication and lithium storage properties of MnO 2 hierarchical hollow cubes[END_REF]. The structure of MDOs is built by an assembly of [ MnO 6 ] octahedral units linked in different ways and forming cavities (tunnels) and thus different polymorphs. For instance, α-MnO 2 (cryptomelane) is constructed by edge and corner sharing of [MnO 6 ] along its c axis and displays the 2×2 tunnels architecture [8].

Submicronic materials, such as nanoparticles, nanorods, nanobelts, nanowires, nanotubes, nanofibers and urchins/orchids, mesoporous MDOs are currently investigated [9][10][11]. KMnO 4 is one of the main starting materials for synthesis of α-MnO 2 as it is not only a suitable Mn source, but it can also stabilize the crystallographic structure of MnO 2 by the presence of K + cations located in the cavities [12]. Based on redox reactions between MnO 4 -and Mn +2 species, MnO 2 nanomaterials have been successfully prepared by several methods, such as sol-gel, solid state reaction, electrochemical deposition, refluxing, hydrothermal and solvothermal routes [13][14][15][16][17][18][19]. The effect of synthetic parameters (e.g. pH value, synthesis temperature, and concentration of reactants) on the morphology of α-MnO 2 has been reported [8]. Subramanian [20] used a hydrothermal reaction at 140 °C for various reaction times (1-18 h) to synthesize MnO 2 nanorods using MnSO 4 ·H 2 O and KMnO 4 as starting materials. Xu et al. [21] prepared hollow spheres with a highly loose and mesoporous cluster structure of α-MnO 2 using KMnO 4 , sulfuric acid and Cu scrap. Nanowhiskers and nanorods of MnO 2 were synthesized at 120 °C by a hydrothermal method using KMnO 4 and HNO 3 [22]. Liu et al. [23] succeeded to synthesize amorphous and spherical MDOs using KMnO 4 , ethanol and sulfuric acid at pH=2 with particle sizes of about 100 nm at 60 °C. Also, the same reagents were used to synthesize α-MnO 2 nanowires with controllable size via a low-temperature hydrothermal route with a subsequent heat treatment, which showed promising electrochemical properties [24]. Feng et al. [25] used the one-pot hydrothermal synthesis to grow α-MnO 2 nanorods with an average diameter of 300 nm and length up to 1.2 mm, while Ji et al.

[26] used a similar method to obtain longer α-MnO 2 nanorods.

In attempts to replace traditional chemical reducing agents such as ethanol, hydrazine hydrate, sodium borohydrate, formaldehyde, ethylene glycol, etc. by biological reagents containing anti-oxidative moieties such as flavonoids, tannins, vitamin C, etc., one can solve problems of cost and pollution [27]. Thus, many natural substances such as extracts of plants [28] can be used in "green synthesis" methods. Lemon juice is mostly water.

The most important ingredient is citric acid, i.e. 5 vol.%, 48 g L -1 , next is malic acid, ascorbic acid (vitamin C: 40 mg per 100 g of lemon), and traces of tartaric acid [29].

For instance, extracts of peel of citrus fruits are directly reducing agents (antioxidant) [30] because they are rich sources of flavonoid glycoside, coumaric acid, βand γ-sitosterol and volatile oils [31][32][33][34]. Extracts of lemon as rich sources of citric and ascorbic acid (vitamin C) were used to synthesize ZnO nanoparticles [35]. Ahmad et al. [36] pointed out that fibers of citrus fruit contain bioactive elements such as polyphenols and ascorbic acid, which promote the crystallization process of metal oxides.

In a recent review on nanostructured MnO 2 as electrode material for energy storage, we pointed out that the problems of the Zn/MnO 2 battery (limited cycling life and power)

have now been entirely solved. The alkaline Zn/MnO 2 batteries now outperform the Liion batteries not only by the lower price, but also by their performance, both in energy and in power density [37]. In particular, Liu et al. reported such a battery, the capacity of which was 285 mAh•g -1 (MnO 2 ), with capacity retention of 92% over 5000 cycles [38].

MnO 2 is thus a promising candidate to be the electrode of next generation of commercial rechargeable batteries. The next problem is thus to optimize the synthesis of this material in terms of cost and environmental friendliness.

The present work addresses this problem by employing a facile, eco-friendly and cost-effective method using lemon juice and citrus peel to prepare α-MnO 2 nanomaterials, in which the reduction of KMnO 4 is ensured by the use of mixed biochelators including carboxylic groups. The as-prepared samples were characterized by XRD, TGA, SEM, TEM and Raman analyses. The electrochemical properties of both α-MnO 2 samples were evaluated by cyclic voltammetry and galvanostatic charge-discharge processes.

Experimental

Two MnO 2 samples were prepared by green synthesis using fresh lemon juice (final product named J-MnO 2 ) and extract of lemon peel (final product named P-MnO 2 ). Pieces of fresh lemon were washed and squeezed to prepare 40 ml of juice, which was boiled for 10 minutes, filtered and completed with distilled water after boiling to have 50 ml then stirred again for 15 minutes at room temperature followed by a final filtration. This extract of juice was added to 4.7 g KMnO 4 , dissolved in 100 ml of water and acidified with 2 ml of 2. water by stirring for 15 minutes at room temperature followed by another filtration. The extract was added to 2.5 g KMnO 4 , dissolved in 100 ml of water and finally treated by the same manner described above.

The crystal structure was determined by XRD analysis using a STOE STADI P diffractometer with curved Ge 111 monochromator and Mo K α1 radiation and a Mythen 1K strip detector (50 μm strip pitch DECTRIS). Rietveld refinements were performed by the FULLPROF program [39,[START_REF] Klug | X-ray Diffraction Procedures for polycrystalline and Amorphous Materials[END_REF]. TGA measurements were carried out using a thermal gravimetric analyzer (Perkin Elmer, TGA 7 series) in the temperature range of 50-1000

°C in air at a heating rate of 10 o C min -1 . The morphology and structure of the samples were further investigated by field emission scanning electron microscopy (FESEM, Quanta FEG 250), and high-resolution transmission electron microscopy (HRTEM, JEOL, JEM-2100, Electron microscope, Japan). Raman spectra were collected on a LabRam Evolution HR (HORIBA) spectrometer equipped with a Nd:YAG laser (523 nm, 1 mW). The final spectra consist of two independent acquisitions with a total acquisition time of 720 s.

Electrochemical properties of MnO 2 electrodes were carried out in Swagelok-type cells. The active material was mixed with carbon black (Super P, Timcal) and PVDF in the ratio 80:15:5. The cathode loading was ~4 mg cm -2 . Two layers of Whatman GF/B separators and 1 mol L -1 LiPF 6 in a 1:1 mixture of ethylene carbonate and dimethyl carbonate were used for the cell assembly. Lithium metal was used as the counter electrode. The material was characterized galvanostatically using the cycling station model Lithium Cell Cycler, KIT. Cyclic voltammograms (CV) were recorded using a VMP3 potentiostat (Biologic Science Instruments, France) at a sweep rate of 0.1 mV s -1 .

Results and discussion

Structural properties

Figures 1a-b display the X-ray diffraction patterns of the green synthesized samples using lemon peel extract (P-MnO 2 ) and lemon juice (J-MnO 2 ), respectively. All the XRD peaks can be readily indexed to -MnO 2 (JCPDS, 44-0141). A Rietveld refinement of the underlying structure model, based on the cryptomelane polymorph noted α-MnO 2 , was applied for P-MnO 2 . The comparison between observed and calculated patterns is shown in Fig. 1a together with their difference curve. The structure parameters of the tetragonal structure (space group I4/m) are summarized in Table 1. Residual potassium in the structure is detected, corresponding to the composition K 0.12 MnO 2 . The potassium distribution is smeared out along the (0,0,z) tunnels, best described by two partially occupied sites K1 and K2. The 002 reflection has a much smaller half-width, which is only determined from the projection of the electron density on the c-axis and not affected by any disorder in the ab-plane. In contrast, despite the optimization of the sintering temperature at 340 °C, J-MnO 2 does not show sufficient long-range order for a reasonable Rietveld refinement. A comparison between the observed diffraction patterns for J-MnO 2 and for an empty capillary is shown in Fig. 1b. The maximum intensity corresponds to the position of the strongest reflection (121) of the cryptomelane structure.

It is well known that large K + cations are inserted into the tunnel cavity (2e Wyckoff site) during synthesis of the -MnO 2 hollandite structure [START_REF] Yuan | [END_REF]42]. The presence of K + is the key parameter, which governs the properties of these materials. Recently,

Yuan et al. investigated the influence of potassium cations on the electrochemical

properties of -MnO 2 . The role of cations inside 2×2 tunnels has three beneficial effects:

(i) increase of the electronic conductivity of the host, (ii) improve the Li + diffusivity and (iii) introduce a structural transition during lithiation for high K + concentration, i.e.

x=0.25 [START_REF] Yuan | [END_REF]43]. This large cation is essential for the formation and stabilization of -MnO 2 lattice [44] and leads to the mixed valence state of Mn 4+ and Mn 3+ ions that depends of the potassium concentration. K + ions increase the concentration of lesslocalized e g d-electrons of the Mn 3+ ions. Especially, Luo et al. [45] demonstrated that the -K 0.12 MnO 2 specimen is homogeneous with the Mn ions in the average oxidation state. and the weak bands at 390 and 180 cm -1 match well with the tetragonal unit cell (space group I4/m; spectroscopic symmetry C 5 4h ). Shortly, the Raman band at 180 cm -1 is due to the translational motion of the MnO 6 octahedra (lattice mode), the band at 390 cm -1 is attributed to the Mn-O bending vibrations, while the high-frequency bands at 577 and 638 cm -1 originate from the stretching vibrations of MnO 6 octahedra within the tetragonal lattice [46,47]. These results appear to be in good agreement with those obtained by Xray diffraction as the degree of crystallinity also affects the local atomic environment, i.e. the strength of the Raman modes. The difference between the XRD patterns of J-MnO 2 and P-MnO 2 and between the Raman spectra as well are attributed to the different degrees of crystallinity for both samples, which originates from the nature of reducing reagents that have been used. It is well-known that the chelate-assisted sol-gel method with different carboxylic acids can result in markedly different structural defects and morphologies of products [48].

However, in the sol-gel method, the choice of chelators often directly affects electrochemical properties of the products. For example, when only citric acid is used as chelating agent, some issues will appear in the process of heat treatment due to the existence of segregation phenomenon in the precursors [49]. By employing a mixture of chelators, these disadvantages can be overcome, which provides a homogeneous distribution of uniform nanosized particles with good stoichiometry control of the final product. Such a procedure has been recently applied to prepare Li-rich cathode materials [50]. In this work, we compare two mixed chelators with different molecular architectures (Fig. 3), which belong to the class of bio-reagents present in citrus fruits [35]. As a result, the reduction of potassium permanganate appeared very sensitive to the complexing reagent, i.e. the bonding of -COOH-carboxylic groups, which makes a big difference in the crystallization of MnO 2 . Powders grown by the lemon juice-assisted route exhibit a highly disordered structure even at the local scale observed by Raman spectroscopy, whereas P-MnO 2 samples synthesized with extracts of lemon peel present a better crystallinity of the nanostructured particles owing to the complex molecular moieties involved in the reduction process acting as fuels for the MnO 2 crystallization.

The ill-resolved bands of the Raman spectrum of the J-sample shows that even the molecular scale is affected, despite the large size of the crystallites (2.4 nm). This is attributed to the fact that the strain field generated by the grain boundaries is long range in nature, i.e. a range that is of the same order of magnitude as the crystallite size. This strain field thus creates lattice distortions that extend to the same size, which explains not only the lack of resolution of the Raman spectrum, but also explains the lack of long-rage crystalline order as observed by X-ray diffraction. Another reason for the poorly resolved Raman spectrum could be that a rather random distribution of K + in the tunnels is blocking and coupling some vibrational modes.

Thermal stability

Figures 4a-b show the thermogravimetric analyses (TGA) of the J-MnO 2 and P-MnO 2 asprepared samples, respectively. These TGA curves have almost the same thermal behavior typical of MDOs. The gradual weight loss observed in the range 25-250 o C with a weight loss of ca. 10 % is assigned to the release of predominantly adsorbed water and weakly bounded water molecules present in the sample and trace amounts of oxygen [51]. The second gradual weight loss is attributed to the formation of highly crystallized -MnO 2 followed by an endothermic reaction which is due to the removal of oxygen and the conversion of -MnO 2 to -Mn 2 O 3 phase. This distinct transformation is observed at 530 and 600 °C for J-MnO 2 and P-MnO 2 , respectively. The third weight loss recorded at T>900 °C is attributed to further oxygen loss and the formation of the Mn 3 O 4 spinel structure [47]. The shape of thermograms as well as phase transitions shown in Fig. 4 are in good agreement with the literature [52][53][54].

Morphology

Figure 5 (a-d) show the SEM and TEM images of green-synthesized MnO 2 samples. Two different morphologies are clearly evidenced. As shown in Fig. 5a, the sample prepared via lemon juice consists of agglomerates of very fine particles of less than 10 nm size (Fig. 5c). Few particles have the tendency to grow with a nanoneedle-like shape (~50 nm length). In contrast, the sample prepared via lemon peel has a different morphology. The poor crystallization of the J-MnO 2 sample explains the irregular form of the particles, but also is an obstacle to the growth of the particles during the synthesis after their nucleation, which explains the smaller size of the primary particles. As shown in Fig. 5d, P-MnO 2 consists of fairly uniform nanorods with an average size about 17 nm in diameter and 150 nm in length. From the above described investigations, it is clearly demonstrated that the nature of the reducing reagent has a strong effect on the morphology of α-MnO 2 particles. It is the combination of citric and ascorbic acids that provide the smallest nanosized particles, while the complex reducing reagent of lemon peel favors the growth of regular nanorod-like materials. Note that among anti-oxidative moieties in Fig. 3b, p-coumarin acid is the most abundant phenolic compound in citrus peel, while β-sitosterol belongs to the class of "plant sterol" with a chemical structure similar to that of cholesterol, and flavonoid glycosides are primarily anti-oxidative components in the lemon peel. Currently, α-MnO 2 nanorods are synthesized by adopting work, we have obtained the same sample morphology of α-MnO 2 crystalline nanorods using a facile and low-cost synthetic process.

Electrochemical tests

MnO 2 powders were electrochemically tested by cyclic voltammetry and galvanostatic charge-discharge cycles in the voltage range 1.5 -3.5 V vs. Li + /Li 0 at different current densities from 10 to 400 mA g -1 (1C=260 mA g -1 ). The cyclic voltammograms (CVs) of the first 20 cycles are displayed in Fig. 6. It is well known that lithium ions are accommodated on off-center 8h Wyckoff positions inside -MnO 2 2×2 tunnels that determine the overall discharge capacity [START_REF] Yuan | [END_REF].

During the first discharge process both CVs are dominated by a broad current peak around 2.5 V. The broadness of redox peaks is attributed to the poor crystallinity and/or the morphology of α-MnO 2 nanopowders. The shift of the reduction peak from 2.5 V at the first discharge cycle to 2.65 V for the forthcoming cycles is assigned to the lithiumcell formation and to the small amount of remaining Li ions inserted in the initial discharge reaction, i.e. the so-called loss of lithium inventory (LLI). This type of structural evolution is currently observed for the hollandite α-MnO 2 electrode [36,58].

Ching et al. [59] have reported the change in peak position as a structural change associated with γ-MnO 2 , which does not occur in our case. CV curves show clearly that the host structure is stabilized by partial lithiation of α-Li x MnO 2 . This stabilization is obviously observed for the subsequent cycles (Fig. 6), for which the set of intense redox peaks is located around 3.15 and 2.65 V, and the differential peak potential between E ox and E red is 0.5 V. This value is higher than the one reported for micro-sized materials [60] and did not vary significantly in the subsequent cycles. Tompsett et al. [61] suggested that lithium ions are preferentially located at the off-center 8h sites, near the walls of the 2×2 tunnels for the initial stage of lithiation (0≤x≤0.5 in α-Li x MnO 2 ), while 8h' sites are occupied for a high concentration Li + ions in α-Li 0.75 MnO 2 because of the different energies of formation. Both samples have a similar behavior for the subsequent discharge cycles. The most distinct features for green synthesized MnO 2 electrodes are the set of small redox peaks located at 2.6 and 2.3 V, which gradually decrease as the cell is cycled.

In case of the P-MnO 2 sample, the reduction process is characterized by an additional reduction peak located at 2.8 V. These features are attributed to the effect of the insertion-deinsertion mechanism in MnO 2 nanocrystallites with sizes smaller than 10 nm. The galvanostatic discharge-charge profiles of the Li//α-MnO 2 cells are presented in Fig. 7. Measurements were carried out in the voltage range 1.5 -3.5 V vs. Li + /Li 0 at a current density of 10 mA g -1 (C/26). These results show several features: (i) the first cycle is dominated by a distinct irreversible capacity for both materials, (ii) the degree of crystallinity affects the shape of discharge-charge profiles, (iii) the charge pseudo plateau is clearly observed in highly crystallized P-MnO 2 sample, while the discharge-charge curves of J-MnO 2 display a rather S-shape characteristic of a disordered material, (iv) a noticed difference is observed in the voltage curve at the end of the discharge process.

The initial discharge specific capacity of J-MnO 2 is ~245 mAh g -1 , whereas subsequent discharging reactions achieve only a specific capacity of ~135 mAh g -1 . The same situation is observed in the case of P-MnO 2 with an initial specific capacity of ~214 mAh g -1 . This can be attributed to the size of nanoparticles that results in a high specific surface area (BET≈12 m 2 g -1 ) and thus an increase of the effective interface between material and electrolyte. The best electrochemical behavior of the P-MnO 2 electrode is evidenced by the estimation of the slope Q/V of the discharge curves. One finds Q/V= 180 mAh g -1 V -1 for J-MnO 2 and Q/V=294 mAh g -1 V -1 for P-MnO 2 . On the other hand, the situation is reversed as soon as the second cycle is carried out (see Fig. 7).

In both samples, the irreversible capacity decreases and the coulombic efficiency increases after the first cycle. These results match well with electrochemical data reported in Ref. [43] for samples prepared by wet-chemical methods. From the second cycle to the 5 th cycle, the discharge capacity of the J-MnO 2 sample increases from 135 mAh g -1 to 145 mAh g -1 , due to the formation of the solid-electrolyte interface, and the fact that additional sites at the surface are available at the surface of the particles. The better performance is even more pronounced when considering the rate capacity reported in Fig. 8 for discharge current densities in the range 10-400 mA g -1 . A reversible specific capacity of 50 mAh g -1 is delivered for the P-MnO 2 cell at 400 mA g -1 , while that of the J-MnO 2 has vanished, an evidence for the sluggish kinetics associated to the lattice disorder. The coulombic efficiency for the first charge of both samples is small, but on the second cycle the cells show good rechargeability with efficiency close to 99%. Fig. 8b presents the cycleability for J-MnO 2 and P-MnO 2 electrodes. After 50 cycles, the capacity retention of P-MnO 2 got restored to 73%, while it was 55% for J-MnO 2 . The better electrochemical performance of P-MnO 2 is attributed to its crystallinity as reported in the structural section.

Conclusion

The green synthesis of MnO 2 prepared with either the juice (J) or the peel (P) of lemon has been successfully achieved. Both the crystallization and the electrochemical properties are improved in the P-MnO 2 with respect to J-MnO 2 . This is attributed to the fact that the lemon peel contains three reducing (anti-oxidative) reagents (and volatile oils), while the juice of lemon contains only citric and ascorbic (Vitamin C) acids, which leads to better results than those obtained with only one of these two acids, but still less than the three active elements in the peel. The electrochemical properties of the P-MnO 2 are as good as those obtained with the traditional chemical reducing reagents that are both costly and polluting. This new synthesis is straightforward and inexpensive then allows for a synthesis process that is green, cheaper, and easily scalable for mass production of α-MnO 2 that has many applications in the industry, including electrochemical energy storage.

Figure captions

Fig. 1 .

 1 Fig. 1. X-ray powder diffraction patterns of green synthesized MnO 2 using (a, left) lemon peel extract, P-MnO 2 and (b, right) lemon juice, J-MnO 2 . The results of a Rietveld refinement is shown for P-MnO 2 with refined composition K 0.12 MnO 2 in (a). A comparison between XRD patterns from J-MnO 2 and the empty capillary is shown in (b), because of a lack of sufficient long-range order. Two characteristic reflections are labelled.

Fig. 2 .

 2 Fig. 2. Raman scattering spectra of α-MnO 2 nanostructured powders prepared by lemon juice (J-MnO 2 ) and lemon peel (P-MnO 2 ).

Fig. 3 .

 3 Fig. 3. Molecular representation of anti-oxidative moieties present in citrus fruits. (a) lemon juice and (b) lemon peel.

Fig. 4 .

 4 Fig. 4. Gravimetric thermograms of green synthesized samples (a) J-MnO 2 and (b) P-MnO 2 in air.

Fig. 5 .

 5 Fig. 5. (a,b) SEM images of green synthesized samples (a) J-MnO 2 and (b) P-MnO 2 and (c,d) TEM images of green synthesized samples (c) J-MnO 2 and (d) P-MnO 2 .

Fig. 6 .

 6 Fig. 6. Cyclic voltammograms of the first 20 cycles (from black via red, yellow and green to blue) samples (a) J-MnO 2 and (b) P-MnO 2 carried out at sweep rate of 0.1 mV s -1 .

Fig. 7 .

 7 Fig. 7. Charge-discharge voltage profiles of MnO 2 //Li cells with (a) J-MnO 2 and (b) P-MnO 2 cathode materials. Measurements were carried out at current of 10 mA g -1 . S1 and S2 are the slope V/Q of the potential profile at Q max /2.

Fig. 8 .

 8 Fig. 8. Rate capability tests of Li half cells for (a) J-MnO 2 and (b) P-MnO 2 .

Fig. 1 .

 1 Fig. 1. X-ray powder diffraction patterns of green synthesized MnO 2 using (a, left) lemon peel extract, P-MnO 2 and (b, right) lemon juice, J-MnO 2 . The results of a Rietveld refinement is shown for P-MnO 2 with refined composition K 0.12 MnO 2 in (a). A comparison between XRD patterns from J-MnO 2 and the empty capillary is shown in (b), because of a lack of sufficient long-range order. Two characteristic reflections are labelled.

Fig. 2 .

 2 Fig. 2. Raman scattering spectra of α-MnO 2 nanostructured powders prepared by lemon juice (J-MnO 2 ) and lemon peel (P-MnO 2 ).

Fig. 3 .

 3 Fig. 3. Molecular representation of anti-oxidative moieties present in citrus fruits. (a) lemon juice and (b) lemon peel.

Fig. 4 .

 4 Fig. 4. Gravimetric thermograms of green synthesized samples (a) J-MnO 2 and (b) P-MnO 2 in air.

Fig. 5 .Fig. 6 .Fig. 7 .

 567 Fig. 5. (a,b) SEM images of green synthesized samples (a) J-MnO 2 and (b) P-MnO 2 and (c,d) TEM images of green synthesized samples (c) J-MnO 2 and (d) P-MnO 2 .

Fig. 8 .

 8 Fig. 8. Rate capability tests of Li half cells for (a) J-MnO 2 and (b) P-MnO 2 .

Acknowledgement

Some part of this work has benefited from financial support within the BMBF project "DESIREE", grant number 03SF0477B.