Portail HAL Ensta
Not a member yet
11080 research outputs found
Sort by
Dolmen: FPGA Swarm for Safety and Liveness Verification
No full textInternational audienceTo ensure correctness of critical systems, swarm verification produces proofs of failure on systems too large to be verified using model-checking. Recent research efforts exploit both intrinsic parallelism and low-latency on-chip memory offered by FPGAs to achieve 3 orders of magnitude speedups over software. However, these approaches are limited to safety verification that encodes only what the system should not do. Liveness properties express what the system should do, and are widely used in the verification of operating systems, distributed systems, and communication protocols. Both safety and liveness properties are of paramount importance to ensure systems correctness. This paper presents Dolmen, the first FPGA implementation of a swarm verification engine that supports both safety and liveness properties. Dolmen features a deeply pipelined verification core, along with a scalable architecture to allow high-frequency synthesis on large FPGAs. Our experimental results, on a Xilinx Virtex Ultrascale+ FPGA, show that the Dolmen architecture can achieve up to 4 orders of magnitude speedups compared to software model-checking
Coupling Architecture Framework and Operation Research: the Case of NAF with Cost and Delay Driven Multi-Criteria Scheduling
No full textInternational audienceArchitecture frameworks are essential tools to model system of systems. The aim of the NATO Architecture Framework (NAF) is to provide a standard for developing and describing architectures for both military and business use. A main purpose is to contribute to the analysis and development of alternative architectures, evaluate and compare them. In this regard AF itself is not sufficient to evaluate alternative architectures and evaluation tools are needed ideally in a seamless way. In this paper we propose a coupling between NAF and operations research, NAF-OR, through linear programming in order to assess the various possible scheduling and resource derived from the different architectures. This in turn improves system design productivity. While management techniques in system engineering and program modifications are based on best effort to respect schedule and budget, this article introduces the benefits of using optimization to input validated data NAF through a significant example using multi-objective scheduling problem introducing NAF-OR, a method that combines NAF and Operation research
Equations de Maxwell en présence de méta-matériaux
No full textThe main subject of this thesis is the study of time-harmonic electromagnetic waves in a heterogeneous medium composed of a dielectric and a negative material (i.e. with a negative dielectric permittivity ε and/or a negative magnetic permeability μ) which are separated by an interface with a conical tip. Because of the sign-change in ε and/or μ, the Maxwell’s equations can be ill-posed in the classical L2 −frameworks. On the other hand, we know that when the two associated scalar problems, involving respectively ε and μ, are well-posed in H1, the Maxwell’s equations are well-posed. By combining the T-coercivity approach with the Mellin analysis in weighted Sobolev spaces, we present, in the first part of this work, a detailed study of these scalar problems. We prove that for each of them, the well-posedeness in H1 is lost iff the associated contrast belong to some critical set called the critical interval. These intervals correspond to the sets of negative contrasts for which propagating singularities, also known as black hole waves, appear at the tip. Contrary to the case of a 2D corner, for a 3D tip, several black hole waves can exist. Explicit expressions of these critical intervals are obtained for the particular case of circular conical tips. For critical contrasts, using the Mandelstam radiation principle, we construct functional frameworks in which well-posedness of the scalar problems is restored. The physically relevant framework is selected by a limiting absorption principle. In the process, we present a new numerical strategy for 2D/3D scalar problems in the non-critical case. This approach, presented in the second part of this work, contrary to existing ones, does not require additional assumptions on the mesh near the interface. The third part of the thesis concerns Maxwell’s equations with one or two critical coefficients. By using new results of vector potentials in weighted Sobolev spaces, we explain how to construct new functional frameworks for the electric and magnetic problems, directly related to the ones obtained for the two associated scalar problems. If one uses the setting that respects the limiting absorption principle for the scalar problems, then the settings provided for the electric and magnetic problems are also coherent with the limiting absorption principle. Finally, the last part is devoted to the homogenization process for time-harmonic Maxwell’s equations and associated scalar problems in a 3D domain that contains a periodic distribution of inclusions made of negative material. Using the T-coercivity approach, we obtain conditions on the contrasts such that the homogenization results is possible for both the scalar and the vector problems. Interestingly, we show that the homogenized matrices associated with the limit problems are either positive definite or negative definite.Le sujet principal de cette thèse est l’étude de la propagation des ondes électromagnétiques, en régime harmonique, dans un milieu hétérogène composé d’un diélectrique et d’un matériau négatif (c’est-à-dire avec une permittivité diélectrique négative ε et/ou une perméabilité magnétique négative μ) qui sont séparés par une interface avec une pointe conique. En raison du changement de signe de ε et/ou μ, les équations de Maxwell peuvent être mal posées dans les cadres classiques (basés sur l’espace L2). D’autre part, nous savons que lorsque les deux problèmes scalaires associés, impliquant respectivement ε et μ, sont bien posés dans H1, les équations de Maxwell sont bien posées. En combinant la méthode de la T-coercivité avec l’analyse de Mellin dans les espaces de Sobolev à poids, nous présentons, dans la première partie de ce travail, une étude détaillée de ces problèmes scalaires. Nous prouvons que pour chacun d’entre eux, le caractère bien posé dans H1 est perdu si et seulement si le contraste associé appartient à un ensemble critique appelé intervalle critique. Ces intervalles correspondent aux ensembles de contrastes négatifs pour lesquels des singularités propagatives, aussi appelées ondes de trou noir, apparaissent à l’extrémité de la pointe. Contrairement au cas d’un coin 2D, pour une pointe 3D, plusieurs ondes de trou noir peuvent exister. Des expressions explicites de ces intervalles critiques sont obtenues pour le cas particulier des pointes coniques circulaires. Pour les contrastes critiques, en utilisant le principe de radiation de Mandelstam, nous construisons des cadres fonctionnels dans lesquels le caractère bien posé des problèmes scalaires est restauré. Le cadre physiquement pertinent est sélectionné par un principe d’absorption limite. En outre, nous présentons, dans la deuxième partie de ce travail, une nouvelle méthode numérique pour les problèmes scalaires dans le cas des contrastes non-critiques. Cette approche, contrairement aux techniques existantes, ne nécessite pas d’hypothèses supplémentaires sur le maillage au voisinage de l’interface. La troisième partie de la thèse concerne l’étude des équations de Maxwell avec un ou deux coefficients critiques. En utilisant de nouveaux résultats de potentiels vecteurs dans des espaces de Sobolev à poids, nous expliquons comment construire de nouveaux cadres fonctionnels pour les problèmes électrique et magnétique, qui sont directement liés à ceux obtenus pour les deux problèmes scalaires associés. Si l’on utilise le cadre qui respecte le principe d’absorption limite pour les problèmes scalaires, alors les cadres fournis pour les problèmes électrique et magnétique sont également cohérents avec le principe d’absorption limite. Enfin, la dernière partie porte sur des résultats d’homogénéisation des équations de Maxwell harmoniques et des problèmes scalaires associés dans un domaine 3D qui contient une distribution périodique d’inclusions faites de matériau négatif. En utilisant l’approche de la T-coercivité, nous obtenons des conditions sur les contrastes telles que le processus d’homogénéisation est possible pour les problèmes scalaires et vectoriels. De façon peu intuitive, nous montrons que les matrices homogénéisées associées auxproblèmes limites sont soit définies positives, soit définies négatives
Sketching the Best Approximate Quantum Compiling Problem
No full text10 pages, 4 figures, 1 tableInternational audienceThis paper considers the problem of quantum compilation from an optimization perspective by fixing a circuit structure of CNOTs and rotation gates then optimizing over the rotation angles. We solve the optimization problem classically and consider algorithmic tools to scale it to higher numbers of qubits. We investigate stochastic gradient descent and two sketch-and-solve algorithms. For all three algorithms, we compute the gradient efficiently using matrix-vector instead of matrix-matrix computations. Allowing for a runtime on the order of one hour, our implementation using either sketch-and-solve algorithm is able to compile 9 qubit, 27 CNOT circuits; 12 qubit, 24 CNOT circuits; and 15 qubit, 15 CNOT circuits. Without our algorithmic tools, standard optimization does not scale beyond 9 qubit, 9 CNOT circuits, and, beyond that, is theoretically dominated by barren plateaus
An Ellipsoidal Predictor-Corrector State Estimation Scheme for Linear Continuous-Time Systems With Bounded Parameters and Bounded Measurement Errors
No full textInternational audienceFor linear time-invariant dynamic systems with exactly known coefficients of their system matrices for which measurements with bounded errors are available at discrete time instants, an optimal polygonal state estimation scheme was recently published. This scheme allows for tightly enclosing all possible state trajectories in presence of uncertain, but bounded, system inputs which may be varying arbitrarily within in their bounds. Moreover, this approach is also capable of accounting for uncertainty related to the measurement time instants. However, the drawback of this polygonal technique is its rapidly increasing complexity for larger system dimensions. For that reason, the polygonal state enclosures are replaced by a computationally less expensive, but nearly optimal, ellipsoidal enclosure technique in this paper. Numerical simulations for representative benchmark examples focusing both on applications with precisely known and uncertain parameters conclude this contribution
Construction d'arbres de décision optimaux
No full textInternational audienceConstruction d'arbres de décision optimau
Guided mode resonator coupled with nanocrystal intraband absorption
No full textInternational audienceIntraband absorption in doped nanocrystals offers an interesting alternative to narrow band gap materials to explore mid infrared optoelectronic device designs. However, the performance of such device clearly lags behind the ones relying on intrinsic materials. Livache et al. have proposed a dye sensitized approach to overcome the limitations observed from intraband materials (high dark current, slow response, low activation energy), where the intraband absorber is coupled to an undoped material which takes care of the charge conduction. Here, we unveil the coupling between both materials using mid-infrared transient reflectivity (TR) measurement. We show that hybrid material displays a unique feature in the TR signal that we attribute to a charge transfer and for which the dynamic matches the hopping time. We then developed a strategy to enhance the photodetection performances of the hybrid material by coupling for the first time intraband absorption to a light resonator. The latter is used to enhance the absorption by a factor 4 and enables an increase of the operating temperature by 80 K compared to the reference device. The obtained device matches the performance of best devices relying on intraband absorption
Quantification of Parkinsonian Kinematic Patterns in Body-Segment Regions During Locomotion
No full textInternational audienceDiagnosis and treatment of Parkinson's Disease (PD) are typically supported by a kinematic gait analysis. Nonetheless, the main drawbacks of the classical analysis, based on a reduced set of markers, are the loss of small dynamical changes, the invasive methodology, and the sparse representation from few points, restricting the disease analysis. This work aims to perform a robust regional kinematic characterization, which may result in a potential digital biomarker of the disease to complement personalized analysis, treatment and monitoring of PD. Methods: This work introduces a markerless computational framework based on a full body-segment kinematic characterization related with PD motor alterations. Firstly, a set of dense motion trajectories are computed to represent locomotion. Such trajectories are grouped using a deep learning based body segmentation, that partitions the human silhouette into regions corresponding to the head, trunk and limbs. Each resultant region is described using dartboard-like kinematic histograms computed along the trajectories
A Composable Look at Updatable Encryption
No full textUpdatable Encryption (UE), as originally defined by Boneh et al. in 2013, addresses the problem of key rotation on outsourced data while maintaining the communication complexity as low as possible. The security definitions for UE schemes have been constantly updated since then. However, the security notion that is best suited for a particular application remains unclear. To solve this problem in the ciphertext-independent setting, we use the Constructive Cryptography (CC) framework defined by Maurer et al. in 2011. We define and construct a resource that we call Updatable Server-Memory Resource USMR, and study the confidentiality guarantees it achieves when equipped with a UE protocol, that we also model in this framework. With this methodology, we are able to construct resources tailored for each security notion. In particular, we prove that IND-UE-RCCA is the right security notion for many practical UE schemes. As a consequence, we notably rectify a claim made by Boyd et al. , namely that their IND-UE security notion is better than the IND-ENC+UPD notions, in that it hides the age of ciphertexts. We show that this is only true when ciphertexts can leak at most one time per epoch. We stress that UE security is thought of in the context of adaptive adversaries, and UE schemes should thus bring post-compromise confidentiality guarantees to the client. To handle such adversaries, we use an extension of CC due to Jost et al. and give a clear, simple and composable description of the post-compromise security guarantees of UE schemes. We also model semi-honest adversaries in CC. Our adaption of the CC framework to UE is generic enough to model other interactive protocols in the outsourced storage setting
Des « bilingues scolaires » dans le paysage sociolinguistique breton ?
No full textInternational audienceDans le prolongement des travaux menés sur le terrain breton à propos du bilinguisme scolaire du jeune enfant, cet écrit vient soumettre à discussion la pertinence de déterminer et mobiliser une nouvelle notion en lien avec cet objet de recherche, la notion de « bilingue scolaire ». Cette idée de conceptualisation vient poursuivre les réflexions scientifiques sur le bilinguisme dit « précoce », en abordant la question des conditions d’appropriation ou de non appropriation d’une langue minoritaire, telle que le breton, transmise par voie de scolarisation. Il s’agit alors de donner à voir comment la détermination et l’usage de cette notion peut apparaître heuristique à la fois sur le plan théorique et du point de vue des perspectives socio-didactiques