Dirk Kuschnerus
email: dirk.kuschnerus@rub.de

Attila Bilgic
email: a.bilgic@krohne.com

Thomas Musch
email: thomas.musch@est.rub.de

Aspect-oriented Data and Safety Modeling for Cyber-Physical Systems in Process Automation

Cyber-physical systems (CPS) integrate computation with physical processes, enabling the dynamic adaption of systems based on economic and environmental conditions. The adoption of CPS in industrial process automation is impeded by legacy systems with severe functional safety constraints and the need for highly configurable devices. To transfer the benefits of CPS to process automation, the inherent conflict between CPS safety and configurability must be explicitly considered during system design and operation. This paper proposes aspect-oriented modeling of safety and data for CPS in process automation as a baseline for formal consistency monitoring.

I. INTRODUCTION

Cyber-physical Systems (CPS) integrate computation and physical processes [START_REF] Lee | Cyber physical systems: Design challenges[END_REF]. A remaining key research challenge for CPS is the definition of suitable modeling approaches covering abstraction and functional safety [START_REF] Derler | Modeling cyber-physical systems[END_REF], [START_REF] Rajkumar | Cyber-physical systems: The next computing revolution[END_REF]. Devices used in process automation CPS are usually mass market products which must be adapted to the specific process environment of the customer. Suppliers implement this requirement by adding configurability to their products, tailoring them to the customer's requirements during production and on-site. This drastically increases device complexity, an effect which is amplified by the emergent requirements for highly dynamic systems arising from initiatives like the German "Industry 4.0", where factory automation shall enable the dynamic adaption of the production to customer's desires or real-time demand and economical factors along the life cycle of a product [START_REF] Colombo | Industrial Cloud-Based Cyber-Physical Systems: The IMC-AESOP Approach[END_REF]. Unlike in factory automation, systems in process automation are typically large scale plants with complex static control loops, where despite its benefits CPS adoption is limited by functional safety restrictions imposed by standards such as IEC 61508 [START_REF]Functional safety of electrical/electronic/programmable electronic safety-related systems[END_REF] due to risks for humans and environment. Safetycritical applications require extended verification of the plant's safety functions, which is impeded when the implementing CPS components are configurable, creating a dependence between safety-critical behavior and configuration data. This conflict raises the need for formal specification and verification techniques to enable safety verification of devices considering specific configurations. In [START_REF] Kuschnerus | A hierarchical domain model for safety-critical cyber-physical systems in process automation[END_REF], we introduced a domain model for hierarchical modeling of CPS in process automation. In this paper, we propose a modeling approach advancing our domain model, using the aspect-oriented paradigm to explicitly model the safety and data concerns separated from the CPS domain model. Our goal is to enable the reasoning about safety in presence of complex configurability, setting a baseline for the application of dynamic CPS in process automation while preserving the required functional safety of the legacy installations. The remainder of this paper is organized as follows: Section II examines related work on CPS modeling, Sections III and IV describe the interconnected modeling of the safety and data aspects. Both aspects are jointly examined in a case study in Section V, which also covers inconsistencies between aspect and domain models. Section VI gives a conclusion and outlines further research directions.

II. RELATED WORK

To obtain an overview of methods for modeling CPS in process automation, we conducted a systematic mapping following the method introduced in [START_REF] Petersen | Systematic mapping studies in software engineering[END_REF]. The mapping identified and categorized a total of 448 relevant publications, 15 of which target the domain of process automation. This low number is also confirmed by [START_REF] Khaitan | Design techniques and applications of cyberphysical systems: A survey[END_REF], where only one publication from the domain of industrial automation is listed. Following our mapping, we further examined the relevant papers from all domains in a systematic literature review as suggested in [START_REF] Kitchenham | Guidelines for performing systematic literature reviews in software engineering[END_REF], focusing on the aspects of data and functional safety. From the 15 process automation papers only [START_REF] Genge | Physical process resilience-aware network design for SCADA systems[END_REF], [START_REF] Saeedloei | A logic-based modeling and verification of CPS[END_REF] and [START_REF] Schwarz | Modelling a real-time control system using parameterized linear hybrid automata[END_REF] address functional safety. A combination of safety and data modeling was only found in [START_REF] Schwarz | Modelling a real-time control system using parameterized linear hybrid automata[END_REF], where the reachability of unsafe hybrid parametrized automata states is determined but further safety and data concepts such as hierarchical modeling and data dependencies are not covered. To additionally cover cross-domain and generic approaches, we broadened our investigation to relevant approaches from all domains and identified 5 further papers covering data and safety aspects in CPS ( [START_REF] Besnard | Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using polychrony[END_REF], [START_REF] Rajhans | Supporting heterogeneity in cyber-physical systems architectures[END_REF], [START_REF] Saunders | Information flow diagram analysis of a model cyber-physical system: Conflict detection and resolution for airport surface traffic[END_REF], [START_REF] Stauner | Systematic development of hybrid systems[END_REF], [START_REF] Zheng | Towards a model checker for NesC and wireless sensor networks[END_REF]). [START_REF] Rajhans | Supporting heterogeneity in cyber-physical systems architectures[END_REF] describes architectural views for heterogeneous CPS models and consistency considerations between these views as well as behavioral semantics for system verification. The approach uses automata states to model and verify the safety of the CPS. [START_REF] Stauner | Systematic development of hybrid systems[END_REF] develops a formal framework and graphical notation for the development of hybrid systems using graphs and hybrid automata. Neither [START_REF] Besnard | Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using polychrony[END_REF], [START_REF] Rajhans | Supporting heterogeneity in cyber-physical systems architectures[END_REF], [START_REF] Saunders | Information flow diagram analysis of a model cyber-physical system: Conflict detection and resolution for airport surface traffic[END_REF] nor [START_REF] Stauner | Systematic development of hybrid systems[END_REF] include the modeling of safety concepts that are incorporated in the design of the whole CPS on various abstraction levels or the in-depth coverage of configuration and the effects of configuration data on system behavior and safety. [START_REF] Zheng | Towards a model checker for NesC and wireless sensor networks[END_REF] does not cover physical and deployment views of CPS which we consider important for safety and data consistency. In addition, none of the publications mentioned before use aspect-oriented modeling for the cross-cutting concerns of safety and data. Concluding our literature review, to the best of our knowledge our approach differentiates from the state of the art by covering the explicit aspect-oriented modeling of functional safety and data for CPS in process automation. We are further not aware of generic or cross-domain approaches providing a comprehensive modeling coverage of safety and data concepts which we consider crucial for CPS in process automation.

III. ASPECT-ORIENTED SAFETY MODELING

In aspect-oriented development, cross-cutting concerns affecting major parts of the development artifacts are represented as detached aspects to achieve separation between functionality and cross-cutting concerns [START_REF] France | Aspect-oriented approach to early design modelling[END_REF]. During the definition of our domain model, we identified the influence of functional safety on its structural, behavioral, physical, deployment and communication viewpoints on the plant, CPS, subsystem and component layers of abstraction. In addition to their distributed influence, safety concepts typically are major development artifacts which regarding to their specification and certification efforts are desired to be reused in multiple projects. We therefore follow the aspect-oriented paradigm by integrating these concerns into safety aspect models abstracted from a specific device development and connecting them to our domain model using formal weaving functions. define cross-cutting safety concerns from all viewpoints and abstraction layers. Multiple concerns are integrated to safety concepts implementing safety functions, which are defined in IEC 61508 [START_REF]Functional safety of electrical/electronic/programmable electronic safety-related systems[END_REF] as functions controlling a process or system to mitigate the risk of dangerous failure causing harm to humans and environment. The connection points between aspect models and the domain model are formally defined by weaving functions and structurally constrained by well-formedness rules (wfrs). The following paragraphs give an overview of the aspect beginning with the cross-cutting concerns. The influence of functional safety on the logical CPS structure is primarily specified by the criticality and safety integrity level (SIL) of structural model elements, needed as baseline for further approaches such as partitioning and deployment. The function crit defines whether an element is safety-related (sr), non-safety related (nsr) or has a mixed criticality:

crit crit crit :Entity ∪ DeployContext ∪ Channel ∪ P rotocol → {sr, nsr, mixed} (1)
The function sil defines a SIL for each element used to determine its valid dependencies regarding safety. To connect this safety information to our domain model, we define the weaving-function addAttribute:

addAttribute addAttribute addAttribute ={faA 1 , ..., faA n } faA i =E ⊆ Entities → type(atti ∈ Attributes) (2)
specifying a function f aAi for each attribute A i that shall be added to the domain model. f aAi assigns the type of A i to each of the targeted Entities E . f aAi is by convention named after the added attribute A i . The application of every weaving function is constrained by associated structural wfrs. IEC 61508 differentiates between systematic failures and random hardware failures e.g. due to hardware aging. The latter are included in safety analysis such as Failure Modes Effects and Diagnostic Analysis (FMEDA) to determine the risk of dangerous undetected failures of the safety function.

We add hardware failure information to the hardware elements in the domain model using the weaving function addAttribute, covering the probability of a hardware error, the fractions of safe, unsafe, detected and undetected errors and aggregated values for system integrators. Both augmentation and restriction can be applied to all behavioral models used in [START_REF] Kuschnerus | A hierarchical domain model for safety-critical cyber-physical systems in process automation[END_REF]. Fig. 2 shows the generic safety automaton, describing the internal safety mode of the CPS from startup to nonsafe and safe operation. The CPS stays in safe operation in case of dangerous undetected and safe errors, switching to a safe state on detection of critical errors. The augmentation of behavioral semantics is used in the motivated verification of process safety functions considering their configurable realization. On the subsystem layer, safety functions are modeled by adding control modes to the hybrid automaton of the process step. The process safety time, i.e. the time between the occurrence of a failure and a resulting hazardous event defines the detection and reaction time available to the safety functions for mitigating the risk of the event and is modeled inside the safety automaton of the specific CPS. The realization of safety functions is modeled on the component layer by modifying the system's activity diagrams. Both concepts are detailed in section V-D.

As shown in Fig. 1, our safety aspect additionally defines reusable safety concepts from sets of cross-cutting concerns. These templates can e.g. define diagnostic functions to detect the hardware failures introduced above, facilitating the tracing between failure analysis and mitigation as shown in the 2-channel safety concept in Fig. 11.

IV. ASPECT-ORIENTED DATA MODELING

The device development for industrial CPS targets mass markets where it is unfeasible to develop individual products for every customer. As a result, complementing the measurement data the CPS gathers and processes, industrial CPS contain a large number of configuration data used for the customization of base device variants to the customer's application. Both data categories influence all viewpoints over the entire system hierarchy. A configuration data model is often used detached from a specific device, e.g. during manufacturing and order processes or customer service and should be separated from other development artifacts. We therefore model CPS data as aspect to enable data development, deployment and analysis to be conducted independently from the domain model. Fig. 3 shows the fundamental data aspect model for CPS in process automation, categorizing data items into device variables and static data. Device variables represent values connected to the physical process which are periodically refreshed and distributed throughout the CPS, whereas static data items describe typically persistent attributes of the CPS itself. Every data item is uniquely identified by its localId and scope, which defines the area where device variables are distributed and static data is synchronized and available to all modules. This can be e.g. a partition or a node. Device variables are produced by one distinct software module (producer), can be set to a synthetic test value (synthetic) and connected to an external CPS interface (outputChannel). Each device variable has an update interval and can be kept local by stopping the bus distribution. The data aspect defines two types of device variables: a float value with timestamp and a double value. Static data is protected by an access level specifying valid editors as well as the item's settings for persistent storage and replication between data stores. Static data is defined for several data types and contains actual, default and SIL values and associated value ranges. The data aspect also defines dependencies between data items. Configuration details of device variables such as limits and default values are given by a referenced static data item (configuredBy). Both device variables and static data can be derived from other data items. Derived data items are locally calculated from primary data items and are not persistently stored. In addition, static data items can interfere with each other during the update of their values. An updateDependency between multiple data items denotes that the CPS can only accept an updated value of a data item if the dependent items are also updated. The checkDependency is an internal dependency that triggers a validation of connected data items if the value of one data item is altered. While the safety and data aspects are specified concurrently to the domain model, there is interdependence between the aspect models. Device variables and static data both have a criticality and SIL defined via the weaving function addAttribute from the safety aspect. In addition, the SIL value in static data items defines a value that is set when the safe operation mode specified by the safety aspect is entered. The aspect model is connected to the domain model using the concepts of weaving functions and restrictions specified by wfrs as described in Section III. In the structural, communication and deployment views, attributes can be altered and entities such as software modules can be deactivated by the data aspect. As the data aspect models the CPS internal representation of process values, it adds a connection between process values and device variables thus connecting physical and computational parts of the domain model. In the deployment and communication views, the storage and distribution data flow of device variables and static data is modeled using the weaving function addData. This function also specifies hardware configuration by connecting static data items to hardware nodes. As described in Section III, the aspect models influence the behavior of the CPS. The influence of configuration data to the behavioral semantics is modeled using the weaving functions addBehavior and removeBehavior as shown in Fig. 9.

V. CASE STUDY

A. Example Process -Distillation in MDI Production

We use the simplified chemical process of methylene diphenyl diisocyanate (MDI) production [START_REF] Pirkl | Process for the preparation of highly pure 2,4'-methylenediphenyldiisocyanate[END_REF] as case study for exemplary application and evaluation of our modeling approach. MDI as a base product of polyurethanes is one of the most produced isocyanates. It can be generated by condensation of aniline and formaldehyde to methylenedianiline (MDA) using hydrochloric acid (HCl) as catalyst followed by phosgenation of the MDA. Using the highly dangerous phosgene, the process is well-suited to study our domain model in a safety-critical environment. As shown in Fig. 4, phosgene and HCl must be separated from the crude MDI after the phosgenation in a distinct subprocess "phosgene separation", on which we focus in our case study. The separation of phosgene, HCl, MDI and the solvent chlorobenzene (MCB) can be realized by distillation, as schematically shown in Fig. 5. The feed mixture F enters the column in liquid state and flows towards the base of the column which is continuously heated by circulation of the base product (MCB and MDI) through a steam reboiler. This leads to vaporization of phosgene, HCl and parts of the MCB, forming a vapor flow V towards the head of the column. This head product exits the column and enters a condenser, which cools down the vapor to liquefy MCB and phosgene while extracting the gaseous HCl. MCB and phosgene are then stored in an output tank and directed towards other subprocesses. In a non-ideal distillation column, the vapor emerging at the column bottom contains both the lighter and heavier compound. To reduce this mixing and to obtain higher purity of base and head product, column floors and a partial reflux L from the output tank to the column are installed. When the steam meets with the reflux at a certain floor, it partly condenses whereat mostly the heavier compound is liquefied. The condensing energy contrarily causes the vaporization of the lighter compound in the reflux.

Aniline

MDA Production

Moving towards the column head, this effect is multiplied by introducing additional floors to reach a desired level of purity. Typical distillation columns are controlled using five control To obtain stable column operation, the levels at the column base (LC 1 ) and the output tank (LC 2 ) as well as the column pressure (P C) are controlled. The product quality is defined by the desired separation between the compounds in both base and head product (distillate). Control schemes for distillation columns are commonly named after the variables used to control the product quality. In our case study, we apply the LV control scheme, which controls the head product composition by the reflux (F C 1 controlling L) and the base product composition by the flow of steam to the reboiler (F C 2 controlling V). To reduce the size of our case study, we evaluate our aspect-oriented modeling approach focusing on condenser and output tank of the distillation. In the following section, we introduce both process steps and derive a state space representation to which we apply our approach.

B. State Space Representation

Control algorithms in process automation are designed based on system models either deduced from physical characteristics of the controlled process or aggregated from measurements. The variables and detail of the model must be adapted to the actual control task. In our case study, the safety-relevant criterion of the condenser is the complete liquefaction of phosgene, warranted if the condenser cools the head product lower than the boiling point of phosgene at 7.44 degrees Celsius. The controlled variable in the condenser is the mass flow w c of the coolant. We abstract the behavior of the condenser with that of a heat exchanger:

Ṫ hp = w hp m hp T hp0 - w hp m hp T hp (t) - kAT hp (t) m hp c hp + kATc(t) m hp c hp Ṫc = wc mc Tc0 - wc mc Tc(t) + kAT hp (t) mccc - kATc(t) mccc (3)
where Ṫ hp and Ṫc are the time-derivatives of the head product and coolant temperatures after condensing, k is a constant of the heat exchanger describing its ability to transfer energy, A is the area of the heat exchanger, m hp and m c are the masses, c hp and c c the heat capacities, w hp and w c the mass flows and T hp0 and T c0 the temperatures at the entry point of the condenser of the head product and coolant, respectively. The change in head product temperature depends on the heat transfer between product and coolant as well as on their initial temperatures. For controlling the head product temperature by manipulating the mass flow of the coolant, we rewrite the second equation for T c (t) and insert it into the first to obtain a non-linear equation for the dependency of Ṫ hp and w c . To facilitate control and verification activities we generate a linear state space representation of the form

∆ ẋt = A∆x(t) + B∆u(t) + E∆d(t) ∆y(t) = C∆x(t) + D∆u(t) (4)
where

A = 0 - w hpR ccw cR kA -w hpR -ccw cR c hp -kA c hp kA mccc -w cR mc -kA m hp chp B = - w hpR ccT cR kA + w hpR ccT c0 kA -ccT cR c hp + ccT c0 c hp Tc0 -TcR C = 1 0 D = 0 E = T hp0R -ccw cR T cR kA -TcR + ccw cR T c0 kA w hpR m hp 0 0 (5)
Variables with the index R are fixed in the operation point. While more complex models for condensing processes exist (see e.g. [START_REF] Shah | Dynamic modeling and control of single and multi-evaporator subcritical vapor compression systems[END_REF]), we use this abstracted form to keep the size of the verification problem manageable for our case study. The output tank is the second process step covered by our case study. The critical process variable concerning functional safety is the level of the distillate h(t) inside the tank which is controlled by LC 2 via the valve F C D . The level is influenced by the input q c from the condenser, the reflux q r to the column and the output flow q D :

qc = V fc * dc(t) qr = kr * dr(t) 2gh(t) qD = kD * u(t) 2gh(t) (6)
The flows are defined by the opening of the corresponding valve (d c (t), d r (t), u(t) ∈ [0..1]) and the constants k r , V f c , k D defining the maximum flow at the entry and exit points of the flow. For the level control, d c (t) and d r (t) are disturbances and the input u(t) is located at F C D . q r and q D are dependent on the current level h(t) according to Torricelli's law. The timederivative ḣ is given by the non-linear equation

ḣ = qc -qr -qD AT (7)
which can be linearized to a linear state space model in the form of (4) where ∆x(t) = ∆y(t) = ∆h(t) and

A = 1 A T √ 2g 1 2 √ h R (krdrR + kDuR) B = -1 A T kD √ 2g √ hR C = 1 D = 0 E = V fc A T -1 A T krR √ 2g √ hR hR = -V fcdcR (-krdrR -kDuR) √ 2g (8)

C. Modeling the CPS

Focusing on the condenser and output tank of the phosgene separation, we first model the control systems PC and LC 2 from Fig. 5 excluding data and functional safety. Both span over the subsystem and component layers of abstraction. The connection between the continuous state space models of condenser and tank introduced in section V-B and the behavior of their control systems is established on the subsystem layer using hybrid automata as defined in [START_REF] Henzinger | The theory of hybrid automata[END_REF]. The states V of a hybrid automaton H = X, V, E, init, inv, f low, jump, event, Σ represent control modes defining the continuous flow of real number variables X, while the transitions E specify discrete mode switches. The labeling functions init, inv, flow and jump assign predicates to each control mode v i , where init assigns initial values to the variables of v i , inv defines invariants for the variables, flow specifies the continuous change of variable values within a control mode and jump defines conditions for control switches. The function event assigns a triggering event from the set Σ of events to each control switch. In our domain model, the automata of a subprocess can exchange signals and change their control modes by the discrete event of receiving a signal and by the violation of a state invariant. Figure 6 shows the hybrid automaton of the condenser, whose control state defines the control algorithm of the condenser in Similar to the condenser, the behavior of the output tank on subsystem level is defined as hybrid automaton shown in Fig. 7. During regular operation, the automaton controls the level of the output tank via the valve F C D , as defined in [START_REF] Khaitan | Design techniques and applications of cyberphysical systems: A survey[END_REF].

                           ) ( ) ( ) ( ) ( ) ( 0 t T t w E t Bw t T t T A T T hp hp c c hp c hp   FCSF1==1 SFC2_switchover Inv Control 1 1 FCSF SF v C F    FCSF1==0 temp_control Δy(t)=ΔThp(t)

Δy(t)=ΔThp(t) Δwc(t)=kc(w(t)-Δy(t)) Δwc(t)=kc(w(t)-Δy(t))

SFC2_switchback Inv Control 1 1 FCSF SF v C F   temp_control Δy(t)
In our domain model, the component layer as lowest layer of abstraction specifies the implementation of the control algorithms defined on the subsystem layer. Fig. 8 shows the deployment structure of the condenser and output tank. The condenser consists of five nodes which are containers for groups of hardware units connected by communication links and typically contained in a separate housing. Three of the nodes are vortex sensors which count the vortexes in the Kármán vortex street behind a bluff body in the pipe to measure the flow speed. The structural model of a vortex node in our domain model consists of a sensor (e.g. piezo elements or a physical switch) for vortex counting, pressure and temperature sensors for mass flow calculation, a vortex algorithm software calculating the mass flow from the vortex frequency f as well as software components for inter-node data management and communication. Condenser Vortex1 and Condenser Vortex2 measure the mass flow w hp and the temperature T hp0 , while Condenser Vortex3 measures the incoming mass flow w c and temperature T c0 of the coolant. The node Condenser Temp1 contains two temperature sensors measuring the temperature T hp of the distillate. In addition to the three sensor nodes, the converter includes a node with two microcontroller units (MCUs) running the software components for the temperature control algorithm and the actual valve control. The converter controls the valve nodes FCC, FCSF1 and FCSF2.

The output tank in our case study consists of three nodes: two radar level sensor nodes Tank Radar1 and Tank Radar2 as well as the Tank converter node which runs the level control algorithm and controls the valve F C D . The nodes of the converter and the tank are connected using a bus system while the connections between valves and control nodes are realized via point to point links.

On the component level the behavior of each control mode from the hybrid automaton on the subsystem level is modeled 7. Behavior of the Output Tank Control System on Subsystem Level as activity diagram defining the control and data flows between the control system entities in this specific mode. Each of the activities carried out by an entity can additionally be detailed by a distinct activity diagram. Fig. 9 partly shows the activity diagram for the control mode of the condenser. The grey actions mark the standard behavior of the control system while the dotted flows and white activities are weaved from the safety aspect as described in section V-D. The mass flow w hp1 is calculated from the vortex frequency f hp1 and the temperature T hp0 1 and transferred via the bus using the action transferSR denoting safety-critical communication. Together with the current temperature value T hp , the temperature control calculates a control input controlF C C which is adjusted in the ValveControl module of the valve F C C .

ECond_T_high | FCSF1==0 control SFOT3_output_closing FCD D v C F    E C o n d _ c o n t r o l & h ( t ) = = 0 ECond_control & h(t) > 0 h(t)==0 FCSF2==1 & h(t) ≥ hmin + hysteresis ESFOT2_Timeout ECond_control | FCSF1==1 /!Eout_control h(t) ≥ hmin + hysteresis h(t) ≤ hmin Safety Function SFOT4 /!Eout_control
             ) ( ) ( * ) ( 2 t F C t F C E F C B t h A h R SF D  tSFOT2_5: FCSF2==1 FCD>0 tSFOT2_4: ECond_control | FCSF1==1 Operation Safety Functions SFOT2, SFOT3 SFOT4_output_closing Control level_control FCD D v C F    Inv Δy(t)=Δh(t) FCD>0 SFOT4_output_closed Control level_control 0  D C F  Inv Δy(t)=Δh(t) FCD=0 h(t)==0 & FCD ≠ 0 tSFOT4_3: h(t) ≠ 0 & FCD==0 Control level_control: Δy(t)=Δh(t) FCSF1>0 Inv SFOT2_input_closing Control level_control Inv Δy(t)=Δh(t) FCSF2>0 2 2 FCSF SF v C F    SFOT2_input_closed Control level_control Inv Δy(t)=Δh(t) 0 2  SF C F  SFOT2_input_opening Control level_control Inv Δy(t)=Δh(t) 2 2 FCSF SF v C F   FCSF2<1 Control level_control Δy(t)=Δh(t) 2 2 FCSF SF v C F    Inv SFOT3_input_opening 0  D C F  FCD=0 Control level_control Δy(t)=Δh(t) 2 2 FCSF SF v C F   Inv FCD==0 tSFOT3_2: SFOT3_output_closed FCD=0 Control level_control Δy(t)=Δh(t) 2 2 FCSF SF v C F    Inv 0  D C F  SFOT3_tank_draining FCD=0 Control level_control Δy(t)=Δh(t) 2 2 FCSF SF v C F    Inv 0  D C F  FCSF2=0 Fig.

D. Modeling Safety Aspects

Complementing the system specification, we use safety aspect models to define the safety functions of condenser and tank on the subsystem layer of abstraction as well as their realization on the component layer. To demonstrate the specification of hardware failures and their tracing to detection methods, we apply the safety concept of 2-channel redundancy by structural and behavioral weaving to the condenser domain model. The safety functions of condenser and output tank are closely coupled. SF C 1 in the condenser ensures that the HCl which is used in other processes or even sold to contractors is not contaminated with phosgene. To prevent this, P C continuously controls pressure and temperature T hp by manipulating the incoming mass flow w c of the coolant. A demand on the safety function SF C 2 occurs when T hp rises above 7.44 degrees Celsius due to insufficient cooling. In this case, the safety function assumes that phosgene has not been completely liquefied and is flowing as gas towards the valve F C SF 1 . SF C 2 must close the valve before phosgene exits. The resulting effect is a mixture of HCL and phosgene leaving the condenser towards the output tank. The output tank has four distinct safety functions. SF OT 1 continuously controls the tank level via the valve F C D . SF OT 2 reacts on the flow of HCl towards the output tank evoked by the triggering of SF C 2 by closing the valve F C SF 2 before HCl can enter the tank, directing the complete As introduced in section III, our domain model extends the behavioral specification of the system models using the weaving functions addBehavior and removeBehavior. Fig. 6 shows the behavioral extension of the condenser automaton by the behavior of the safety functions from Table I fires and the tank level decreases due to the reflux to the column. The safety function waits for the signal E Cond control which announces regular condenser operation with complete separation of HCl and phosgene. If at this point in time the tank still contains HCl and phosgene, SF OT 3 enters the state tank draining and waits for h(t) to decrease to zero. If h(t) equals zero, the safety function reopens F C SF 2 in the state input opening, filling the output tank with phosgene, and returns to normal operation via t SF OT 3 6 when the level rises above a minimum threshold h min + hysteresis. The safety function SF OT 4 ensures that the output valve F C D is closed when the tank level h(t) decreases to zero to prevent damage to following subprocesses. The demand for the safety function is a decrease of h(t) below a configurable threshold h min which causes firing of the transition t SF OT 4 1 . In the state output closing, SF OT 4 closes the valve F C D . If F C D is completely closed, the safety function waits in the state output closed for the tank level to rise over the minimum threshold with hysteresis and switches back to normal operation via t SF OT 4 4 . If however the tank level decreases to zero before F C D is completely closed, a safety-critical error Err Lvl occurs representing the failure of SF OT 4 in preserving a safe system state for the process step. The safety functions of condenser and output tank have to react by transferring their process step into a safe state during the interval between the occurrence and the consequence of dangerous events referred to as process safety time. Fig. 10 shows the safety automaton of condenser and output tank. As described in section III, in addition to the modes of operation the safety automaton defines the process safety times and safety-critical errors for each safety function. For SF C 2, the automaton defines the safety time tsaf e SF C2 whose violation leads to the critical error Err F C SF 1 , and the chained safety times tsaf e SF OT 2 and tsaf e SF OT 3 leading to the error state Err F C D . Section V-F argues that the occurrence of these safety-critical errors depends on the configuration on both subsystem and component layer and uses the automaton in Fig. 10 to define a reachability problem supporting the prove of correct system configurations regarding functional safety. To support reuse and reduce modeling complexity, the safety aspect defines safety concepts which can be used to implement safety functions. These safety concepts are weaved into both structural and behavioral models on the component layer. Fig. 11 shows the structural aspect model of the safety concept "2-channel" which introduces a system of two sensors, two processing units and two actuators. The sensors send a dynamic data item to both processing units where they are compared by software modules. The comparison modules on each processing unit then calculate a derived data item and exchange it to verify the calculation on each MCU. Each of the processing units controls an actuator connected to the same physical process. This safety concept introduces redundancy to safety-related control tasks. Fig. 8 shows the weaving of the 2-channel safety concept to the condenser control structure. Both the node Condenser Vortex2 and the processing units VortexMCU2 and ControlMCU2 and the corresponding bus channels are part of the 2-channel safety concept added to the model via the weaving function addEntity. Well formedness rules ensure the correct binding of aspect and domain models using the types of the elements in the aspect model as reference.

0 2  SFOT t  SFOT2 1 2  SFOT t  0 3  SFOT t  0 4  SFOT t  FCSF1==0 SFOT3 0 2  SFOT t  1 3  SFOT t  Err_FCD /!ESFOT3_Timeout /!ESFOT2_Timeout 0 3  SFOT t  FCSF1==1 FCSF1==1 & FCSF2==1 & h(t) ≥ hmin + hysteresis 0 2  SFC t  SFC2 1 2  SFC t  Err_FCSF1 /!ESFC2_Timeout 0 2  SFC t  FCSF1==0 tSFC2 ≥ tsafeSFC2 Thp(t) > Thp_max /tSFC2=0 /tSFOT2=0 tSFOT2 ≥ tsafeSFOT2 /tSFOT3=0 tSFOT3 ≥ tsafeSFOT3
The hardware failure information introduced in section III can be used on the component level to document the identified failure modes from a safety analysis and trace their implemented countermeasures to support system certification. In Fig. 8 this is illustrated using the failure dataCorruption which occurs at the memory of VortexMCU1 and leads to a dangerous failure with the rate λ D = 1.7 * 10 -9 . The 2-channel safety concept acts as diagnostic measure against the dataCorruption error with a diagnostic coverage DC D of 90% regarding dangerous failures.

Complementing the structure, a behavioral description of safety concepts is part of the aspect models as shown for the 2-channel concept in Fig. 12. The activity diagram defines the cross-verification data exchange between the concept entities. An exemplary weaving of the safety concept is shown in the activity diagram of the condenser in Fig. 9 oriented approach improves the accessibility of common safety patterns like the 2-channel approach to domain experts without explicit safety knowledge and encourages extended reuse from implementation to documentation and certification artifacts when reusing complete safety concepts.

E. Modeling Data Aspects

We use the data aspect to add configurability to condenser and tank on subsystem and component level and demonstrate how a specific configuration can be defined and bound to the domain models. On the subsystem level, the aspect focuses on the parameters of process steps and their safety functions, providing a process owner's point of view. The major part of the data represent customization and data processing of the CPS parts realizing the process control on the component level. Similar to the safety aspect, weaving functions connect device variables and static data items with the behavioral and structural models on both layers, where the weaving on component level corresponds to the customization of a mass market device to a specific application. The hybrid automata on the subsystem layer use device variables in their flow equations and static data items in transition guards and invariants. The weaving function addData connects the device variables and static data items from the data aspect to the variables and constants of the hybrid automata. Fig. 6 shows the connection of the device variable T hp and its configuration data item Conf T hp as well as the maximum value T hp max to the condenser automaton. This reduced data set shows that inline modeling of all configuration data values would magnify the complexity of behavioral models beyond the point of efficient handling. Using our aspect-oriented approach, we promote to hold complete data models externally, e.g. in a separate database and trace the connections to the variables in the automata via the aspect weaving. On the component layer, the origin of the device variables introduced in the hybrid automata is defined by connecting the device variables to producing software modules in the structural and deployment viewpoint using the weaving function producedBy. Dependent on their scope, the device variables are then distributed to all data management modules in the scope of the device variable. Fig. 8 illustrates the source modules of device variables by the labels of their outgoing links. Hardware-related characteristics used by software modules are bound to the respective hardware unit or link via the addData weaving function, configuration of software modules is done using the function configure. In Fig. 8, the construction variable bluff body width of the vortex sensor C V 3 is defined using the static data item bluffBodyWidth and the baudrate of the bus system connecting the nodes is set using the data item bus1Baudrate. The storage and replication of static data items is defined in the structural models of the component by the weaving functions replicate and deploy, as shown in Fig. 8 for the example of the maximum temperature at the condenser T hp max , which is deployed at TempMCU1 of the condenser and replicated to ControlMCU1. Configuration data influences the behavior of the control system on the component layer by manipulating the control flows of the overview and detailed activity diagrams. The scope and distribution settings of device variables can add sending behavior via the addBehavior weaving function as shown in Fig. 9 for w hp1 . The common case of behavioral manipulation is the binding of activities and control paths to device variables as shown for the control state of the tank subsystem in Fig. 13.

F. Model-based Verification

During our case study, we focused on inconsistencies arising from the interdependence between the influences of data and safety aspects on the domain model. The configuration of a domain model via the data aspect can lead to an unsafe system due to structural and behavioral configuration errors. Structural inconsistencies are static misconfigurations which prevent correct system execution, arising from the weaving of the data aspect into domain models with varying complexity. They can be mitigated using the well-formedness rules connected to the weaving functions of our aspect models. For example in the hardware and deployment viewpoint, the safety aspect adds wfrs that constrain the deployment of elements to safety considerations:

W f r sil deploy W f r sil deploy W f r sil deploy : ∀depi ∈ Deployee, dci ∈ DeployContext : (depi, dci) ∈ deploy → sil(depi) ≤ sil(dci) (9)
wf r sil deploy ensures that elements dep i may only be deployed on hardware or partitions dc i that have a SIL high enough to provide the safety demanded by dep i . Additional wfrs restrict the control of safety-related actuator and sensor hardware. In our case study, the deployment of device variables to producing modules in Fig. 8 must be checked using wfrs that guarantee that the producing software modules of sr device variables are sr themselves, have a sil equal or higher than those of the device variable and are deployed on an appropriate hardware unit.

Apart from these errors within the scope of a single viewpoint, more complex scenarios arise when interactions of multiple system parts defined on multiple views must be considered. Inconsistencies arising due to the influence of data items on the system behavior are more difficult to detect. As illustrated in Fig. 10, safety functions of a control system must mitigate risks within the process safety time defined in the hybrid automata on the subsystem layer from the process owner's point of view. In contrast to this, device vendors deliver systems which are highly configurable via data items manipulating structure and behavior on the component layer. As motivated before, this raises the problem of verifying that a system configuration given by an instanced data model does not prevent the safety functions from transferring the system into a safe state in case of a dangerous event within the safety time. A longer query interval of the valve value F C SF 1 due to energy restrictions e.g. leads to longer activation and thus shorter available reaction time of the safety function SF OT 2.

To detect and prevent these error scenarios, we propose to extend the activity diagrams on the component layer by worst case execution times (WCET) determined for each action and accumulated for activities in the overview activity diagrams. Since every state in the hybrid automaton of a control system is represented by a distinct overview activity diagram at the component layer, the accumulated execution times of a diagram iteration can be interpreted as the WCET of a transition exiting the corresponding state in the hybrid automaton of the control system. Through the manipulation of control flows in activities, the influence of static data items and device variables on the WCET becomes traceable and can be automatically evaluated from the activity diagrams, specifying the correlation between data and execution time. Fig. 13 shows excerpts from the tank and safety automaton and the overview activity diagram of the tank control state. In the example, the data-including WCET of the transition t SF OT 2 1 is 393.5ms. This delay is added to the counter t SF OT 2 in the safety automaton which models the occurrence of a safety-critical error in case of a safety timeout. Note that the timer in the safety automation starts at the condition F C SF 1r == 0 which references the real value of the valve independent of control system delays. Using this approach, the ability of a control system to perform its safety functions within the safety time under a given configuration can be expressed as reachability problem, where the error states of the safety automaton may not be reached by the configuration under test. When moving from our simple example to more complex models, e.g. the 2-channel safety scheme weaved into the condenser behavior in Fig. 9, the need for automated verification becomes obvious. Such a verification approach must prove that the error states of the system, e.g. Err F C D in Fig. 13, can never be reached given the influences of the data configuration on the execution times of the hybrid automata. Existing approaches use overapproximation of the continuous flows inside the automata states to manage termination and execution time and space. We currently investigate the application of the tool SpaceEx which was used by Frehse et. al. in [START_REF] Frehse | Formal analysis of timing effects on closed-loop properties of control software[END_REF] for control system verification to our data-driven approach.

VI. CONCLUSION AND FUTURE WORK

In this paper, we extend our domain model for hierarchical modeling of CPS in industrial automation introduced in [START_REF] Kuschnerus | A hierarchical domain model for safety-critical cyber-physical systems in process automation[END_REF] by defining comprehensive aspect models for the cross-cutting concerns of functional safety and data. Both aspects are key concerns in process automation systems. We use the concepts of weaving functions and well-formedness rules to give a concise definition of the valid connections between aspect and domain models, providing a baseline for isolated formal reasoning about data and safety. We apply our aspect models to a case study on the development of an industrial CPS in MDI production, focusing on the conflicts between functional safety and configurability. We identify possible consistency conflicts due to the interdependence between safety and data aspects and the domain model. Based on our case study, we propose approaches for static and dynamic verification of the safety of given configurations and deduce the need for algorithmic support for monitoring and configuring large-scale industrial safety-critical CPS. Future work includes the formal definition of configuration and data conflicts in industrial CPS and research on algorithms enabling offline and online monitoring of configurations conflicting with the functional safety of the CPS.

Fig. 1 Fig. 1 .

 11 Fig. 1. Scope of the safety aspect

Fig. 2 .

 2 Fig. 2. Safety modes introduced by the safety aspect

Fig. 3 .

 3 Fig. 3. Basic data model defined by the data aspect

Fig. 4 .

 4 Fig. 4. Schematic Overview of MDI Production

Fig. 5 .

 5 Fig. 5. Schematic Overview of Phosgene Separation by Distillation loops.To obtain stable column operation, the levels at the column base (LC 1 ) and the output tank (LC 2 ) as well as the column pressure (P C) are controlled. The product quality is defined by the desired separation between the compounds in both base and head product (distillate). Control schemes for distillation columns are commonly named after the variables used to control the product quality. In our case study, we apply the LV control scheme, which controls the head product composition by the reflux (F C 1 controlling L) and the base product composition by the flow of steam to the reboiler (F C 2 controlling V). To reduce the size of our case study, we

FCCFig. 8 .

 8 Fig. 8. Deployment Diagram of the Condenser Control System

Fig. 9 .

 9 Fig. 9. Weaving of 2-Channel Concept into Condenser Behavior

  safe_operation

Fig. 10 .Fig. 11 .

 1011 Fig. 10. Safety Automaton of Condenser and Output Tank

Fig. 13 .

 13 Fig. 13. Dynamic Verification

  The dependable transfer of safety-related data must be ensured by safe communication channels in safety-critical CPS. The applicability of a channel for transporting data of a specific SIL is influenced by the bit error probability of the underlying hardware link as well as qualitative and quantitative communication measures modeled by the safety aspect both in the deployment and communication viewpoints. Safety-critical CPS typically adapt their behavior according

				[!check successful]		DU / SD / SU error
	Startup	error detected	Nonsafe Operation	mode change	Safety Check	[check successful]	Safe Operation
							DD error detected
			error resolved	Maintenance Mode	!error resolved service attempt	State Safe Error

  Behavior of the Condenser Control System on Subsystem Level safe operation mode, where the mass flow of the coolant w c is controlled to keep the temperature T hp below T hp max . The control system in our case study uses a proportional controller ∆w c (t) = k c (w(t) -∆y(t)) which multiplies the comparison of reference variable w(t) and output ∆y(t) by a factor k c . The invariants of the control state define that during regular control, the HCl output valve F C F S1 is constantly open and the temperature ∆T hp is always below the threshold T hp max of 7.44 degrees Celsius.

				SFC2_overtemp
		Control
		temp_control
		Δy(t)=ΔThp(t)
		Δwc(t)=kc(w(t)-Δy(t))
		F 	C	S F	1 	0
	FCSF1>0	Inv		FCSF1=0
	ΔThp(t)≤Thp_max & FCSF1=1
	=ΔThp(t)
	Δwc(t)=kc(w(t)-Δy(t))
	FCSF1<1
	Fig. 6.

TABLE I .

 I SAFETY FUNCTIONS OF CONDENSER AND OUTPUT TANK

		Process Step	Mode	Control	Description
	SF C 1	condenser	continuous	PC	temperature control
	SF C 2	condenser	on demand	PC	prevent phosgene output
	SF OT 1	tank	continuous	LC2	level control
	SF OT 2	tank	on demand	LC2, P C	prevent HCl output
	SF OT 3	tank	on demand	LC2	prevent HCl output
	SF OT 4	tank	on demand	LC2	prevent empty pipe

condenser output back to the distillation column as reflux. SF OT 3 closes the input and output valves F C SF 2 and F C D in case SF OT 2 is not successful in preventing the entry of HCl into the output tank. SF OT 3 is responsible for emptying the tank via the reflux to ensure that no HCl is put out to following subprocesses. A demand on SF OT 4 is triggered when the tank level falls below a minimum threshold. SF OT 4 is responsible for ensuring that the output valve is never opened when the tank is completely empty to prevent damage to following subprocesses caused by empty pipes. Table

I

lists the safety functions covered by our case study.

  . The safety function SF C 1 is continuously executed during safe operation in the control state of the automaton without altering the behavior. SF C 2 is executed on demand, i.e. when a dangerous event occurs that may lead to process risks which have to be mitigated. We use the weaving function addBehavior to add three additional states to the automaton that are executed by SF C 2. The demand for SF C 2 is modeled by the transition t SF C2 1 which transfers the automaton to the state switchover when the temperature T hp (t) rises above T hp max and broadcasts the signal E Cond T high . In this state, SF

C 2 closes the valve F C SF 1 at maximum speed v F CSF 1 which is denoted by the flow equation Ḟ C SF 1 = -v F CSF 1 . When the valve is completely closed, SF C 2 enters the state overtemp in which the valve F C SF 1 remains closed ( Ḟ C SF 1 = 0) so that gaseous phosgene cannot be released and the total output of the condenser flows towards the tank. When the temperature T hp (t) falls below T hp max including a hysteresis preventing

  using the weaving function addBehavior to add entities, activities, control and data flows to the original behavior with correspondence to the safety concept ensured by well-formedness rules. The aspect-

	Sensor1	Sensor2	Comparison1	Comparison2	Actuator1	Actuator2
	measure	measure
	m1	m2
	process	process
			compare
						compare
					[m1 m2] [m1 m2]
			[else]	safetyReaction	[else]
			calculate	calculate
			derived m1	derived m2
			dm1	m2,dm2	m1,dm1	dm2
			calculate	calculate
			derived m2	derived m1
			compare	compare
				[dm1 dm2] [dm1 dm2]	[else]	adjust
			[else]		safetyReaction
							adjust
	Fig. 12. Behavioral Aspect Model for Safety Concept "2-Channel"

  The device variable w hp1 e.g. is produced at the vortex sensor Condenser Vortex1, and transferred to both Control MCUs of the condenser where it is compared before further processing (see Fig.8 and 9). If one of the compared w hp values is configured with a narrow scope, it is not transferred and thus not usable by the comparison module. In addition, static inconsistencies can arise due to influence of both data and safety aspects on the same domain model elements. During our case study, this conflict occurred in combination with check and update dependencies of data items. Check dependencies ensure that the configuration of a data item d 1 is only accepted by the system if the attached data items d 2 ..d n perform checks including range compliance on their values. If the safety aspect however removes parts of an activity diagram by the weaving function removeBehavior to which the dependent data item d i>1 is attached, data item d 1 cannot satisfy its check dependencies and thus cannot be configured. In industrial scale CPS with multiple processes and control loops, even the basic single-view cases discussed above become critical and the set of possible inconsistencies are not manually controllable. Our case study therefore confirms the need for algorithmic support to concisely monitor the structural consistency of safety and data aspects with respect to the domain model during system development and operation.


Jean-Gabriel Luque

Macdonald polynomials at t = q k

Keywords: Symmetric functions, Macdonald polynomials, q-discriminant 1365-8050

We investigate the homogeneous symmetric Macdonald polynomials P λ (X; q, t) for the specialization t = q k . We show an identity relying the polynomials P λ (X; q, q k ) and P λ "

1-q 1-q k X; q, q k " . As a consequence, we describe an operator whose eigenvalues characterize the polynomials P λ (X; q, q k ).

Résumé. Nous nous intéressons aux propriétés des polynômes de Macdonald symétriques P λ (X; q, t) pour la spécialisation t = q k . En particulier nous montrons une égalité reliant les polynômes P λ (X; q, q k ) et P λ "

1-q 1-q k X; q, q k " .

Nous en déduisons la description d'un opérateur dont les valeurs propres caractérisent les polynômes P λ (X; q, q k ).

Introduction

The Macdonald polynomials are (q, t)-deformations of the Schur functions which play an important rôle in the representation theory of the double affine Hecke algebra [START_REF] Lascoux | Yang-Baxter graphs, Jack and Macdonald polynomials[END_REF][START_REF] Macdonald | Affine Hecke algebra and orthogonal polynomials[END_REF] since they are the eigenfunctions of the Cherednik elements. More precisely, the non-symmetric Macdonald polynomials are the eigenfunctions of the Cherednik elements, but the symmetric Macdonald polynomials are the eigenfunctions of the symmetric functions in the Cherednik elements. The polynomials considered here are the homogeneous symmetric Macdonald polynomials P λ (X; q, t) and are the eigenfunctions of the Sekiguchi-Debiard-Macdonald operator M 1 . For (q, t) generic, the dimension of each eigenspace equals 1 and each Macdonald polynomial is characterized (up to a multiplicative constant) by the associated eigenvalue of M 1 . That is no longer true when t is specialized to a rational power of q (note that the case of the specialization t n q m = 1n and m being integerhas been investigated by Feigin et al. [START_REF] Feigin | Symmetric polynomials vanishing on the shifted diagonals and Macdonald polynomials[END_REF] in their study of ideals of symmetric functions defined by vanishing conditions). Hence, it is more convenient to characterize the Macdonald (homogeneous symmetric) polynomials by orthogonality (w.r.t. a (q, t)-deformation of the usual scalar product on symmetric functions) and by some conditions on their dominant monomials (see e.g. [START_REF] Macdonald | Symetric functions and Hall polynomials[END_REF]). In this paper, we consider the specialization t = q k where k is a (strictly) positive integer. One of our motivations is to generalize an identity of [START_REF] Belbachir | Hankel hyperdeterminants, rectangular Jack polynomials and even power of the Vandermonde[END_REF], which shows that even powers of the discriminant are rectangular Jack polynomials. Here, we show that this property follows from deeper relations between the Macdonald polynomials P λ (X; q, q k ) and P λ 1-q 1-q k X; q, q k (in the λ-ring notation). This result is interesting in the context of the fractional quantum Hall effect [START_REF] Laughlin | Anomalous Quantum Hall Effect: An Incompressible Quantum Fluid with Fractionally Charged Excitations[END_REF], since it implies properties of the expansion of the powers of the discriminant in the Schur basis [START_REF] Di Francesco | Laughlin's wave functions, Coulomb gases and expansions of the discriminant[END_REF][START_REF] King | The square of the Vandermonde determinant and its qgeneralization[END_REF][START_REF] Scharf | Powers of the Vandermonde determinant and the quantum Hall effect[END_REF]. It implies also that the Macdonald polynomials (at t = q k ) are characterized by the eigenvalues of an operator M (described in terms of isobaric divided differences) whose eigenspaces are of dimension 1.

The paper is organized as follows. After recalling notations and background (Section 2) related to Macdonald polynomials, we give, in Section 3, some properties of the operator which substitutes a complete function to each power of a letter. These properties allow us to show our main result in Section 4 which is an identity involving the polynomial P λ (X; q, q k ) and P λ 1-q 1-q k X; q, q k . As a consequence, we describe (Section 5) an operator M whose eigenvalues characterize the Macdonald polynomials P λ (X; q, q k ). Finally, in Section 6, we give an expression of M in terms of the Cherednik elements.

Notations and background

We recall here the basic definitions and classical properties of the symmetric functions and the Macdonald polynomials.

Symmetric functions

Consider an alphabet X (potentially infinite). Following [START_REF] Lascoux | Symmetric function and combinatorial operators on polynomials[END_REF] we define the symmetric functions on X by the generating functions of the complete homogeneous functions S p (X),

σ z (X) := i S i (X)z i = x∈X 1 1 -xz .
The algebra Sym of symmetric functions has a λ-ring structure [START_REF] Lascoux | Symmetric function and combinatorial operators on polynomials[END_REF] and many properties of that structure can be understood by manipulating σ z . For example, the sum of two alphabets X + Y is defined by the product

σ z (X + Y) := σ z (X)σ z (Y) = i S i (X + Y)z i .
In particular, if X = Y one has σ z (2X) = σ z (X) 2 . This definition is extended to any complex number α by σ z (αX) = σ z (X) α . For example, the generating series of the elementary functions is

λ z (X) := Λ i (X)z i = x∈X (1 + xz) = σ -z (-X) = i (-1) i S i (-X)z i .
The complete functions of the product of two alphabets XY are given by the Cauchy kernel

K(X, Y) := σ 1 (XY) = i S i (XY) = x∈X y∈Y 1 1 -xy = λ S λ (X)S λ (Y),
where S λ denotes, as in [START_REF] Lascoux | Symmetric function and combinatorial operators on polynomials[END_REF], a Schur function. More generally, one has

K(X, Y) = λ A λ (X)B λ (Y)
for any pair of bases (A λ ) λ and (B λ ) λ in duality for the usual scalar product , , i.e. K(X, Y) is the reproducing kernel associated to , .

Macdonald polynomials

The usual scalar product on symmetric functions admits a (q, t)-deformation (see e.g. [START_REF] Macdonald | Symetric functions and Hall polynomials[END_REF]) defined for a pair of power sum functions Ψ λ and Ψ µ (in the notation of [START_REF] Lascoux | Symmetric function and combinatorial operators on polynomials[END_REF]) by

Ψ λ , Ψ µ q,t = δ λ,µ z λ l(λ) i=1 1 -q λi 1 -t λi , (1)
where δ λ,µ = 1 if λ = µ and 0 otherwise. The family of (symmetric homogeneous) Macdonald polynomials (P λ (X; q, t)) λ is the unique basis of the symmetric functions orthogonal w.r.t. , q,t verifying

P λ (X; q, t) = m λ (X) + µ≤λ u λµ m µ (X), (2)
where m λ denotes, as usual, a monomial function [START_REF] Lascoux | Symmetric function and combinatorial operators on polynomials[END_REF][START_REF] Macdonald | Symetric functions and Hall polynomials[END_REF]. The reproducing kernel associated to this scalar product is

K q,t (X, Y) := λ Ψ λ , Ψ λ -1 q,t Ψ λ (X)Ψ λ (Y) = σ 1 1 -t 1 -q XY see e.g. [12, VI.2].
In particular, one has

K q,t (X, Y) = λ P λ (X; q, t)Q λ (Y; q, t), (3)
where Q λ (X; q, t) is the dual basis of P λ (Y; q, t) with respect to , q,t , Q λ (X; q, t) = P λ , P λ -1 q,t P λ (X; q, t).

The coefficient b λ (q, t) = P λ , P λ -1

q,t is known to be b λ (q, t) = (i,j)∈λ 1 -q λj -i+1 t λ i -j 1 -q λj -i t λ i -j+1 (5)
see [START_REF] Macdonald | Symetric functions and Hall polynomials[END_REF]VI.6]. Writing

K q,t 1 -q 1 -t X, Y = K(X, Y), (6)
one finds that P λ 1-q 1-t X; q, t λ is the dual basis of (Q λ (X; q, t)) λ with respect to the usual scalar product , .

Note that there exists an other Kernel type formula which reads

λ 1 (XY) = λ P λ (X; t, q)P λ (Y; q, t) = λ Q λ (X; t, q)Q λ (Y; q, t). ( 7
)
where λ denotes the conjugate partition of λ. This formula can be found in [12, VI.5 p329].

From equalities ( 6) and ( 3) , one has

σ 1 (XY) = K q,t 1 -q 1 -t X, Y = λ Q λ 1 -q 1 -t X; q, t P λ (Y; q, t). (8)
Applying [START_REF] Korányi | Hua-type integrals, hypergeomatric functions and symmetric polynomials[END_REF] to

σ 1 (XY) = λ -1 (-XY), one obtains σ 1 (XY) = λ (-1) |λ| Q λ (-X; t, q)Q λ (Y; q, t). (9)
Identifying the coefficient of P λ (Y; t, q) in ( 8) and ( 9), one finds the following property.

Lemma 2.1

Q λ (-X; t, q) = (-1) |λ| P λ 1 -q 1 -t X; q, t . (10)
Unlike the usual (q = t = 1) scalar product, there is no expression as a constant term for the product , q,t when X = {x 1 , . . . , x n } is finite. But the Macdonald polynomials are orthogonal with respect to an other scalar product defined by

f, g q,t;n = 1 n! C.T.{f (X)g(X ∨ )∆ q,t (X)} (11)
where C.T. denotes the constant term w.r.t. the alphabet X,

∆ q,t (X) = i =j (x i x -1 j ; q) ∞ (tx i x -1 j ; q) ∞ , (a; b) ∞ = i≥0 (1 -ab i ) and X ∨ = {x -1 1 , . . . , x -1 n }.
The expression of P λ , Q λ q,t;n is given by ([12, VI.9])

P λ , Q λ q,t;n = 1 n! C.T.{∆ q,t (X)} (i,j)∈λ 1 -q i-1 t n-j+1 1 -q i t n-j . ( 12
)

Skew symmetric functions

Let us define as in [START_REF] Macdonald | Symetric functions and Hall polynomials[END_REF]VI.7], the skew Macdonald functions Q λ/µ by Q λ/µ , P ν q,t := Q λ , P µ P ν q,t .

Straightforwardly, one has

Q λ/µ (X; q, t) = ν Q λ , P ν P µ q,t Q ν (X; q, t). ( 14
)
And classically, the following property holds (see e.g. [12, VI.7] for a short proof of this identity), Proposition 2.2 Let X and Y be two alphabets, one has

Q λ (X + Y; q, t) = µ Q µ (X; q, t)Q λ/µ (Y; q, t),
or equivalently P λ (X + Y; q, t) = µ P µ (X; q, t)P λ/µ (Y; q, t).

Equalities ( 3) and ( 7) are generalized by identities ( 15) and ( 16) as shown in [12, example 6 p.352],

ρ P ρ/λ (X; q, t)Q ρ/µ (Y; q, t) = K qt (X, Y) ρ P µ/ρ (X; q, t)Q λ/ρ (Y; q, t), (15)
ρ Q ρ /λ (X; t, q)Q ρ/µ (Y; q, t) = λ 1 (XY) ρ Q µ /ρ (X, t, q)Q λ/ρ (Y; q, t). ( 16
)
3 The substitution x p → S p (Y) and the Macdonald polynomials

Let X = {x 1 , . . . , x n } be a finite alphabet and Y be an other (potentially infinite) alphabet. For simplicity we will denote by Y the substitution

Y : x p → S p (Y), (17)
for each x ∈ X and each p ∈ Z. Let us define the symmetric function

H n,k λ/µ (Y; q, t) := 1 n! Y P λ (X; q, t)Q µ (X ∨ ; q, t)∆(X, q, t) (18)
where

X ∨ = {x -1 1 , . . . , x -1 n }. Set Y tq := 1-t
1-q Y and consider the substitution

Y tq x p = S p Y tq = Q p (Y; q, t). ( 19
)
The following result shows that H n,k λ/µ is a skew Macdonald polynomial on a suitable alphabet. Theorem 3.1 Let X = {x 1 , . . . , x n } be an alphabet, λ = (λ 1 , . . . , λ n ) be a partition and µ ⊂ λ. The polynomial H n,k λ/µ (Y tq ; q, t) is the Macdonald polynomial

H n,k λ/µ (Y tq ; q, t) = 1 n! (i,j)∈λ 1 -q i-1 t n-j+1 1 -q i t n-j C.T.{∆(X, q, t)}P λ/µ (Y, q, t) (20)
Set Y = {-y 1 , . . . , -y m , . . .} if Y = {y 1 , . . . , y m , . . .} and note that the operation Y → Y makes sense even for virtual alphabet since it sends any homogeneous symmetric polynomial P (Y) of degree p to (-1) p P (Y). One observes the following phenomenon which is obtained from Theorem 3.1 by applying the operations of the λ-ring structure.

Corollary 3.2 Let X = {x 1 , . . . , x n } be an alphabet, λ = (λ 1 , . . . , λ n ) be a partition and µ ⊂ λ. One has

H n,k λ/µ (-Y; q, t) = 1 n! (i,j)∈λ 1 -q i-1 t n-j+1 1 -q i t n-j C.T.{∆(X, q, t)}Q λ /µ (Y, t, q). (21)
Note that in the case of partitions, one has

Corollary 3.3 H n,k λ (-Y, q, t) = 1 n! (i,j)∈λ 1 -q i-1 t n-j+1 1 -q i t n-j C.T.{∆(X, q, t)}Q λ (Y, t, q) (22)
Example 3.4 Consider the following equality H 2,3 41/3 (-Y; q, t) = ( * )C.T.{∆(X, q, t)}Q 2111/111 (Y; t, q).

where X = {x 1 , x 2 }. The coefficient ( * ) is computed as follows. One writes the partition [41] in a rectangle of height 2 and length 4.

× × × × × Each × of coordinates (i, j) is read as the fraction [i, j] := 1-q i-1 t 3-j 1-q i t 2-j . Hence ( * ) = [1, 2][1, 1][2, 1][3, 1][4, 1] = (1 -t)(1 -t 2 )(1 -qt 2 )(1 -q 2 t 2 )(1 -q 3 t 2 ) (1 -q)(1 -qt)(1 -q 2 t)(1 -q 3 t)(1 -q 4 t)
4 A formula involving the polynomials P λ 1-q 1-q k X; q, q k and P λ X; q, q k Now, we suppose that t = q k with k ∈ N. In that case, the constant term C.T.{∆(X, q, t)} admits a closed form and Corollary 3.3 gives

Corollary 4.1 H n,k λ (-Y, q, q k ) = β n,k λ (q)Q λ (Y; q k , q). ( 23
)
where

β n,k λ (q) = n-1 i=0 λ n-i -1 + k(i + 1) k -1 q and n p q = (1-q n )...(1-q n-p+1 ) (1-q)...(1-q r )
denotes the q-binomial.

Example 4.2 Set k = 2, n = 3 and consider the polynomial

H 3,2 [320] (-Y; q, q 2 ) = 1 n! -Y P [32] (x 1 + x 2 + x 3 ; q, q 2 ) i =j (1 -x i x -1 j )(1 -qx i x -1 j ).
One has

H 3,2 [320] (-Y; q, q 2 ) = 1 -q 5 1 -q 8 (1 -q) 2 Q [221] (Y; q 2 , q).
Let

Ω S := 1 n! X i =j (1 -x i x -1 j ) (24)
and for each v ∈ Z n , Sv (X) = det x vj +n-j i i<j

(x i -x j ) -1 . Lemma 4.3 If v is any vector in Z n , one has Ω S Sv (X) = S v (X) := det(S vi-i+j (X)) (25)
In particular, Ω S leaves invariant any symmetric polynomial. The operator

A m := Ω S Λ n (X) -m (26)
acts on symmetric polynomials by substracting m from each part of the partitions appearing in their expansion in the Schur basis.

P 32 (X; q, t) = S 32 (X) + (-q + t) S 311 (X) qt -1 + (q + 1) qt 2 -1 (-q + t) S 221 (X) (qt -1) 2 (qt + 1) .
Hence,

A 1 P 32 (X; q, t) = (-q+t)S2(X) qt-1 + (q+1)(qt 2 -1)(-q+t)S11(X) (qt-1) 2 (qt+1)
= (-q+t)(t+1)(q 2 t-1)P11(X;q,t) (qt-1) 2 (qt+1)

+ (-q+t)P2(X;q,t) qt-1

.

Theorem 4.5 If λ denotes a partition of length at most n, one has

A (k-1)(n-1) P λ (X; q, q k ) k-1 l=1 i =j (x i -q l x j ) = β n,k λ (q)P λ 1 -q 1 -q k X; q, q k (27)
Example 4.6 Set k = 2, n = 3 and λ = [START_REF] Boussicault | Staircase Macdonald polynomials and the q-Discriminant Formal Power Series and Algebraic Combinatorics[END_REF]. One has

P [2] (x 1 + x 2 + x 3 ; q, q 2 ) i =j (x i -qx j ) = -q 3 S [6,2] + q 2 q 3 -1 q -1 S [6,1,1] + q 2 (q 5 -1) q 3 -1 S [5,3] - q(q 2 + 1)(q 5 -1) q 3 -1 S [5,2,1] - q(q 7 -1) q 3 -1 S [4,3,1] + q 7 -1 q -1 S [4,2,2] .
And,

A 2 P [2] (x 1 + x 2 + x 3 ; q, q 2 ) i =j (x i -qx j ) = q 7 -1 q -1 S [2] .
Since,

P [2] x 1 + x 2 + x 3 1 + q ; q, q 2 = q -1 q 3 -1 S [2]
one obtains

A 2 P [2] (x 1 + x 2 + x 3 ; q, q 2 ) i =j (x i -qx j ) = 1 1 q 3 1 q 7 1 q P [2] x 1 + x 2 + x 3 1 + q ; q, q 2 .
As a consequence, one has

Corollary 4.7 If λ = µ + [((k -1)(n -1)) n ], P µ (X; q, q k ) k-1 l=1 i =j (x i -q l x j ) = β n,k λ (q)P λ 1 -q 1 -q k X; q, q k .
Example 4.8 Set k = 3, n = 2 and λ = [START_REF] Kaneko | Selberg integrals and hypergeometric functions associated with Jack polynomials[END_REF][START_REF] Boussicault | Staircase Macdonald polynomials and the q-Discriminant Formal Power Series and Algebraic Combinatorics[END_REF]. One has

P [5,2] (x 1 + x 2 ; q, q 3 )(x 1 -qx 2 )(x 1 -q 2 x 2 )(x 2 -qx 1 )(x 2 -q 2 x 1 ) = q 3 S [9,2] + (1 -q 7 )(1 + q 4 ) 1 -q 5 S [7,4] - (1 -q 2 )(1 + q)(1 + q 2 )(1 + q 4 ) 1 -q 5 S [8,3] .
This implies

A 2 P [5,2] (x 1 + x 2 ; q, q 3 )(x 1 -qx 2 )(x 1 -q 2 x 2 )(x 2 -qx 1 )(x 2 -q 2 x 1 ) = (x 1 x 2 ) -2 P [5,2] (x 1 + x 2 ; q, q 3 )(x 1 -qx 2 )(x 1 -q 2 x 2 )(x 2 -qx 1 )(x 2 -q 2 x 1 ) = P [3] (x 1 + x 2 ; q, q 3 )(x 1 -qx 2 )(x 1 -q 2 x 2 )(x 2 -qx 1 )(x 2 -q 2 x 1 ).
One verifies that

P [3] (x 1 + x 2 ; q, q 3 )(x 1 -qx 2 )(x 1 -q 2 x 2 )(x 2 -qx 1 )(x 2 -q 2 x 1 ) = 4 2 q 10
2 q P [5,2] ( x 1 + x 2 1 + q + q 2 ; q, q 3 ). Remark 4.9 If µ is the empty partition, Corollary 4.7 gives

k-1 l=1 i =j (x i -q l x j ) = β n,k λ (q)P [((k-1)(n-1)) n ] 1 -q 1 -q k X; q, q k . ( 28
)
This equality generalizes an identity given in [START_REF] Belbachir | Hankel hyperdeterminants, rectangular Jack polynomials and even power of the Vandermonde[END_REF]:

i<j (x i -x j ) 2(k-1) = ( -1)
((k-1)n(n-1) 2 n! kn k, . . . , k P (k) n (n-1)(k-1) (-X),
where

P (k) λ (X) = lim q→1 P (α)
λ (X; q, q k ) denotes a Jack polynomial (see e.g. [START_REF] Macdonald | Symetric functions and Hall polynomials[END_REF]). The expansion of the powers of the discriminant and their q-deformations in different basis of symmetric functions is a difficult problem having many applications, for example, in the study of Hua-type integrals (see e.g. [START_REF] Kaneko | Selberg integrals and hypergeometric functions associated with Jack polynomials[END_REF][START_REF] Korányi | Hua-type integrals, hypergeomatric functions and symmetric polynomials[END_REF]) or in the context of the fractional quantum Hall effect (e.g. [START_REF] Di Francesco | Laughlin's wave functions, Coulomb gases and expansions of the discriminant[END_REF][START_REF] King | The square of the Vandermonde determinant and its qgeneralization[END_REF][START_REF] Laughlin | Anomalous Quantum Hall Effect: An Incompressible Quantum Fluid with Fractionally Charged Excitations[END_REF][START_REF] Scharf | Powers of the Vandermonde determinant and the quantum Hall effect[END_REF]). Note that in [START_REF] Boussicault | Staircase Macdonald polynomials and the q-Discriminant Formal Power Series and Algebraic Combinatorics[END_REF], we gave an expression of an other q-deformation of the powers of the discriminant as staircase Macdonald polynomials. This deformation is also relevant in the study of the expansion of i<j (x i -x j ) 2k in the Schur basis (for example, we generalized in [START_REF] Boussicault | Staircase Macdonald polynomials and the q-Discriminant Formal Power Series and Algebraic Combinatorics[END_REF] a result of [START_REF] King | The square of the Vandermonde determinant and its qgeneralization[END_REF]).

5 Macdonald polynomials at t = q k as eigenfunctions Let Y = {y 1 , . . . , y kn } be an alphabet of cardinality kn with y 1 = x 1 , . . . , y n = x n . One considers the symmetrizer π ω defined by πωf (y 1 , . . . , y kn ) = Y i<j (x i -x j ) -1 X σ∈S kn sign(σ)f (y σ(1) , . . . , y σ(kn) )y kn-1 σ(1) . . . y σ(kn-1) .

Note that π ω is the isobaric divided difference associated to the maximal permutation ω in S kn . This operator applied to a symmetric function of the alphabet X increases the alphabet from X to Y in its expansion in the Schur basis, since

π ω S λ (X) = S λ (Y). (29)
Indeed, the image of the monomial y i1 1 . . . y i kn kn is the Schur function S I (Y). Since π ω S λ (X) = π ω x λ1 1 . . . x λn n = π ω y λ1 1 . . . y λn n y 0 n+1 . . . y 0 kn , one recovers equality (29).

One defines the operator π tq which consists in applying π ω and specializing the result to the alphabet X tq := {x 1 , . . . , x n , qx 1 , . . . , qx n , . . . , q k-1 x 1 , . . . , q k-1 x n }.

From equality (29), one has

π tq ω S λ (X) = S λ (1 + q + . . . + q k-1 )X , (30)
for l(λ) ≤ n. Furthermore, the expansion of S λ (1 + q + . . . + q k-1 )X in the Schur basis is triangular, so the operator π tq defines an automorphism of the space Sym ≤n generated by the Schur functions indexed by partitions whose length are less or equal to n, i.e. for each function f ∈ Sym ≤n , one has

π tq f (X) = f (X tq ). (31)
In particular, Lemma 5.1 Let λ be a partition such that l(λ) ≤ n then π tq ω P λ 1 -q 1 -q k X; q, t = q k = P λ (X, q, q k ).

Consider the operator M : f → Mf defined by

M := (x 1 . . . x n ) (k-1)(1-n) π tq ω k-1 l=1 i =j (x i -q l x j ).
The following theorem shows that the Macdonald polynomials are the eigenfunctions of the operator M.

Theorem 5.2 The Macdonald polynomials P λ (X; q, q k ) are eigenfunctions of M. The eigenvalue associated to P µ (X; q, q k ) is β n,k µ+((k-1)(n-1)) n (q). Furthermore, if k > 1, the dimension of each eigenspace is 1.

Example 5.3 If n = 5, the eigenvalues associated to the partitions of 4 are

β 4,k [4 k,4 k-4,4 k-4,4 k-4,4 k-4] = h 5k-5 k-1 i q h 6k-5 k-1 i q h 7k-5 k-1 i q h 8k-5 k-1 i q h 9k-1 k-1 i q (λ = [4, 0, 0, 0, 0]), β 4,k [4 k-1,4 k-3,4 k-4,4 k-4,4 k-4] = h 5k-5 k-1 i q h 6k-5 k-1 i q h 7k-5 k-1 i q h 8k-4 k-1 i q h 9k-2 k-1 i q (λ = [
i q h 6k-4 k-1 i q h 7k-4 k-1 i q h 8k-4 k-1 i q h 9k-4 k-1 i q (λ = [1, 1, 1, 1, 0]).
6 Expression of M in terms of the Cherednik elements

In this paragraph, we restate Proposition 5.2 in terms of Cherednik operators. Cherednik's operators {ξ i ; i ∈ {1, . . . , n}} =: Ξ are commutative elements of the double affine Hecke algebra. The Macdonald polynomials P λ (X; q, t) are eigenfunctions of symmetric polynomials f (Ξ) and the eigenvalues are obtained substituting each occurrence of ξ i in f (Ξ) by q λi t n-i (see [START_REF] Lascoux | Yang-Baxter graphs, Jack and Macdonald polynomials[END_REF] for more details). Suppose that k > 1 and consider the operator M : f → Mf defined by

M := k-1 i=1 (1 -q i ) n M. (33)
From Proposition 5.2, one has MP λ (X; q, q k ) = n-1 i=0 k-1 j=1

(1 -q λn-i+k(i+1)-j )P λ (X; q, q k ).

The following proposition shows that M admits a closed expression in terms of the Cherednick elements. (1 -q l+k ξ i )f (X).

(35)

Example 4 . 4

 44 If X = {x 1 , x 2 , x 3 } and λ = [320], one has

Proposition 6 . 1

 61 One supposes that k > 1. For any symmetric function f , one has

Acknowledgments The author is grateful to Alain Lascoux and Jean-Yves Thibon for fruitful discussions. I also thank Christophe Tollu for its corrections.