Keywords: Pif1 helicase, Crystal structure, Unwinding activity, Conformational change Unwound Fraction Time

Pif1 helicases, conserved in eukaryotes, are involved in maintaining genome stability in both the nucleus and mitochondria. Here, we report the crystal structure of a truncated Candida Albicans Pif1 (CaPif1 368-883 ) in complex with ssDNA and an ATP analog. Our results show that the Q-motif is responsible for identifying adenine bases, and CaPif1 preferentially utilizes ATP/dATP during dsDNA unwinding. Although CaPif1 shares structural similarities with Saccharomyces cerevisiae Pif1, CaPif1 can contact the thymidine bases of DNA by hydrogen bonds, whereas ScPif1 cannot. More importantly, the crosslinking and mutant experiments have demonstrated that the conformational change of domain 2B is necessary for CaPifl1 to unwind dsDNA. These findings contribute to further the understanding of the unwinding mechanism of Pif1.

Introduction

Helicases are almost ubiquitous enzymes involved in multiple aspects of DNA and RNA metabolism.

Helicases are classified into 6 superfamilies, SF1 to SF6, based on the conserved helicase motifs. In each superfamily, the helicases are categorized into subgroups A and B according to the directionality of their translocation along nucleic acids [START_REF] Singleton | Structure and mechanism of helicases and nucleic acid translocases[END_REF].

Pif1, a DNA helicase of the SF1B, is widely found in eukaryotes from yeast to humans [START_REF] Chung | To peep into Pif1 helicase: multifaceted all the way from genome stability to repairassociated DNA synthesis[END_REF][START_REF] Bessler | The Pif1p subfamily of helicases: region-specific DNA helicases?[END_REF]. For example, ScPif1 (Saccharomyces cerevisiae Pif1), as the founding member of the Pif1 family, has multiple in vivo functions, such as maintaining mitochondrial DNA [START_REF] Bochman | Unwinding the functions of the Pif1 family helicases[END_REF], inhibiting telomerase [START_REF] Zhou | Pif1p helicase, a catalytic inhibitor of telomerase in yeast[END_REF][START_REF] Boule | The yeast Pif1p helicase removes telomerase from telomeric DNA[END_REF], processing Okazaki fragments [START_REF] Pike | An alternative pathway for Okazaki fragment processing: resolution of fold-back flaps by Pif1 helicase[END_REF], and resolving G-quadruplex (G4) structures [START_REF] Ribeyre | The yeast Pif1 helicase prevents genomic instability caused by G-quadruplex-forming CEB1 sequences in vivo[END_REF][START_REF] Paeschke | DNA replication through G-quadruplex motifs is promoted by the Saccharomyces cerevisiae Pif1 DNA helicase[END_REF].

Based on sequence alignments, Pif1 protein can be broadly divided into 3 parts, the central helicase core and the N-terminal and C-terminal accessory domains. Although the 2 accessory domains vary in length and sequence between species, they are required for the helicase's in vivo and in vitro functions [START_REF] Bessler | The Pif1p subfamily of helicases: region-specific DNA helicases?[END_REF]. For example, the N-terminal domain of ScPif1 is essential for Rim1's stimulation of Pif1-catalyzed strand separation activity [START_REF] Ramanagoudr-Bhojappa | Physical and functional interaction between yeast Pif1 helicase and Rim1 single-stranded DNA binding protein[END_REF]. The N-terminal domain of human Pif1 (hPif1) possesses ssDNA annealing activity [START_REF] Gu | Biochemical analysis of human PIF1 helicase and functions of its N-terminal domain[END_REF]. On the other hand, ScPif1's C-terminal domain promotes the processivity of DNA unwinding [START_REF] Singh | A Monomer of Pif1 Unwinds Double-Stranded DNA and It Is Regulated by the Nature of the Non-Translocating Strand at the 3'-End[END_REF].

The helicase core, evolutionarily conserved in various organisms, comprises 2 RecA-like domains, 1A and 2A, and 2 additional domains, 1B and 2B [START_REF] Byrd | Structure and function of Pif1 helicase[END_REF]. The 1B domain, consisting of a loop and an α-helix, is inserted into 1A; 2B, which forms an SH3-like domain, is inserted into 2A. The helicase core is the basic unit with which Pif1 protein exerts its helicase activity. During dsDNA unwinding, the 1A and 2A domains bind the 5′-tail of a dsDNA and begin to translocate along the single strand in a 5′→3′ direction driven by ATP hydrolysis [START_REF] Singleton | Structure and mechanism of helicases and nucleic acid translocases[END_REF]. In this case, 1B is believed to form a pin or wedge that splits the incoming duplex [START_REF] Dehghani-Tafti | Structural and functional analysis of the nucleotide and DNA binding activities of the human PIF1 helicase[END_REF]. In recent years, structures of Bacteroides spp. (Bs) and Thermus oshimai Pif1(ToPif1) with and without ligands binding have been solved, and domain 2B has been found to undergo a significant conformation change upon DNA and ATP binding [START_REF] Dai | Structural and functional studies of SF1B Pif1 from Thermus oshimai reveal dimerization-induced helicase inhibition[END_REF][START_REF] Zhou | Structural and Functional Insights into the Unwinding Mechanism of Bacteroides sp Pif1[END_REF][START_REF] Chen | Crystal structures of the BsPif1 helicase reveal that a major movement of the 2B SH3 domain is required for DNA unwinding[END_REF].

Here, we described a ternary complex structure of CaPif1 helicase core bound to ssDNA and ADP•AlF4.

The structural snapshots and biochemical analyses revealed some characteristics of CaPif1 in dsDNA unwinding, ssDNA binding, and ATP hydrolysis.

Materials and methods

Protein expression and purification

The gene encoding the Candida albicans Pif1 helicase core (CaPif1 368-883 , "CaPif1" for short) was generated by PCR and cloned into a modified pET-15b vector (Invitrogen) with an N-terminal SUMO tag to generate His-SUMO-CaPif1. The construct was transformed into E. coli C2566H (New England Biolabs). The cells were grown in LB medium containing 100 μg/mL ampicillin at 37°C to OD600 of 0.7 and induced with 0.4 mM IPTG at 18°C for an additional 16 h. The cells were then harvested, resuspended in a lysis buffer [25 mM Tris-HCl (pH 7.8), 500 mM NaCl, 10% (v/v) glycerol, 5 mM imidazole and 1 mM EDTA], homogenized with a French press (1000 bar) 3 times, and sonicated 2-3 times to shear their DNA. After centrifugation and filtration using a 0.45-mm membrane, the clarified cell lysate was loaded onto a cOmplete His-Tag Purification Column (CHTPR, Roche) equilibrated with the lysis buffer at 18°C. His-SUMO-CaPif1 was eluted in a gradient increased to 300 mM imidazole over 20 column volumes (cv). The identified fractions were incubated with SUMO protease and dialyzed with the dialysis buffer [25 mM Tris-HCl (pH 7.6), 500 mM NaCl and 10% (v/v) glycerol] at 18°C overnight. Protein was then diluted to 150 mM NaCl with the dilution buffer [25 mM Tris-HCl (pH 7.6), 20 mM NaCl, 10% (v/v) glycerol and 1 mM EDTA], loaded on a 5-ml HiTrap SP HP column (GE Healthcare), and eluted with a 100-ml gradient of 150-1000 mM NaCl in the same buffer. The purified protein fractions were concentrated to 10 mg/mL and exchanged into the storage buffer [25 mM Tris-HCl (pH 7.6), 500 mM NaCl and 30% (v/v) glycerol]. The purification of CaPif1 C426A and CaPif1 C662A followed the same protocol as that for the wide-type CaPif1.

Crystallization

The CaPif1 protein at 10 mg/mL in 100 mM NaCl, 20 mM Tris-HCl (pH 7.6), 2 mM MgCl2, and 1 mM DTT was mixed with poly(T8) DNA (5′-TTTTTTTT-3′) at a 1:1.2 molar ratio, with ADP•AlF4 to a final concentration of 1 mM. Crystallization trials of this ternary complex was performed at 20°C by the sitting-drop vapor diffusion method. Well-diffracted crystals were obtained under conditions of 15% (v/v) PEG 4k, 100 mM MES (pH 6.5), and 200 mM KNaTatrate.

Data collection and structural determination

X-ray diffraction data were collected on the beamline BL17U1 at SSRF synchrotron (Shanghai, China) and indexed and scaled with XDS [START_REF] Kabsch | Xds[END_REF]. The initial structure of the CaPif1-poly(T8)-ADP•AlF4 complex was solved by molecular replacement, performed in Phenix [START_REF] Adams | PHENIX: a comprehensive Python-based system for macromolecular structure solution[END_REF] with Phaser [START_REF] Mccoy | Phaser crystallographic software[END_REF] using the ScPif1 structure (PDB: 5O6D) as the template [START_REF] Lu | Insights into the structural and mechanistic basis of multifunctional S. cerevisiae Pif1p helicase[END_REF]. The final structure was manually rebuilt with Coot [START_REF] Emsley | Features and development of Coot[END_REF] and refined in Phenix. Data collection and refinement statistics are provided in Table 1. The atomic coordinates and structure factor amplitudes of CaPif1-poly(T8)-ADP•AlF4 have been deposited in the Protein Data Bank (PDB: 7OTJ).

DNA substrate preparations

All oligonucleotides (Sangon Biotech, Shanghai) were HPLC-purified (Supplementary Table 1). The partial duplex DNA S26D17 used in the stopped-flow assay was heated to 95°C in the annealing buffer [20 mM Tris-HCl (pH 8.0) and 100 mM KCl] and slowly cooled to room temperature.

Fluorescence polarization binding assay

The apparent dissociation constants of CaPif1 under equilibrium conditions were determined using a fluorescence anisotropy assay. The protein concentration-dependent changes in fluorescence anisotropy were measured with FAM-labeled probes using an Infinite F200 instrument (TECAN). Varying amounts of protein were added to 150 μL of binding buffer [50 mM KCl, 20 mM Tris-HCl (pH 7.5), 2 mM MgCl2 and 1 mM DTT] with 5 nM FAM-labeled probes. Each sample was allowed to equilibrate in solution at 24°C for 5 min. Then, steady-state fluorescence anisotropy was performed. A second reading was taken after 3 min to ensure that the mixture was well-equilibrated and stable. Each experiment was repeated at least 3 times. The equilibrium dissociation constant was determined by fitting the binding curves using the method described previously [START_REF] Liu | The Bacteroides sp. 3_1_23 Pif1 protein is a multifunctional helicase[END_REF].

Stopped-flow unwinding assay

A stopped-flow assay was used for measuring the helicase activity of CaPif1, according to Duan et al. [START_REF] Duan | G-quadruplexes significantly stimulate Pif1 helicase-catalyzed duplex DNA unwinding[END_REF]. In summary, unwinding kinetics were measured in a 2-syringe mode, where the helicase and fluorescently labeled DNA substrate were pre-incubated at 37°C in a syringe for 5 min. Then, the unwinding reaction was initiated by rapidly adding the ATP from the other syringe. The unwinding assays were performed in 25 mM Tris-HCl (pH 7.5) containing 25 mM NaCl, 2 mM MgCl2, and 1 mM DTT. The standard reaction was performed with 4 nM DNA, 1 mM ATP, and 100 nM CaPif1. All stopped-flow kinetic traces were averages of over 10 individual traces. The duplex unwinding kinetic parameters were estimated using the Bio-Logic SFM-400 mixer and the Bio-Logic MOS450/AF-CD optical system (FC-15, Bio-Logic, France) and analyzed as reported [START_REF] Zhang | Escherichia coli RecQ is a rapid, efficient, and monomeric helicase[END_REF].

Results and discussion

Crystal structure of CaPif1 with bound DNA and ADP•AlF4

The 5′-tail of a dsDNA is required for Pif1 helicase to unwind the duplex. The Pif1 helicase core, CaPif1 (CaPif1 368-883 ), displayed a high affinity to poly(T), poly(C), poly(A), and G-rich ssDNA in the presence of an ATP analog (Figure S1). Thus, CaPif1 was crystallized in complex with different ssDNA molecules in the presence of an ATP analog. Subsequently, the ternary complex containing CaPif1, Poly(T8) DNA, and nucleotide ADP•AlF4 was crystallized, and its structure was solved at a resolution of 2.57 Å. The asymmetric unit (a.u.) in the C121 space group contained 2 ternary complexes, and 2 CaPif1 molecules in both ternary complex exhibits similar organization that could be superimposed with an r.m.s.d. deviation of 0.258 Å for 282 equivalent α-carbon atoms.

CaPif1 helicase core was divided into 5 structural domains: 2 RecA-like domains 1A, at residues 367-437 and 457-555, respectively; 2A, at residues 556-618 and 812-867, respectively; 1B, at residues 438-456; 2B, at residues 619-682 and 769-811, respectively; and a yeast-specific extra structure domain 2C at residues 683-768 (Figure 1). However, residues 689-752 from domain 2C were not observed in the electron density map. Two RecA-like domains were separated by a cleft that bound and hydrolyzed ATP. Domain 1B formed an extended loop followed by a short helix, known as the "wedge region." Domain 2B adopted an SH3-like fold seen in the structure of RecD2, and the tip of its rail-like βhairpin (green in Figures 1b and1c) was close to domain 1B [START_REF] Saikrishnan | Mechanistic basis of 5'-3' translocation in SF1B helicases[END_REF]. The overall structure of the folded CaPif1 was similar to that of other Pif1 family helicases.

ATP binding and hydrolysis

NTP (dNTP)-binding and hydrolysis are necessary for a helicase to unwind a dsDNA. The ATP analog ADP•AlF4, bound in the cleft between domains 1A and 2A, was resolved in our structure (Figure 1b).

For ATP binding, such as ADP•AlF4 binding here, CaPif1 showed a similar binding site compared to that in ScPif1 (Figure 2a). The aromatic ring of adenine was found to be stacked by a highly conserved F555. The α-and β-phosphates were coordinated by interactions with 7 residues, G393-V398 and R556. AlF4 corresponding to the γ-phosphate of ATP was recognized by G393, K396, Q512, R556, and R847.

The highly conserved Q-motif in helicase involved in the special recognition of adenine bases has already been structurally and functionally described [START_REF] Tanner | The Q motif: a newly identified motif in DEAD box helicases may regulate ATP binding and hydrolysis[END_REF]. In CaPif1, the adenine base was found to be specifically recognized by Q373. We verified whether ATP/dATP could be used preferentially in the duplex unwinding process of CaPif1 by conducting a fluorescent stopped-flow helicase activity assay.

A partial duplex DNA was used as a substrate. All the measured kinetic curves (Figures 2b andS2) were fitted according to Zhang et al. [START_REF] Zhang | Escherichia coli RecQ is a rapid, efficient, and monomeric helicase[END_REF]. The results showed that the unwinding rate of the fast phase with ATP (kfast = 11 s -1 ) and dATP (kfast = 10 s -1 ) was significantly higher than that with other deoxyand ribonucleotide triphosphates (Figure 2c). All these structural and biochemical results show that Capifl1 uses the Q-motif to recognize adenine specifically, and it utilizes ATP and dATP more efficiently.

Interaction of ssDNA with CaPif1

S. cerevisiae Pif1was reported to prefer G-rich DNA to non-G-rich DNA, and no hydrogen bonds could be found between the helicase and poly(T) DNA in ScPif1 in complex with poly(T8) and ATPγS (PDB: 5O6D) [START_REF] Lu | Insights into the structural and mechanistic basis of multifunctional S. cerevisiae Pif1p helicase[END_REF][START_REF] Paeschke | Pif1 family helicases suppress genome instability at G-quadruplex motifs[END_REF]. However, our results showed that C. albicans Pif1 exhibited a comparable affinity for DNA with poly(T), poly(C) sequences, and G-rich sequences in the absence and presence of ADP•AlF4 (Figure S1). Thus, we analyzed the interactions between CaPif1 and poly(T) DNA using PDBsum (http://www.ebi.ac.uk/thornton-srv/databases/pdbsum/Generate.html) to delineate the mechanism of CaPif1's binding to ssDNA. The incomplete 6-nt oligo-dT (thymidine base and deoxyribose group of dT6 are missing) binding site was found to traverse along a channel that run across the top of domains 2A and 1A of CaPif1 in a 5′-to-3′ direction (Figure 3a), similar to that observed in other Pif1 helicases [START_REF] Singleton | Structure and mechanism of helicases and nucleic acid translocases[END_REF].

The binding of CaPif1 to poly(T) DNA was found to be mediated mainly by the contacts between the DNA backbone and the protein (Figure 3b), similar to that observed in ScPif1. Specifically, G442 formed a hydrogen bond with the phosphate group of dT4, T432 with dT5, S435 with dT6, R605 with both dT2 and dT3, and S816 with dT3. The imidazole ring of H434 and H818 was found to stack against the deoxyribose group of dT4 and dT2, respectively. All these residues are conserved between CaPif1 and ScPif1.

CaPif1 also demonstrated extensive interactions with the thymidine bases. The 5′-end dT1 base was stacked by CaPif1's F836. K518 stabilized the dT2 base through hydrophobic interaction. V516 interrupted the base stacking between dT2 and dT3, and L441 disrupted the base stacking between dT4 and dT5 by inserting between the thymidine bases. Notably, 2 amino acids, V517 from domain 1A and N645 from domain 2B, were involved in the interaction with the base of dT2 and dT5, respectively, via hydrogen bonds.

Sequentially, V517 and N645 of CaPif1 correspond to S386 and Q505 of ScPif1. However, S386 and Q505 of ScPif1 are not involved in oligo-dT binding, and no other residues interact with the thymidine bases via hydrogen bonds in the ternary complex structure of ScPif1-poly(T)-ATPγS. Thus, our observation of CaPif1's high affinity for poly(T) ssDNA in the presence of an ATP analog may help explain the difference between CaPif1 and ScPif1 (Figure 3c) [START_REF] Lu | Insights into the structural and mechanistic basis of multifunctional S. cerevisiae Pif1p helicase[END_REF].

Domain 2B movement is necessary for duplex unwinding

We and others have reported the domains 2B of BsPif1 and ToPif1 undergo a significant rotation upon binding to ssDNA and ATP [START_REF] Dai | Structural and functional studies of SF1B Pif1 from Thermus oshimai reveal dimerization-induced helicase inhibition[END_REF][START_REF] Zhou | Structural and Functional Insights into the Unwinding Mechanism of Bacteroides sp Pif1[END_REF][START_REF] Chen | Crystal structures of the BsPif1 helicase reveal that a major movement of the 2B SH3 domain is required for DNA unwinding[END_REF]. Domain 2B is in a closed conformation and located near domains 1A in Pif1 apo; it is in an opened conformation and far away from domain 1A in Pif1 in complex with DNA and ATP. On the other hand, the rotation of domain 2B is an important regulatory mechanism in both BsPif1's and ToPif1's helicase activity [START_REF] Dai | Structural and functional studies of SF1B Pif1 from Thermus oshimai reveal dimerization-induced helicase inhibition[END_REF][START_REF] Chen | Crystal structures of the BsPif1 helicase reveal that a major movement of the 2B SH3 domain is required for DNA unwinding[END_REF].

We probed whether domain 2B of CaPif1 behaved in the same manner by fixing 2B on 1A by crosslinking its cysteines. Five cysteines can be found in the truncated Pif1, C426 and C507 from domain 1A, C584 and C592 from domain 2A, and C662 from domain 2B. C426 is closest to C662 when the domain 2B is in an open conformation in the ternary complex (9.0 Å, Figure 4a). Thus, domain 2B in CaPif1 apo was expected to be in the same closed conformation as in BsPif1 and ToPif1 apo, and the spatial distance between C426 and C662 were expected to be closer, thus helping the establishment of a disulfide bridge between the 2 residues and the blocking of the rotation of domain 2B.

The wild-type CaPif1 without oxygen treatment was found to unfold a partial duplex with normal amplitude and rate in the absence or presence of DTT while showing negligible unwinding activity after a 2-hour oxygen treatment in the absence of DTT (Figures 4b-4d). Moreover, the unwinding activity of the wild-type CaPif1 with oxygen treatment could be rejuvenated with 2-5 mM DTT to reach a level comparable to that of the untreated protein (Figures 4c and4d). We designed and purified CaPif1 C426A and CaPif1 C662A to further analyzed the unwinding activity of CaPif1. After oxygen treatment, the unwinding activities of the 2 mutants were partially rejuvenated compared with that of the wild-type in the absence as well as the presence of DTT (Figures 4c and4d). Therefore, the unwinding activity of wild-type CaPif1 after oxygen treatment is likely reduced by the formation of a disulfide bridge between C426 and C662 that blocks the rotation of domain 2B. These results together stress the importance of 2B rotation/movement in duplex unwinding by CaPif1.

In summary, we have solved the ternary complex structure of CaPif1-ssDNA-ADP•AlF4 at high resolution. We have described the binding mechanism of CaPif1 to ssDNA and an ATP analog. Moreover, we found that blocking the potential rotation of domain 2B suppressed the unwinding activity of CaPif1. Our structural and biochemical data provide a foundation for future investigation of the unwinding mechanism of Pif1.

Declaration of competing interest

No competing financial interests.

Figure captions Figure 1 .

 captions1 Figure captions Figure 1. Structure of the CaPif1-ssDNA-ADP•AlF4 ternary complex. (a) The domain structure of CaPif1. (b and c) The structure of the CaPif1-ssDNA-ADP•AlF4 complex shown in cartoon (b) and surface (c), with domain 1A (blue), 2A (red), 1B (magenta), 2B (orange), 2C (yellow), and C-terminal domain (CTD; gray).

Figure 2 .

 2 Figure 2. CaPif1 exhibits a preference for ATP and dATP. (a) Detailed view of the nucleotidebinding site of CaPif1 with ADP•AlF4. (b) Stopped-flow kinetic traces for the unwinding of partial duplex DNA (S26D17) with different dNTPs. The unwinding rate of the fast phase (c) was determinedfrom the fittings using a previously reported equation[START_REF] Saikrishnan | Mechanistic basis of 5'-3' translocation in SF1B helicases[END_REF].

Figure 3 . 1 (

 31 Figure 3. CaPif1 binds to ssDNA. (a) Detailed view of the interactions between ssDNA and CaPif1. The amino acids involved in DNA binding are colored according to domain colors defined in Figure 1 (domain 1A, blue; 2A, red; 1B, magenta; and 2B, orange) and presented in sticks. (b) The interaction between CaPif1 and Poly(T) DNA. (c) The ssDNA binding curves of CaPif1 determined with Poly(T12) and GR12 (12-nt G-rich ssDNA) in the absence (left panel) or presence (right panel) of 1 mM ADP•AlF4.

Figure 4 .

 4 Figure 4. CaPif1 unwinding activity is suppressed by crosslinking. (a) The distance between C426

Figure 1 Figure 2 Figure 3

 123 Figure 1

Figure 4

 4 Figure 4

Table 1

 1 Data collection and refinement statistics of CaPif1-poly(T8)-ADP•AlF4 complex.

	Data Set	CaPif1-poly(T8)-ADP•AlF4
	Data collection
	Wavelength	0.977
	Resolution range (Å)	82.51-2.57 (2.66-2.57)
	Space group	C121
	Cell dimension
	a, b, c (Å)	198.97 79.96 94.11
	α, β, γ (°)	90 117.28 90
	Multiplicity	3.4 (3.5)
	Completeness (%)	96.51 (99.37)
	Mean I/sigma (I)	9.24 (2.16)
	Rmerge	0.085 (0.403)
	Unique reflections	40378 (4106)
	Refinement
	Reflections used in refinement	40316 (4092)
	Reflections used for R-free	2072 (181)
	Rwork (%)	20.9 (27.9)
	Rfree (%)	23.6 (33.9)
	Protein residues	866
	Bond lengths (Å)	0.005
	Bond angles (°)	1.14
	Ramachandran favored (%)	99.17
	Ramachandran allowed (%)	0.83
	Ramachandran outliers (%)	0.00
	PDB ID	7OTJ
	Statistics for the highest-resolution shell are shown in parentheses.

Acknowledgments

We thank beamline scientists at BL17U1 of the Shanghai Synchrotron Radiation Facility for assistance with data collection. This work was supported by the National Natural Science Foundation of China (No. 31870788) and Northwest A&F University Startup Funding for Xu-Guang Xi (No. Z101021903).

Supplementary material

Supplementary Table 1 Oligonucleotides used in this study Names Oligo sequences (5′-3′)

GTGTGTGTGTGT-F S26D17 TTTTTTTTTTTTTTTTTTTTTTTTTTATGTATGTCAAGGAAGG-F HF-CCTTCCTTGACATACAT F represents Fam. HF represents hexachlorofluorescein.

Supplementary Figure captions

Conflict of Interest

No competing financial interests.

Conflict of Interest


Hamza Bourbouh
email: hamza.bourbouh@nasa.gov

C Garion

X Thirioux
email: xavier.thirioux@isae-supaero.fr.

From Lustre to Simulink: Reverse Compilation for Embedded Systems Applications

Keywords: Computer systems organization → Real-time system specification, Embedded software, • Software and its engineering → Model-driven software engineering, Data flow languages, Model-based design, formal verification, translation validation, equivalence checking, Simulink

Model-based design is now unavoidable when building embedded systems and, more specifically, controllers. Among the available model languages, the synchronous dataflow paradigm, as implemented in languages such as MATLAB Simulink or ANSYS SCADE, has become predominant in critical embedded system industries. Both of these frameworks are used to design the controller itself but also provide code generation means, enabling faster deployment to target and easier V&V activities performed earlier in the design process, at the model level. Synchronous models also ease the definition of formal specification through the use of synchronous observers, attaching requirements to the model in the very same language, mastered by engineers and tooled with simulation means or code generation.

However, few works address the automatic synthesis of MATLAB Simulink annotations from lower-level models or code. This article presents a compilation process from Lustre models to genuine MATLAB Simulink, without the need to rely on external C functions or MATLAB functions. This translation is based on the modular compilation of Lustre to imperative code and preserves the hierarchy of the input Lustre model within the generated Simulink one. We implemented the approach and used it to validate a compilation toolchain, mapping Simulink to Lustre and then C, thanks to equivalence testing and checking. This backward compilation from Lustre to Simulink also provides the ability to produce automatically Simulink components modeling specification, proof arguments, or test cases coverage criteria.

CCS Concepts: •

INTRODUCTION

When developing safety-critical software and systems like aircraft controllers, system designers and engineers are now using Model-Based System Engineering (MBSE). MBSE provides early stage prototyping and often tools enabling simulation or even code generation. Among the standard modeling languages used, we shall mention MATLAB Simulink and ANSYS SCADE as industry-grade model languages used in multiple contexts from aerospace systems to healthcare devices or nuclear plants.

Let us focus on safety-critical controller software and systems. In most cases, such systems are designed and implemented as the composition of several reactive components, each performing a specific and relatively simple function. In the aerospace domain, the certification regulation DO178C [START_REF]C. Software Considerations in Airborne Systems and Equipment Certification[END_REF] specifies the different steps of software development and emphasizes the need to specify requirements and to verify the validity of intermediate models or code with respect to their requirements. A first question that naturally arises is the following: in a MBSE context, how can system designers specify these requirements and verify the validity of their models?

In addition to models, a leading methodology to develop component-based software is contractbased design. In this paradigm, each component is associated with a contract specifying its inputoutput behavior in terms of guarantees provided by the component when its environment satisfies certain given assumptions. These assume/guarantee pairs can thus be used to specify requirements at the component level. This approach was first proposed by Hoare [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] to specify axiomatic semantics of imperative programs; however, it was later lifted to reactive systems through the notion of synchronous observers [START_REF] Champion | CoCoSpec: A mode-aware contract language for reactive systems[END_REF][START_REF] Dieumegard | Compilation of synchronous observers as code contracts[END_REF][START_REF] Halbwachs | Synchronous observers and the verification of reactive systems[END_REF][START_REF] Halbwachs | Validation of synchronous reactive systems: From formal verification to automatic testing[END_REF][START_REF] Rushby | The versatile synchronous observer[END_REF]. When contracts are specified formally for individual components, they can facilitate several development activities, such as compositional reasoning during static analysis, step-wise refinement, systematic component reuse, and component-level and integration-level test case generation.

At the model level, writing requirements with synchronous observers can usually be performed in the same language as the model, easing its deployment and the adoption of the approach by engineers. These requirements may be verified on the model by simulation or other techniques, such as model checking. Notice that contracts or synchronous observers attached to model components can also be used to specify additional knowledge such as invariants computed by a first analysis.

At a research level, the topics of certified compilation, test-case generation, or formal analysis of dataflow languages are very active. Yet the integration of research ideas from academia into commercial frameworks such as Simulink is quite difficult. The main reason is the lack of formally publicly available semantics of the Simulink language. It is more common to develop methods and tools on well-defined and publicly available languages such as Lustre [START_REF] Bourbouh | Automated analysis of Stateflow models[END_REF][START_REF] Bourbouh | CoCoSim, a code generation framework for control/command applications: An overview of CoCoSim for multi-periodic discrete Simulink models[END_REF][START_REF] Scaife | Defining and translating a "safe" subset of Simulink/Stateflow into Lustre[END_REF]. For instance, approaches such as FRET [START_REF] Giannakopoulou | Generation of formal requirements from structured natural language[END_REF] or Dassault Systèmes STIMULUS 1 ease the formalization of requirements but can hardly be directly linked to Simulink models to provide genuine Simulink components representing the specification. However, the FRET tool can generate these requirements in the CoCoSpec specification language [START_REF] Champion | CoCoSpec: A mode-aware contract language for reactive systems[END_REF], an extension of the Lustre language to support assume-guarantees contracts. Formal analysis of Simulink models is also addressed by first providing a formal semantic of the model allowing either executable embedded code or a model for analysis by formal tools. CoCoSim [START_REF] Hamza Bourbouh | CoCoSim-Automated Analysis Framework for Simulink[END_REF] supports the analysis of a discrete subset of Simulink/Stateflow models by generating an equivalent Lustre model for which contracts are expressed using the CoCoSpec specification language and verified using model-checking techniques with tools such as Kind2 [START_REF] Champion | CoCoSpec: A mode-aware contract language for reactive systems[END_REF][START_REF] Kahsai | PKind: A parallel k-induction based model checker[END_REF].

Although translating Simulink models into formal languages such as Lustre allows to formally analyze such models, bringing back analysis artifacts generated from Lustre in the Simulink model is currently not done and needs a translation of Lustre code to Simulink. These artifacts can include invariants generated from SMT solvers that can be used to infer contracts for subcomponents, Lustre annotations such as test-case coverage conditions, and auto-generated CoCoSpec contracts from formalized requirements using FRET for instance. Connecting Lustre artifacts back to the Simulink model makes it simpler for engineers using Simulink to adopt the use of formal tools, and no knowledge of formal languages such as Lustre is required.

Contributions. The main contribution of this work is a compilation process from Lustre models to Simulink models allowing closer connection to formal analysis tools of Simulink models (e.g., CoCoSim). More specifically:

• We based this new compilation on the existing modular compilation of synchronous dataflow languages [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF][START_REF] Garoche | Testing-based compiler validation for synchronous languages[END_REF], providing a sound compilation scheme, preserving the semantics. • Connected to the FRET [START_REF] Giannakopoulou | Generation of formal requirements from structured natural language[END_REF] tool, we automatically produce Simulink contracts from English language specifications, generating an intermediate Lustre encoding. • The compilation proposed is also used to provide runnable evidence at the model level, soundly translating analysis results from a model checker. • The Simulink model can be annotated with test-case coverage conditions.

• The approach has been applied to large benchmarks, showing the applicability on a large set of components and requirements. • Last, all of the presented approaches are implemented and available in the open source Co-CoSim toolbox [START_REF] Hamza Bourbouh | CoCoSim-Automated Analysis Framework for Simulink[END_REF].

Related works. Programming languages could be fitted with specification languages, such as ACSL [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language, Version 1.16[END_REF] for C or SPARK [START_REF]SPARK 2014 Reference Manual[END_REF]. In the case of synchronous languages and models, multiple works [START_REF] Cimatti | A property-based proof system for contract-based design[END_REF][START_REF] Liu | From design contracts to component requirements verification[END_REF][START_REF] Whalen | Your what is my how: Iteration and hierarchy in system design[END_REF] advocate for the use of component-attached requirements. Notice that the actual definition of such contracts or reasoning on them is still a challenge. Formalized contracts can be used for a large set of applications: test oracles, test synthesis, reactive synthesis [START_REF] Katis | Synthesis from assume-guarantee contracts using skolemized proofs of realizability[END_REF][START_REF] Klein | Revisiting synthesis of GR(1) specifications[END_REF], compositional reasoning, or validation of individual contracts. CoCoSpec [START_REF] Champion | CoCoSpec: A mode-aware contract language for reactive systems[END_REF][START_REF] Champion | The Kind 2 model checker[END_REF] is a specification language for Lustre [START_REF] Halbwachs | The synchronous dataflow programming language LUSTRE[END_REF] and has been extended to Simulink models.

Regarding the compilation of Lustre models as Simulink components, an interesting approach is the Assume Guarantee Reasoning Environment (AGREE) framework [START_REF] Liu | From design contracts to component requirements verification[END_REF]. In AGREE, AADL components are associated to Lustre contracts. Validation of the composition of components is performed thanks to the combination of these contracts by Lustre-based tools such as JKind [START_REF] Gacek | The JKind model checker[END_REF]. In the case of AADL components defined by Simulink models, the Lustre contract is also checked against the Simulink model using Simulink Design Verifier. The method proposed by Liu et al. [START_REF] Liu | From design contracts to component requirements verification[END_REF] provides an encoding of the Lustre contract as a piece of MATLAB code-that is, an imperative program embedded within a MATLAB S-function Simulink component. This approach enables the analysis of the model with the Simulink Design Verifier but is restricted to MATLAB-based tools since few external approaches are capable of analyzing or compiling MATLAB code.

Outline. The article is structured as follows. Section 2 presents the CoCoSim framework, as well as the Lustre language and the associated CocoSpec contracts used within the framework as intermediate models. Section 3 develops the compilation process from Lustre nodes to Simulink subsystems. Section 4 presents experimental results, and Section 5 presents various uses such as synthesis of contracts as runnable evidence or test oracles.

BACKGROUND

In this section, we present CoCoSim, a Simulink analysis framework, as well as the syntax and semantics of Lustre [START_REF] Halbwachs | The synchronous dataflow programming language LUSTRE[END_REF] and associated contracts.

Simulink

Simulink [START_REF]MATLAB Simulink (R2018b)[END_REF], developed by MathWorks, is a graphical programming language for modeling dynamical systems, including discrete time ones (i.e., synchronous dataflow systems). Simulink has gained popularity in critical embedded systems development. It supports the design and simulation of complex systems before automatically generating embedded C code. A Simulink model consists of a set of blocks connected by signals that can be organized as hierarchical models. Figure 1 illustrates a stopwatch example that measures the amount of time elapsed between its activation and deactivation. The stopwatch is controlled by two external signals: a toggle signal to toggle the activation of the stopwatch and a reset signal to reset the counter.

Simulink has a rich library of blocks and also supports both continuous and discrete solvers in its simulation engine. Blocks can run on different sample times (multi-periodic) or on one global sample time (mono-periodic). However, Simulink is lacking a formally published reference semantics for its library of blocks, which makes formal analysis of such models difficult.

CoCoSim

CoCoSim [START_REF] Hamza Bourbouh | CoCoSim-Automated Analysis Framework for Simulink[END_REF] is an open source toolbox for verifying Simulink/Stateflow models. It is integrated within MATLAB as a toolbox and provides easy access to a set of tools. Specification-wise, Co-CoSim allows attaching contracts, such as synchronous observers, to Simulink subsystems. Contracts are dedicated subsystems relying on Boolean dataflows to denote elements of the contract (e.g., assumptions and guarantees). CoCoSim is structured as a compiler and follows a simple schema initially developed for the discrete subset of Simulink [START_REF] Tripakis | Translating discrete-time Simulink to Lustre[END_REF]. Using the MATLAB API, it iterates over blocks and produces their equivalent version as Lustre nodes.

Figure 2 presents the CoCoSim architecture. In practice, a first preprocessing phase performs model-to-model transformation and replaces some blocks by equivalent but simpler versions. The second phase consists of compiling this simpler version of the Simulink model to Lustre (cf. Section 2.3). This compilation is modular and produces a Lustre node for each Simulink subsystem. Once the Lustre model is obtained, it can be either compiled to C code with the LustreC compiler [START_REF] Dieumegard | Compilation of synchronous observers as code contracts[END_REF] or submitted to Lustre model checkers such as Kind2 [START_REF] Champion | CoCoSpec: A mode-aware contract language for reactive systems[END_REF][START_REF] Kahsai | PKind: A parallel k-induction based model checker[END_REF] or Zustre [START_REF] Garoche | Hierarchical state machines as modular horn clauses[END_REF].

CoCoSim carefully addresses traceability issues by manipulating a model along its processing chain. This enables the expression of feedback from model checkers to Simulink models. For example, a counterexample can be replayed at the Simulink level using its simulation engine.

Lustre

Lustre [START_REF] Caspi | Lustre: A declarative language for programming synchronous systems[END_REF] is a synchronous language for modeling systems of synchronous reactive components.

A Lustre program L is a collection of nodes N 0 , N 1 , . . . , N m . The nodes satisfy the grammar described in Figure 3 in which td denotes type constructors, including enumerated types, and value v denotes either constants of enumerated types C or primitive constants such as integers i or reals r . Each node is declared by the grammar construct d of Figure 3 and is represented by the following tuple:

N i = (I N i , O N i , L i , Eqs i ),
where I N i , O N i , and L i are sets of typed input, output, and local variables. Eqs i represents the set of stream definitions defined as

Eqs i = (v j i ) 1≤j ≤nb i = expr i i ∈{0, ..., |Eqs i |-1}
, where nb i ∈ N * denotes the number of output variables defined by the expression expr i , v j i ∈ O N i ∪ L i and expr i is an expression where Vars(expr i ) ⊆ O N i ∪ I N i ∪ L i . Vars(expr i ) is the set of variables in expr i , and expressions expr i are arbitrary Lustre expression, as presented in Figure 3 by constructor e, including node calls N j (u 1 , . . . ,u n ).

Lustre code consists of a set of nodes transforming streams of input values into streams of output values. Lustre models are synchronous in the sense that the processing time of each component is neglected and communication is assumed to be instantaneous [START_REF] Benveniste | The Synchronous Approach to Reactive and Real-Time Systems[END_REF]. A notion of symbolic "abstract" universal clock is used to model system progress.

Let us illustrate Lustre syntax on a possible model for the stopwatch example. The code is presented in Listing 1. Lines 1 through 4 of Listing 1 define a count node returning an integer stream representing the sequence of natural numbers. Primitive types like bool, int, or real are available. Note that, in general, a node may declare several output streams.

Line 6 declares a node named stopwatch that takes three Boolean streams as parameters, namely tick, toggle, and reset, and declares a single integer stream as output, namely time.

In Lustre, a node is defined by a set of stream equations with possible local variables denoting internal flows. Stream equations are defined between the let and tel keywords. For instance, line 7 declares running as a local Boolean flow.

When defining equations, regular arithmetic and comparison operators are lifted to streams and are evaluated at each timestep. For instance, line 9 of Listing 1 defines stream running as a disjunction of the reset input stream and the result of comparing two Boolean streams: false -> pre running, a Lustre expression, and toggle, one of the input streams of the node. The temporal operator pre, for previous, enables a limited form of memory, allowing to read the value of a stream at the previous instant. The arrow operator allows to build a stream c -> e as the expression e while specifying the first value c. Therefore, the expression false -> pre running denotes a Boolean stream whose first value is false and whose next values are the previous values of the running stream.

A node that relies on these constructs is considered as stateful; its internal state is defined by the values of the memories. Without these temporal operators, nodes act as mathematical functions.

Another specific construct of Lustre is the definition of clocks and clocked expressions. Clocks are defined as enumerated types, the simplest ones being Boolean clocks. Expressions can then be clocked for such clock values. For instance, let us consider the expression e when c where c is a Boolean clock, then the expression e when c is not defined when variable c is false.

Let us now explain the expressions in lines 10 and 11:

• count(tick when running) is a call to node count with argument tick clocked on the clock running. Therefore, there is no value for this expression when running is false. Notice that the tick parameter of the node count is unused in the definition: it is only used for clocking. • count(tick when running) every reset is the previous call to node count completed with a reset expression every reset. This specifies that if Boolean reset is true, then the call to count reinitializes the node to its initial state and therefore the time stream to 0. The local stream running is true whenever reset is true, and therefore the node count is always executed when reset is true and the arrow operator will reset to its initial value 0. time will be clocked on the base clock.

-When running is true, the expression count(tick when running) every reset is used to define time. This expression must be clocked on running, which is trivially the case here, but we may have used an external expression clocked on running for instance. -When running is false, the expression (0 -> pre time) when not running is used to define time and is also trivially clocked on the negation of running. Table 1 presents an example of an evaluation of several streams from the stopwatch node: first running is false, then becomes true when the toggle is true and becomes false when the toggle is true again (simulating the operator pressing the toggle button of the stopwatch). The reset parameter is considered always false in this example.

Finally, expressions associated with each clock case have to be clocked appropriately, and the clocking phase of the compiler allows checking the consistency of clock definitions and uses, as would do a typing compilation phase.

Nodes and calls form a hierarchy of nodes comparable to the notion of subsystems in Simulink. Type and clock inferences guarantee at compile time that expressions and function calls respect their type constraints and properly rely on previous values to build current ones. For example, consider the following equations x = f(y); y = g(x);. These two equations create a causality problem and produce an algebraic loop error. However, notice that the same definitions with either f(pre y) or g(pre x) would be typable and accepted by the compiler. A more complete definition including additional constructs such as automata or clocks based on enumerated types [START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF], as used in our framework, can be found in the work of Garoche et al. [START_REF] Garoche | Hierarchical state machines as modular horn clauses[END_REF]. Our approach handles those constructs, but their definition is not required to present the contribution.

Synchronous Observers

The synchronous observer acts as a description of an axiomatic semantics for a synchronous model. The observer is defined in the same language as the model itself and corresponds to a set of Boolean streams. If the property is valid, the output flow encoding the property should remain true during the execution of the program.

In CoCoSim, this is performed with a specific specification subsystem and implemented at Lustre level by expressing these Boolean flows as comments in the code. Different syntaxes enable such annotations, and CoCoSpec contracts [START_REF] Champion | CoCoSpec: A mode-aware contract language for reactive systems[END_REF] are one of them in which annotations specify assumeguarantee contracts, a kind of Hoare triples extended to the synchronous setting [START_REF] Dieumegard | Compilation of synchronous observers as code contracts[END_REF].

For instance, a synchronous observer on the previous stopwatch example would be the assertion that the stream time always has a non-negative value. Listing 2 illustrates a simple CoCoSpec contract using the stopwatch node introduced earlier and specifying that the stream time always has a non-negative value given the assumption that toggle and reset cannot be pressed at the same time.

Our objective is then to be able, starting from a Lustre implementation and specification of a system, to generate a Simulink design with the same behavior as the Lustre one with the Simulink synchronous observers corresponding to the specification of the Lustre nodes.

COMPILING LUSTRE NODES AS SIMULINK BLOCKS

The compilation of Lustre nodes into Simulink subsystems is performed in two steps:

• The first step is to produce a simplified version of the input Lustre model, preserving the hierarchical structure of nodes. This is done using a dedicated backend we implemented in LustreC [START_REF] Dieumegard | Compilation of synchronous observers as code contracts[END_REF], an open source Lustre compiler. • The second step is to submit the previously produced description to a dedicated backend of CoCoSim that creates Simulink objects of the associated hierarchy of components and connects the corresponding ports in the Simulink model.

Translating discrete Simulink to Lustre is algorithmically simple. Each connection between blocks is associated with a fresh variable, and each block is mapped to a function call, a basic operator, or another node in the case of Simulink subsystems. The challenge is more on defining the semantic of each Simulink block. For instance, Simulink unit delays modeling memories are mapped to expressions i -> pre e where i is the initial value specified in the unit delay block and e is the input signal of the unit delay.

Going backward (i.e., translating Lustre to Simulink) is more challenging when dealing with a complex Lustre AST and requires a simplified version of Lustre equations. For instance, although a basic expression pre e could be associated with unit delay, its presence as an argument in a complex expression or a node call is more difficult to tackle. Our idea is to use a Lustre compiler to simplify expressions and produce appropriate constructs. We use LustreC, a Lustre compiler implementing the synchronous dataflow languages hierarchical compilation scheme [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF][START_REF] Bourke | A formally verified compiler for Lustre[END_REF]. The LustreC compiler is implemented as a sequence of transformations and could eventually produce an imperative version of the Lustre input model.

From Lustre to Normalized Lustre

LustreC compilation is essentially structured in three main phases. LustreC takes as input Lustre models composed of "classic" dataflow nodes, mixed with hierarchical state machines [START_REF] Bourbouh | Automated analysis of Stateflow models[END_REF][START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF][START_REF] Garoche | Hierarchical state machines as modular horn clauses[END_REF]. The first phase of the compiler, therefore, amounts to producing pure dataflow Lustre by introducing fresh variables for each automaton to represent its states and encoding transitions in automata as clocked expressions and merges of them. The second phase performs normalization, of which the updated version will be detailed in the following. The main idea of this normalization phase in LustreC is to introduce fresh Lustre variables to encode intermediate values as in classic three-address code. Finally, the last phase translates each normalized node into imperative machine code.

Since the previously presented compilation scheme used by the compiler LustreC is reliable and used to produce trustable C code [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF][START_REF] Garoche | Testing-based compiler validation for synchronous languages[END_REF], we adapted it to perform our required simplifications on the Lustre code by modifying the existing normalization stage to produce for each Lustre node a normalized node that can be easily compiled into a Simulink construct, preserving the hierarchy of the initial Lustre nodes. Whereas the original normalization of the LustreC tool was the direct implementation of Biernacki et al. [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF], the updated normalization introduces extra variables and associated definition for all operators or function calls, including primitive operators such as arithmetic or logical operators.

The normalization process transforms a Lustre model defined into the grammar of Figure 3 into one of Figure 4. It introduces an additional grammar element l denoting a leaf value (i.e., a variable or a constant). Normalization of an expression returns a fresh typed and clocked variable along with a set of newly bound stateful normalized equations and associated fresh variables. These normalized equations, except for node calls, do not involve nested constructs and correspond to three-address code for binary operators. The arguments of node calls are constants or variables, except for a special case where they are all sampled on the same clock that optimized in Simulink block generation as explained in the following section.

Let us illustrate the normalization of the stopwatch example presented in Listing 1. After normalization, the Lustre code presented in Listing 3 is generated. The original Lustre expressions are given in the comments.

Listing 3 follows the grammar described in Figure 4. The nodes count and stopwatch are normalized in a classic three-address code so each complex expression is decomposed into simple expressions involving new fresh variables or constants. Each stateful node has a Boolean variable is_init denoting its first timestep defined by true -> false. The arrow expression l1→l2 is replaced by a conditional statement if is_init then l1 else l2; see variable time in node count and streams __stopwatch_7 and __stopwatch_2 in node stopwatch. Node stopwatch contains clocked expressions using when and merge operators, and their semantics is explained in Section 2.3. Stream __stopwatch_4 (respectively, __stopwatch_3) is clocked on running (respectively, not running). The expression (count(tick when running)every reset) is not further normalized since it respects the grammar rule f (l when C(x), . . . , l when C(x)) every l described in Figure 4. The advantage of keeping it unnormalized is explained in the next section.

From Normalized to Simulink

A normalized node is translated to a Simulink subsystem. We first start translating leaf nodes and then finish with the top nodes. All nodes are translated as subsystems and used as a library of nodes; if a node g calls a node f, then the subsystem that corresponds to node f is instantiated and used inside the subsystem that corresponds to node g.

Each equation definition is mapped to Simulink components. Since both Simulink and Lustre are synchronous dataflow languages, the order of equations is not important. When a Lustre variable is defined, a Goto Simulink block is used with the same name as the variable. When the Lustre variable is used in an equation, a From Simulink block is used to read from the signal associated with the same variable. For each Lustre variable, there is one Goto Simulink block that stores the value of the variable and many From Simulink blocks that read from the Goto Simulink block.

The generated Simulink model of the Lustre example of Listing 3 is illustrated in Figure 5. The user has the choice to keep the Goto and From blocks or remove them and link signals with the same tag to each other. For readability, we kept only the is_init and running Gotos. We note that the generated Simulink models are sometimes difficult to read when the Lustre source is large. We recommend that engineers always update the Lustre files and regenerate the Simulink blocks rather than try to edit the generated model directly.

To explain the generated Simulink model of Figure 5, we will go over the grammar in Figure 4 of the normalized Lustre code and define the equivalent Simulink components. Each case is illustrated in Figures 6 through 8. We present the following: (a) Rule x = l, local assignment of a variable or constant to another variable (e.g., out1 = x). The equation is a simple alias between variables and is modeled in Figure 6(a). A From Simulink block is used to read from the signal associated with the variable x specified in the tag. A Goto Simulink block is used to write on the signal associated with the variable out1 specified in the tag. In the case of an assignment of a constant x = C, a Constant Simulink block is used in place of the From Simulink block. (b) Rule x = pre l, state assignment-that is, a pre construct over a variable (e.g., pre_x = pre x).

Thanks to our modified normalization phase, each pre operator argument is aliased to a fresh variable, here pre_x. In Figure 6(b), Unit Delay acts as a memory, but its initial value, usually specified in Simulink, is left unused since, in a valid Lustre model, any pre is guarded by an arrow construct, preventing its use at the first timestep or after a reset. (c) Rule x = true → f alse, this is the only arrow construct in our normalized Lustre (e.g., is_init = true→false) and is modeled in Figure 6(c). The Unit Delay block uses its initial condition true at the first step and then the previous value of its input for the following steps. Since the input of the Unit Delay in Figure 6(c) is the constant false, the Unit Delay will produce false at all times except the initial step defined by true. The Unit Delay block could be reset to its initial value by an external signal (see Reset block in Figure 9). is a Lustre node running on the same base clock as its parent node (e.g., x = bar(in1, in2)). This is modeled in Figure 7(a) where bar_call is an instantiation of subsystem bar associated to some Lustre node called bar. In the case of an operator of the standard library, such as x = in1 + in2, the subsystem bar_call would be a basic Simulink block, such as Add block, or Gain with scalar -1 for unary minus.

Let us finish with two complex constructs: clocked expressions and resetting nodes. Clocked expressions. Following Biernacki et al. [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF], Lustre nodes are considered to be homogeneous in terms of clocks-that is, all input and output flows have to be clocked with the same base clock. However, within the node content, internal flows may be clocked on other signal values, either local signals or inputs. Let ck be the base clock of the node. Then, any local clock is defined as a subclock of this base clock ck. Thus, any expression and equation, including those listed previously, are clocked, perhaps implicitly through the application of the clock calculus phase, and subject to the transformations presented here. Clocked expressions are any right-hand side of an equation where the defined variable is assigned a specific clock different from the base clock ck. In the grammar of the normalized Lustre defined in Figure 4, the right-hand side expressions that can be clocked are f (l, . . . , l) and f (l, . . . , l) every l if the arguments of node f are clocked on a different clock than the base clock ck, expressions f (l when C(x), . . . , l when C(x)) and f (l when C(x), . . . , l when C(x)) every l, and the expression l when C(x). Clocked expressions can be modeled in Simulink with an If Action subsystem; it is a subsystem whose execution is enabled by an If block. The If block evaluates a logical expression and then, depending on the result of the evaluation, outputs an action signal that enables the execution of the If Action subsystem linked to it. When the latter is not activated, it is configured to either reset its memories (e.g., Unit Delays use the initial condition) or hold the previous value. We choose the Held feature to ensure that the If Action subsystem maintains its state when not active. For instance, in the expression count(tick when running), the node count holds the value of the counter when it is not running.

The advantage of not further normalizing the equation y = f(x when true(c)) is illustrated in Figure 8(c); the argument x does not need to be clocked twice, since node f is only executed when condition c is positive. The equivalent normalized Lustre code is x2 = x when true(c); y = f(x2);, where both expressions x when true(c) and f(x2) will be embedded inside two different If Action Subsystems with the same condition. The first If Action Subsystem is shown in Figure 8(a), and the second is shown in Figure 8(c). This special construction is also handled since first it occurs frequently in our LustreC compilation chain and second it exempts us from implementing a If Action subsystem factorization algorithm. Stateful nodes and reset. In Figure 9, the called node bar is stateful: either it contains an arrow function, and typically pre expressions, or it calls other stateful nodes.

Since foo contains a stateful node, it is itself stateful. The definition of the node as a resettable subsystem as suggested in Figure 7(b) will recursively reset each memory in the node and its children, performing the expected behavior. This produces the Simulink diagram presented in Figure 9.

There is, however, a case where this encoding is erroneous. Indeed, in Simulink, if a resettable subsystem contains Action Subsystems with the Held feature, then the reset action is not propagated within these Action Subsystems. The only place where we use these Action Subsystems in our translation is in the treatment of clocked expressions explained earlier. Therefore, in the case of a node conditionally reset with an every cond and containing subexpressions defined over subclocks, then one needs to explicitly propagate the reset signal to these Action Subsystems.

The generation of subsystems associated with clocked node calls should then be explicitly extended with reset inputs, adding memory to record the reset status of the node for clocked substreams. The subsystem (that keeps track of the reset status is presented in Figure 10. Its output is added as an input of the Action Subsystem and the isActive input is the condition associated with the If Action Subsystem, whereas the reset input is the reset condition of the parent subsystem. The output "to be reset" is positive when the reset input is positive or the Action Subsystem is re-activated and "to be reset" was previously active. If the Action Subsystem is not active, the previously "to be reset" value is kept. For instance, in Table 2, Table 2. A Simulation of the "Should Be Reset" Subsystem of Figure 10 isActive

False False False True True reset

False True False False False to be reset False True True True False we give an example of an execution of the subsystem presented in Figure 10. The If Action Subsystem was inactive for the first three steps, and the reset signal was active for the second timestep. The If Action Subsystem should be reset when it was re-activated at the fourth step, and the "to be reset" signal is going to negative at the fifth step since the reset input was not triggered. Thanks to the extensive validation we performed, we are confident that this encoding faithfully addresses this specific case. The validation process is detailed in the following section.

EVALUATION

Our approach was evaluated on a set of case studies, from small benchmarks taken from our regression test suite to industrial ones, using equivalence checking, which will be defined in the following.

Let us denote by L and S the sets of Lustre and Simulink models. Model semantics is denoted by • L for L ∈ L and • S for S ∈ S. Each function is a (possibly stateful) map from a set of n typed input flows to m typed output flows (e.g., L L : T n → T m ).

The objective of equivalence checking is to verify that two models, in the same language, are equivalent. For Lustre models L 1 , L 2 ∈ L, we say that L 1 is equivalent to L 2 , denoted by L 1 ≡ L L 2 if and only if for any input flow i ∈ T n , L 1 L (i) = L 2 L (i). The property ≡ S is defined similarly on Simulink models. Behavioral equivalence can be evaluated either at the Simulink level with Simulink Design Verifier or at the Lustre level with the Kind2 model checker [START_REF] Champion | CoCoSpec: A mode-aware contract language for reactive systems[END_REF][START_REF] Kahsai | PKind: A parallel k-induction based model checker[END_REF]. It can also be evaluated through tests when formal tools cannot conclude.

One can consider the compilation process of the CoCoSim toolbox from Simulink to Lustre as a map S2L : S → L. Similarly, the algorithm proposed in Section 3 characterizes a map L2S : L → S. We assume that S2L is sound, and we target specifically the validation of L2S. Therefore, we consider the following verification challenges: For all model S ∈ S, S ≡ S L2S • S2L(S),

(1) For all model L ∈ L, L ≡ L S2L • L2S(L).

(

) 2
Let us add that in both cases, there is a single call to L2S and that the function S2L, implemented in the CoCoSim toolbox, shares no code or algorithm with the LustreC tool used to implement the function L2S.

The results are presented in Table 3. The first three columns give metrics about the size of the models. Simulink Design Verifier was applied to the top level of the system. Lustre equivalence checking (cf. Equation (2)) using Kind2 has been used both on the main node and modularly, considering each subnode as a verification target.

Concerning the 89 Lustre benchmarks from our regression suite (see the first line of Table 3), 85 benchmarks contain only one large top node with 1,600 code lines and 465 variables on average. Since there is a single top node in these benchmarks, applying compositional verification does not improve the results. Table 3 shows that model checking using a global (top-level) encoding both in Simulink Design Verifier and Lustre was able to prove 87 benchmarks but unable to prove the validity of two remaining benchmarks. We applied compositional verification on the two remaining benchmarks that were hard to prove due to their complexity. For the first benchmark, 9 out of 16 nodes were proved safe, and one node was proved safe by k-induction [START_REF] Kahsai | PKind: A parallel k-induction based model checker[END_REF][START_REF] Sheeran | Checking safety properties using induction and a SATsolver[END_REF]. Similar results were obtained on the second benchmark. Nodes that were hard to validate were hierarchical state machines expressed in Lustre. Lustre automata are compiled into pure dataflow equations, encoding transitions as clocked expressions, which explains that the final Lustre code is more complicated than the original model. All unproved nodes were validated by equivalence testing.

The approach was also applied to four industrial Simulink benchmarks: the NASA Transport Class Model (TCM) [START_REF] Brat | Verifying the safety of a flight-critical system[END_REF], the ROSACE use case [START_REF] Pagetti | The ROSACE case study: From Simulink specification to multi/many-core execution[END_REF], a Full Authority Digital Engine Control (FADEC), and a CNES Attitude and Orbital Control System (AOCS). All of these benchmarks were analyzed using Equation [START_REF]C. Software Considerations in Airborne Systems and Equipment Certification[END_REF].

Table 3 shows the effectiveness of compositional verification compared to monolithic verification. Simulink Design Verifier was unable to globally prove any model. This can be explained by both the use of nonlinear arithmetic operators, which are hardly analyzed by solvers, and the size of the model. Using model checking on the Lustre global encoding, we were able to prove two of the four models. Compositional verification in Lustre shows better performance: more than 85% of nodes are proved safe. Equivalence testing was applied to the unproved nodes. For the AOCS case study, the fact that we were able to globally prove the system with Lustre but unable to prove all of the corresponding nodes can be explained by the elimination of some behaviors difficult to prove for particular nodes when considering the global system.

APPLICATIONS

Producing Simulink subsystems from Lustre models has several advantages. We mention a few of them next.

Easing the Formalization of Requirements at the Model Level

An essential step when it comes to supporting the formalization of requirements is the capability to add the specification to a model. Most of the tools handling formalized requirements use some formal annotation and formal languages to express these requirements. For instance, the AGREE framework [START_REF] Liu | From design contracts to component requirements verification[END_REF] and FRET [START_REF] Giannakopoulou | Generation of formal requirements from structured natural language[END_REF] formalization tool use Lustre and CoCoSpec, respectively, to express requirements. We integrated our work in CoCoSim and connected it with FRET output, automatically translating CoCoSpec contracts generated by FRET to contracts expressed in Simulink and supported by CoCoSim. This work was applied to publicly available industry-provided examples2 from Lockheed Martin Cyber-Physical Systems challenges [START_REF] Elliott | An example set of cyber-physical V&V challenges for S5, Lockheed Martin Skunk works[END_REF][START_REF] Elliott | On example models and challenges ahead for the evaluation of complex cyber-physical systems with state of the art formal methods V&V, Lockheed Martin Skunk works[END_REF], which is a set of aerospace-inspired examples provided as text documents specifying the requirements along with associated Simulink models. Examples range from a basic integrator to complex autopilots. The complete case study and formalized requirements are presented in a detailed technical report [START_REF] Mavridou | Evaluation of the FRET and CoCoSim Tools on the Ten Lockheed Martin Cyber-Physical Challenge Problems[END_REF].

Generation of Runnable Evidence at the Simulink Level

The initial motivation for this work came from the use of the property-directed reachability-based tool Zustre [START_REF] Garoche | Synthesizing modular invariants for synchronous code[END_REF] to analyze synchronous observers associated with Simulink models by translating them to Lustre before analyzing them. The Zustre model checker can provide a counterexample in case of failure and also returns a set of invariants in case of success. However, although traceability information was sufficient to execute the counterexample on the initial Simulink model, the expression of the produced invariant as runnable evidence was not possible. More specifically, the hierarchy-preserving encoding of the Lustre model into the model checker provides, in case of success, a set of local invariants that could be attached to Simulink subsystems. As an example, Listing 4 presents such a generated local invariant (can be read as (pre(time)>= 0 => time >= 0)). The Lustre to Simulink translation allows attaching this property to a subsystem as a synchronous observer.

Generation of Lustre Annotations at the Simulink Level

The LustreC compiler can generate the MC-DC coverage criterion as Lustre annotations in Lustre code. In addition, these annotations are included in the compilation process described in Section 3. These annotations could be attached to Simulink subsystems. Listing 5 provides an example of generated local MC-DC coverage conditions. All MC-DC coverage conditions can be added to a subsystem as a synchronous observer (cf. Figure 11(a)). We use it to calculate the coverage of a given test suite by simulation. Figure 11 illustrates all 10 MC-DC conditions of the expression out in Listing 5.

Simulink Models into Equivalent Simpler Models

As presented in Section 3, the set of generated constructs in Simulink is limited: basic operators, logically executed subsystems with action blocks, and unit delays. However, the input language accepted by the CoCoSim toolchain is much larger.

The combination of the CoCoSim compilation of a Simulink+Stateflow model to Lustre and its translation back to simple Simulink provides an interesting feature. Addressing the analysis of the large set of constructs considered, such as Stateflow blocks or conditionally activated subsystems, is then reduced to the minimal subset of basic constructs. For instance, it could support the definition of new analysis tools that could concentrate the effort on the handling of this restricted subset of Simulink constructs while addressing a much larger set of input models. In Table 4, we give the example of the TCM model from Table 3. The original model contains around 27 unique blocks. After simplification of the model, we get 14 unique blocks (Constant, Delay, From, Gain, Goto, Inport, Logic, Outport, Product, RelationalOperator, Subsystem, Sum, Switch, Trigonometry) consisting of almost all of the basic blocks we use.

CONCLUSION

The presented approach enables the translation of Lustre nodes to Simulink subsystems. The proposed algorithm can be used to produce regular subsystems or to support the definition of contracts at the Simulink level, using Boolean flows.

The added value of our approach to alternative approaches such as those of Liu et al. [START_REF] Liu | From design contracts to component requirements verification[END_REF] is the production of basic Simulink subsystems relying only on primitive blocks such as unit delays, merge, and relational and arithmetic operators. It is also capable of addressing the complete input language of the compiler we used. Particularly, we can handle clocks, hierarchical definition through multiple Lustre nodes and Lustre automata. The implementation is however limited since it does not yet handle machine-level types nor external C functions, although this could technically be implemented since Simulink supports both constructs.

The approach has been validated on large use cases, demonstrating the behavioral equivalence between some compiled models.

The applications are numerous, from validation of the framework to support of formal specification or production of runnable proof evidence as synchronous observers. It is now integrated into the CoCoSim toolbox and is mature enough to be used automatically to provide feedback at the model level.

Future work includes the extension of the input language to enable the use of externally defined functions, such as C code, and the handling of machine data types (i.e., int8, uint8, int16, uint16 ...).

Fig. 1 .

 1 Fig. 1. Stopwatch example in Simulink.

Fig. 2 .

 2 Fig. 2. The overall architecture of CoCoSim.

Fig. 3 .

 3 Fig. 3. A subset of Lustre syntax.

Fig. 4 .

 4 Fig. 4. The normalized Lustre syntax.

Fig. 5 .

 5 Fig. 5. The Simulink model generated from the Lustre example of Listing 3.

Fig. 6 .

 6 Fig. 6. Primitive and branching constructs.

Fig. 7 .

 7 Fig. 7. Node calls.

Fig. 8 .

 8 Fig. 8. Branching construct for clocked expressions.

Fig. 9 .

 9 Fig. 9. Stateful Lustre node call is translated as a Simulink Resettable subsystem when the node foo is called with every operator.

Fig. 10 .

 10 Fig. 10. Action Subsystem with Held feature might need to be reset when it is re-activated.

Fig. 11 .

 11 Fig. 11. (a) MC-DC observer attached to its subsystem. (b) MC-DC conditions subsystem from inside. Each condition is colored green if it was covered during simulation and red otherwise.

Table 1 .

 1 Evolution of Expressions and Variables Using a Clock in the Stopwatch Example toggle False True False False False False True False False running False True True True True True False False False pre time) when not running is an integer stream. It starts with value 0 and then uses the previous value of time. This expression is clocked on the negation of the running clock. Notice that it is defined if and only if the previous expression is not defined. • Lines 10 and 11 define a merge expression. It is used to create a flow clocked on a particular clock using expressions clocked on subclocks of this particular clock. Here, this means the following:

	count(tick		1	2	3	4	5
	when running)
	(0 -> pre(time))	0						5	5	5
	when not running
	time	0	1	2	3	4	5	5	5	5
	• (0 ->

Table 3 .

 3 Experiments , safe (proven valid); U, unknown (i.e., unable to conclude with model checkers; to be evaluated through tests).[L] use cases were initially defined in Lustre and [S] in Simulink. Note the larger set of cases in the last column since it considers all subnodes as intermediate challenges.

					Simulink
		#loc	#nodes #vars	Design	Lustre Model Checking
					Verifier	Monolithic Compositional
	89 Benchmarks [L] 289,181	160	43,001 87 S + 2 U 87 S + 2 U	152 S + 8U
	TCM [S]	2,040	91	1,239	U	U	79 S + 12 U
	ROSACE [S]	926	94	520	U	U	87 S + 7 U
	FADEC [S]	68	1	46	U	S	S
	AOCS [S]	3,649	93	3,390	U	S	79 S + 14 U

S

Table 4 .

 4 Number of Unique Block Types in the Original TCM Model vs. the Simplified Version

			Original Model		Simplified Model
	Model #blocks #unique block types #blocks #unique block types
	TCM	570	27	7587	14

https://www.3ds.com/products-services/catia/products/stimulus/.

https://github.com/hbourbouh/lm_challenges.

This work was partially supported by grant ANR JCJC FEANICSES ANR-17-CE25-0018.