BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Laurent Fribourg

Laurent Fribourg appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Systems and Controleess.SYLogic in Computer ScienceOperating SystemsDistributed, Parallel, and Cluster ComputingProgramming LanguagesSoftware EngineeringSymbolic Computation

Catalog footprint

What is connected

9works
8topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

9 published item(s)

preprint2020arXiv

Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method: The Brusselator and biped examples

The phenomenon of phase synchronization was evidenced in the 17th century by Huygens while observing two pendulums of clocks leaning against the same wall. This phenomenon has more recently appeared as a widespread phenomenon in nature, and turns out to have multiple industrial applications. The exact parameter values of the system for which the phenomenon manifests itself are however delicate to obtain in general, and it is interesting to find formal sufficient conditions to guarantee phase synchronization. Using the notion of reachability, we give here such a formal method. More precisely, our method selects a portion $S$ of the state space, and shows that any solution starting at $S$ returns to $S$ within a fixed number of periods $k$. Besides, our method shows that the components of the solution are then (almost) in phase. We explain how the method applies on the Brusselator reaction-diffusion and the biped walker examples.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis

The proceedings consist of a keynote paper by Alberto followed by 6 invited papers written by Lorenzo Clemente (U. Warsaw), Alain Finkel (U. Paris-Saclay), John Gallagher (Roskilde U. and IMDEA Software Institute) et al., Neil Jones (U. Copenhagen) et al., Michael Leuschel (Heinrich-Heine U.) and Maurizio Proietti (IASI-CNR) et al.. These invited papers are followed by 4 regular papers accepted at VPT 2020 and the papers of HCVS 2020 which consist of three contributed papers and an invited paper on the third competition of solvers for Constrained Horn Clauses. In addition, the abstracts (in HTML format) of 3 invited talks at VPT 2020 by Andrzej Skowron (U. Warsaw), Sophie Renault (EPO) and Moa Johansson (Chalmers U.), are included.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Robust optimal control using dynamic programming and guaranteed Euler's method

Set-based integration methods allow to prove properties of differential systems, which take into account bounded disturbances. The systems (either time-discrete, time-continuous or hybrid) satisfying such properties are said to be "robust". In the context of optimal control synthesis, the set-based methods are generally extensions of numerical optimal methods of two classes: first, methods based on convex optimization; second, methods based on the dynamic programming principle. Heymann et al. have recently shown that, for certain systems of low dimension, the second numerical method can give better solutions than the first one. They have built a solver (Bocop) that implements both numerical methods. We show in this paper that a set-based extension of a method of the second class which uses a guaranteed Euler integration method, allows us to find such good solutions. Besides, these solutions enjoy the property of robustness against uncertainties on initial conditions and bounded disturbances. We demonstrate the practical interest of our method on an example taken from the numerical Bocop solver. We also give a variant of our method, inspired by the method of Model Predictive Control, that allows us to find more efficiently an optimal control at the price of losing robustness.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Control of nonlinear switched systems based on validated simulation

We present an algorithm of control synthesis for nonlinear switched systems, based on an existing procedure of state-space bisection and made available for nonlinear systems with the help of validated simulation. The use of validated simulation also permits to take bounded perturbations and varying parameters into account. It is particularly interesting for safety critical applications, such as in aeronautical, military or medical fields. The whole approach is entirely guaranteed and the induced controllers are correct-by-design.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Distributed Synthesis of State-Dependent Switching Control

We present a correct-by-design method of state-dependent control synthesis for linear discrete-time switching systems. Given an objective region R of the state space, the method builds a capture set S and a control which steers any element of S into R. The method works by iterated backward reachability from R. More precisely, S is given as a parametric extension of R, and the maximum value of the parameter is solved by linear programming. The method can also be used to synthesize a stability control which maintains indefinitely within R all the states starting at R. We explain how the synthesis method can be performed in a distributed manner. The method has been implemented and successfully applied to the synthesis of a distributed control of a concrete floor heating system with 11 rooms and 2^11 = 2048 switching modes.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Correct-by-design Control Synthesis for Multilevel Converters using State Space Decomposition

High-power converters based on elementary switching cells are more and more used in the industry of power electronics owing to various advantages such as lower voltage stress and reduced power loss. However, the complexity of controlling such converters is a major challenge that the power manufacturing industry has to face with. The synthesis of industrial switching controllers relies today on heuristic rules and empiric simulation. The state of the system is not guaranteed to stay within the limits that are admissible for its correct electrical behavior. We show here how to apply a formal method in order to synthesize a correct-by-design control that guarantees that the power converter will always stay within a predefined safe zone of variations for its input parameters. The method is applied in order to synthesize a correct-by-design control for 5-level and 7-level power converters with a flying capacitor topology. We check the validity of our approach by numerical simulations for 5 and 7 levels. We also perform physical experimentations using a prototype built by SATIE laboratory for 5 levels.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Toward Parametric Timed Interfaces for Real-Time Components

We propose here a framework to model real-time components consisting of concurrent real-time tasks running on a single processor, using parametric timed automata. Our framework is generic and modular, so as to be easily adapted to different schedulers and more complex task models. We first perform a parametric schedulability analysis of the components using the inverse method. We show that the method unfortunately does not provide satisfactory results when the task periods are consid- ered as parameters. After identifying and explaining the problem, we present a solution adapting the model by making use of the worst-case scenario in schedulability analysis. We show that the analysis with the inverse method always converges on the modified model when the system load is strictly less than 100%. Finally, we show how to use our parametric analysis for the generation of timed interfaces in compositional system design.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems

Parametric analysis is a powerful tool for designing modern embedded systems, because it permits to explore the space of design parameters, and to check the robustness of the system with respect to variations of some uncontrollable variable. In this paper, we address the problem of parametric schedulability analysis of distributed real-time systems scheduled by fixed priority. In particular, we propose two different approaches to parametric analysis: the first one is a novel technique based on classical schedulability analysis, whereas the second approach is based on model checking of Parametric Timed Automata (PTA). The proposed analytic method extends existing sensitivity analysis for single processors to the case of a distributed system, supporting preemptive and non-preemptive scheduling, jitters and unconstrained deadlines. Parametric Timed Automata are used to model all possible behaviours of a distributed system, and therefore it is a necessary and sufficient analysis. Both techniques have been implemented in two software tools, and they have been compared with classical holistic analysis on two meaningful test cases. The results show that the analytic method provides results similar to classical holistic analysis in a very efficient way, whereas the PTA approach is slower but covers the entire space of solutions.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Synthesis of Switching Rules for Ensuring Reachability Properties of Sampled Linear Systems

We consider here systems with piecewise linear dynamics that are periodically sampled with a given period τ . At each sampling time, the mode of the system, i.e., the parameters of the linear dynamics, can be switched, according to a switching rule. Such systems can be modelled as a special form of hybrid automata, called "switched systems", that are automata with an infinite real state space. The problem is to find a switching rule that guarantees the system to still be in a given area V at the next sampling time, and so on indefinitely. In this paper, we will consider two approaches: the indirect one that abstracts the system under the form of a finite discrete event system, and the direct one that works on the continuous state space. Our methods rely on previous works, but we specialize them to a simplified context (linearity, periodic switching instants, absence of control input), which is motivated by the features of a focused case study: a DC-DC boost converter built by electronics laboratory SATIE (ENS Cachan). Our enhanced methods allow us to treat successfully this real-life example.

0 citations0 reviewsNo code linkedOpen access