EDBT 2026 Demo / reviewers in the wild / expert
Albert Benveniste
dblp:14/6732
· DBLP profile ↗
72ranked-venue papers
32as first author
3since 2021 · last 2025
0000-0003-3352-4137ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 25 · 13 first-author · 2 since 2021Applied, interdisciplinary, general and emerging computing · 16 · 12 first-author · 1 since 2021Software engineering, systems software and programming languages · 14 · 4 first-authorSystems, architecture and hardware · 6 · 3 first-authorGraphics, computer vision, multimedia, augmented reality and games · 4Artificial intelligence and machine learning · 3Computer networks · 3 · 1 first-authorDatabases, data management, data science and information retrieval · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | HypercontractsabstractAbstract Contract theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. This paper introduces hypercontracts , a compositional assume-guarantee formalism that supports the expression and manipulation of hyperproperties of arbitrary structure. Hyperproperties can express characteristics such as mean response times, security attributes, and robustness that lie outside the expressivity of trace properties and contracts. By considering hyperproperties with interval and downward closed structure, we obtain specializations of the theory of hypercontracts to interval and conic hypercontracts. These specializations are more general than assume-guarantee contracts but come with finite descriptions, while enabling new applications of contracts in security and autonomous cyber-physical system design. Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
Formal Methods Syst. Des. | 2 |
| 2025 | Correction: Hypercontracts
Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
Formal Methods Syst. Des. | 2 |
| 2025 | Pacti: Assume-Guarantee Contracts for Efficient Compositional Analysis and DesignabstractContract-based design is a method to facilitate modular design of systems. While there has been substantial progress on the theory of contracts, there has been less progress on practical algorithms for the algebraic operations in the theory. In this article, we present (1) principles to implement a contract-based design tool at scale and (2) Pacti, a tool that can efficiently compute these operations. We illustrate the use of Pacti in a variety of case studies. Inigo Incer, Apurva Badithela, Josefine Graebener, Piergiuseppe Mallozzi, Ayush Pandey 0001, Nicolas Rouquette, Sheng-Jung Yu, Albert Benveniste, Benoît Caillaud, Richard M. Murray, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
ACM Trans. Cyber Phys. Syst. | 8 |
| 2018 | Building a Hybrid Systems Modeler on Synchronous Languages PrinciplesabstractHybrid systems modeling languages that mix discrete and continuous time signals and systems are widely used to develop cyber-physical systems where control software interacts with physical devices. Compilers play a central role, statically checking source models, generating intermediate representations for testing and verification, and producing sequential code for simulation and execution on target platforms. This paper presents a novel approach to the design and implementation of a hybrid systems language, built on synchronous language principles and their proven compilation techniques. The result is a hybrid systems modeling language in which synchronous programming constructs can be mixed with ordinary differential equations (ODEs) and zero-crossing events, and a runtime that delegates their approximation to an off-the-shelf numerical solver. We propose an ideal semantics based on nonstandard analysis, which defines the execution of a hybrid model as an infinite sequence of infinitesimally small time steps. It is used to specify and prove correct three essential compilation steps: 1) a type system that guarantees that a continuous-time signal is never used where a discrete-time one is expected and conversely; 2) a type system that ensures the absence of combinatorial loops; and 3) the generation of statically scheduled code for efficient execution. Our approach has been evaluated in two implementations: the academic language Zélus, which extends a language reminiscent of Lustre with ODEs and zero-crossing events, and the industrial prototype Scade Hybrid, a conservative extension of Scade 6. Albert Benveniste, Timothy Bourke, Benoît Caillaud, Jean-Louis Colaço, Cédric Pasteur, Marc Pouzet |
Proc. IEEE | 1 |
| 2017 | Structural Analysis of Multi-Mode DAE SystemsabstractDifferential Algebraic Equation (DAE) systems constitute the mathematical model supporting physical modeling languages such as Modelica, VHDL-AMS, or Simscape. Unlike ODEs, they exhibit subtle issues because of their implicit latent equations and related differentiation index. Multi-mode DAE (mDAE) systems are much harder to deal with, not only because of their mode-dependent dynamics, but essentially because of the events and resets occurring at mode transitions. Unfortunately, the large literature devoted to the numerical analysis of DAEs does not cover the multi-mode case. It typically says nothing about mode changes. This lack of foundations cause numerous difficulties to the existing modeling tools. Some models are well handled, others are not, with no clear boundary between the two classes. In this paper we develop a comprehensive mathematical approach to the structural analysis of mDAE systems which properly extends the usual analysis of DAE systems. We define a constructive semantics based on nonstandard analysis and show how to produce execution schemes in a systematic way. Albert Benveniste, Benoît Caillaud, Hilding Elmqvist, Khalil Ghorbal, Martin Otter, Marc Pouzet |
HSCC | 1 |
| 2016 | Loosely Time-Triggered Architectures: Improvements and ComparisonsabstractLoosely Time-Triggered Architectures (LTTAs) are a proposal for constructing distributed embedded control systems. They build on the quasi-periodic architecture, where computing units executenearly periodically, by adding a thin layer of middleware that facilitates the implementation of synchronous applications. In this article, we show how the deployment of a synchronous application on a quasi-periodic architecture can be modeled using a synchronous formalism. Then we detail two protocols,Back-PressureLTTA, reminiscent of elastic circuits, andTime-BasedLTTA, based on waiting. Compared to previous work, we present controller models that can be compiled for execution, a simplified version of the Time-Based protocol and optimizations for systems using broadcast communication. We also compare the LTTA approach with architectures based on clock synchronization. Guillaume Baudart, Albert Benveniste, Timothy Bourke |
ACM Trans. Embed. Comput. Syst. | 2 |
| 2015 | Loosely time-triggered architectures: improvements and comparisonsabstractLoosely Time-Triggered Architectures (LTTAs) are a proposal for constructing distributed embedded control systems. They build on the quasi-periodic architecture, where computing units execute `almost periodically', by adding a thin layer of middleware that facilitates the implementation of synchronous applications. In this paper, we show how the deployment of a synchronous application on a quasi-periodic architecture can be modeled using a synchronous formalism. Then we detail two protocols, Back-Pressure LTTA, reminiscent of elastic circuits, and Time-Based LTTA, based on waiting. Compared to previous work, we present controller models that can be compiled for execution and a simplified version of the Time-Based protocol. We also compare the LTTA approach with architectures based on clock synchronization. Guillaume Baudart, Albert Benveniste, Timothy Bourke |
EMSOFT | 2 |
| 2014 | A type-based analysis of causality loops in hybrid systems modelersabstractExplicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete- and continuous-time behaviors with complex interactions between them. A key issue in their compilation is the static detection of algebraic or causality loops. Such loops can cause simulations to deadlock and prevent the generation of statically scheduled code. Albert Benveniste, Timothy Bourke, Benoît Caillaud, Bruno Pagano, Marc Pouzet |
HSCC | 1 |
| 2014 | QoS-aware management of monotonic service orchestrations
Albert Benveniste, Claude Jard, Ajay Kattepur, Sidney Rosario, John A. Thywissen |
Formal Methods Syst. Des. | 1 |
| 2014 | Foreword in honor of Glynn Winskel
Albert Benveniste, Claude Jard, Samy Abbes |
Theor. Comput. Sci. | 1 |
| 2014 | Application of branching cells to QoS aware service orchestrations
Albert Benveniste, Claude Jard, Samy Abbes |
Theor. Comput. Sci. | 1 |
| 2012 | An overview of the career of Paul CaspiabstractThis session is dedicated to Paul Caspi. It is made of five talks, each of them addressing one aspect of Paul Caspi's contributions to the development of safe embedded software and systems: synchronous languages and models, the implementation of synchronous languages, the relation between functional and synchronous languages, the relation between continuous and discrete models, and the definition of embedded software and systems master curricula. This session is only a selection of recent work; Paul Caspi also worked on dependability and fault-tolerance, code distribution, and formal verification with theorem provers. Albert Benveniste, Edward A. Lee, Marc Pouzet, Stavros Tripakis, Florence Maraninchi |
EMSOFT | 1 |
| 2012 | Negotiation Strategies for Probabilistic Contracts in Web Services OrchestrationsabstractService Level Agreements (SLAs) have been proposed in the context of web services to maintain acceptable quality of service (QoS) performance. This is specially crucial for composite service orchestrations that invoke many atomic services to render functionality. A consequence of SLA management entails efficient negotiation protocols among orchestrations and invoked services. In composite services where data and QoS (modeled in a probabilistic setting) interact, it is difficult to select an atomic service for negotiation, in order to improve end-to-end QoS performance. A superior improvement in one negotiated domain (eg. latency) might mean deterioration in another domain (eg. cost); improvement in one of the invoked services may be annulled by another due to the control flow specified in the orchestration. In this paper, we propose a integer programming formulation based on first order stochastic dominance as a strategy for re-negotiation over multiple services. A consequence of this is better end-to-end performance of the orchestration compared to random selection of services for re-negotiation. We also demonstrate this optimal strategy can be applied to negotiation protocols specified in languages such as Orc. Such strategies are necessary for composite services where QoS contributions from individual atomic services vary significantly. Ajay Kattepur, Albert Benveniste, Claude Jard |
ICWS | 2 |
| 2012 | Non-standard semantics of hybrid systems modelers
Albert Benveniste, Timothy Bourke, Benoît Caillaud, Marc Pouzet |
J. Comput. Syst. Sci. | 1 |
| 2011 | A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous codeabstractHybrid modeling tools like Simulink have evolved from simulation platforms into development platforms on which testing, verification and code generation are also performed. It is critical to ensure that the results of simulation, compilation and verification are consistent. Synchronous languages have addressed these issues but only for discrete systems. Albert Benveniste, Timothy Bourke, Benoît Caillaud, Marc Pouzet |
EMSOFT | 1 |
| 2011 | Optimizing Decisions in Web Services Orchestrations
Ajay Kattepur, Albert Benveniste, Claude Jard |
ICSOC | 2 |
| 2011 | Divide and recycle: types and compilation for a hybrid synchronous languageabstractHybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step. Albert Benveniste, Timothy Bourke, Benoît Caillaud, Marc Pouzet |
LCTES | 1 |
| 2011 | A Modal Interface Theory for Component-based DesignabstractThis paper presents the modal interface theory, a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-based model, which allows the designer to express assum Jean-Baptiste Raclet, Éric Badouel, Albert Benveniste, Benoît Caillaud, Axel Legay, Roberto Passerone |
Fundam. Informaticae | 3 |
| 2010 | Loosely Time-Triggered Architectures for Cyber-Physical SystemsabstractCyber-Physical Systems require distributed architectures to support safety critical real-time control. Kopetz' Time-Triggered Architectures (TTA) have been proposed as both an architecture and a comprehensive paradigm for systems architecture, for such systems. To relax the strict requirements on synchronization imposed by TTA, Loosely Time-Triggered Architectures (LTTA) have been recently proposed. In LTTA, computation and communication units at all triggered by autonomous, non synchronized, clocks. Communication media act as shared memories between writers and readers and communication is non blocking. In this paper we review the different variants of LTTA and discuss their principles and usage. Albert Benveniste |
DATE | 1 |
| 2010 | A unifying view of loosely time-triggered architecturesabstractCyber-Physical Systems require distributed architectures to support safety critical real-time control. Kopetz' Time-Triggered Architectures (TTA) have been proposed as both an architecture and a comprehensive paradigm for systems architecture, for such systems. To relax the strict requirements on synchronization imposed by TTA, Loosely Time-Triggered Architectures (LTTA) have been recently proposed. In LTTA, computation and communication units at all triggered by autonomous, non synchronized, clocks. Communication media act as shared memories between writers and readers and communication is non blocking. In this paper we pursue our previous work by providing a unified presentation of the two variants of LTTA (token- and time-based), with simplified analyses. We compare these two variants regarding performance and robustness and we provide ways to combine them. Albert Benveniste, Anne Bouillard, Paul Caspi |
EMSOFT | 1 |
| 2010 | Document Based Modeling of Web Services Choreographies Using Active XMLabstractThis paper proposes a document based framework for the modeling of web-based choreographies involving a tight combination of workflow and data management. Our starting point is Active XML proposed by S. Abiteboul — AXML documents are XML documents with embedded service calls. We enhance Active XML with a rich notion of interface and we propose an effective technique to decide if provided services and needs of callers (defined as interfaces) are compatible. We also explicitly take distribution into account and allow for the composition of distributed AXML systems. Loïc Hélouët, Albert Benveniste |
ICWS | 2 |
| 2010 | Variability Modeling and QoS Analysis of Web Services OrchestrationsabstractThe ever-growing choice in diverse services is making service orchestration variability an essential aspect of a composite web service. Influence of this variation on the Quality of Service (QoS) of a composite service is critical and the focus of our work. In this paper, we present a methodology to first model orchestration variability using a feature diagram (FD). The FD specifies a product line of orchestrations represented as configurations of invoked/rejected atomic services. Second, due to the potentially large set of configurations we employ combinatorial testing techniques to automatically generate configurations covering all valid pair wise interactions between services. Third, we analyze QoS variation for each configuration using probabilistic models of QoS. Using a crisis management system case study we experimentally show that pair wise generation covers all QoS outliers and eliminates analysis of > 75% of all possible configurations. The QoS analysis of the pair wise configurations reveals unsafe/ineffective configurations, helps determine realistic Service Level Agreements (SLAs), and provides valuable feedback to help remodel an orchestration. Ajay Kattepur, Sagar Sen, Benoit Baudry, Albert Benveniste, Claude Jard |
ICWS | 4 |
| 2009 | Monotonicity in Service Orchestrations
Anne Bouillard, Sidney Rosario, Albert Benveniste, Stefan Haar |
Petri Nets | 3 |
| 2009 | Modal interfaces: unifying interface automata and modal specificationsabstractThis paper presents a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-based model, which allows to make assumptions on the environment and propose an optimistic view for composition : two components can be composed if there is an environment where they can work together. Modal specification is a language theoretic account of a fragment of the modal mu-calculus logic that is more complete but which does not allow to distinguish between the environment and the component. Partial unifications of these two frameworks have been explored recently. A first attempt by Larsen et al. considers modal interfaces, an extension of modal specifications that deals with compatibility issues in the composition operator. However, this composition operator is incorrect. A second attempt by Raclet et al. gives a different perspective, and emphasises on conjunction and residuation of modal specifications, including when interfaces have dissimilar alphabets, but disregards interface compatibility. The present paper contributes a thorougher unification of the two theories by correcting the modal interface composition operator presented in the paper by Larsen et al., drawing a complete picture of the modal interface algebra, and pushing even further the comparison between interface automata, modal automata and modal interfaces. Jean-Baptiste Raclet, Éric Badouel, Albert Benveniste, Benoît Caillaud, Axel Legay, Roberto Passerone |
EMSOFT | 3 |
| 2009 | Concurrency, sigma-Algebras, and Probabilistic Fairness
Samy Abbes, Albert Benveniste |
FoSSaCS | 2 |
| 2009 | Actors without Directors: A Kahnian View of Heterogeneous Systems
Paul Caspi, Albert Benveniste, Roberto Lublinerman, Stavros Tripakis |
HSCC | 2 |
| 2009 | Flexible Probabilistic QoS Management of Transaction Based Web Services OrchestrationsabstractIn this paper we extend our previous work on soft probabilistic contracts for QoS management, from the particular case of "response time", to general QoS parameters. Our study covers composite QoS parameters dealing not only with time aspects but also with quality of data. We also study contract composition (how to derive QoS contracts for an orchestration from the QoS contracts with its called services), and contract monitoring. Our approach supports comprehensive and flexible QoS management within a probabilistic framework. Sidney Rosario, Albert Benveniste, Claude Jard |
ICWS | 2 |
| 2009 | Monitoring probabilistic SLAs in Web service orchestrationsabstractWeb services are software applications that are published over the Web, and can be searched and invoked by other programs. New Web services can be formed by composing elementary services, such composite services are called Web service orchestrations. Quality of service (QoS) issues for Web service orchestrations deeply differ from corresponding QoS issues in network management. In an open world of Web services, service level agreements (SLAs) play an important role. They are contracts defining the obligations and rights between the provider of a Web service and a client with respect to the services' function and quality. In a previous work we have advocated using soft contracts of probabilistic nature, for the QoS part of contracts. Soft contracts have no hard bounds on QoS parameters, but rather probability distributions for them. An essential component of SLA management is the continuous monitoring of the performance of called Web services, to check for violation of the agreed SLA. In this paper we propose a statistical technique for QoS contract run time monitoring. Our technique is compatible with the use of soft probabilistic contracts. Sidney Rosario, Albert Benveniste, Claude Jard |
Integrated Network Management | 2 |
| 2008 | Implementing Synchronous Models on Loosely Time Triggered ArchitecturesabstractSynchronous systems offer a clean semantics and an easy verification path at the expense of often inefficient implementations. Capturing design specifications as synchronous models and then implementing the specifications in a less restrictive platform allow to address a much larger design space. The key issue in this approach is maintaining semantic equivalence between the synchronous model and its implementation. We address this problem by showing how to map a synchronous model onto a loosely time-triggered architecture that is fairly straightforward to implement as it does not require global synchronization or blocking communication. We show how to maintain semantic equivalence between specification and implementation using an intermediate model (similar to a Kahn process network but with finite queues) that helps in defining the transformation. Performance of the semantic preserving implementation is studied for the general case as well as for a few special cases. Stavros Tripakis, Claudio Pinello, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Paul Caspi, Marco Di Natale |
IEEE Trans. Computers | 3 |
| 2008 | True-concurrency probabilistic models: Markov nets and a law of large numbers
Samy Abbes, Albert Benveniste |
Theor. Comput. Sci. | 2 |
| 2008 | Composing heterogeneous reactive systemsabstractWe present a compositional theory of heterogeneous reactive systems. The approach is based on the concept of tags marking the events of the signals of a system. Tags can be used for multiple purposes from indexing evolution in time (time stamping) to expressing relations among signals, like coordination (e.g., synchrony and asynchrony) and causal dependencies. The theory provides flexibility in system modeling because it can be used both as a unifying mathematical framework to relate heterogeneous models of computations and as a formal vehicle to implement complex systems by combining heterogeneous components. In particular, we introduce an algebra of tag structures to define heterogeneous parallel composition formally. Morphisms between tag structures are used to define relationships between heterogeneous models at different levels of abstraction. In particular, they can be used to represent design transformations from tightly synchronized specifications to loosely-synchronized implementations. The theory has an important application in the correct-by-construction deployment of synchronous design on distributed architectures. Albert Benveniste, Benoît Caillaud, Luca P. Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Embed. Comput. Syst. | 1 |
| 2008 | Probabilistic QoS and Soft Contracts for Transaction-Based Web Services OrchestrationsabstractService level agreements (SLAs), or contracts, have an important role in web services. They define the obligations and rights between the provider of a web service and its client, about the function and the Quality of the service (QoS). For composite services like orchestrations, contracts are deduced by a process called QoS contract composition, based on contracts established between the orchestration and the called web services. Contracts are typically stated as hard guarantees (e.g., response time always less than 5 msec). Using hard bounds is not realistic, however, and more statistical approaches are needed. In this paper we propose using soft probabilistic contracts instead, which consist of a probability distribution for the considered QoS parameter—in this paper, we focus on timing. We show how to compose such contracts, to yield a global probabilistic contract for the orchestration. Our approach is implemented by the TOrQuE tool. Experiments on TOrQuE show that overly pessimistic contracts can be avoided and significant room for safe overbooking exists. An essential component of SLA management is then the continuous monitoring of the performance of called web services, to check for violations of the SLA. We propose a statistical technique for run-time monitoring of soft contracts. Sidney Rosario, Albert Benveniste, Stefan Haar, Claude Jard |
IEEE Trans. Serv. Comput. | 2 |
| 2007 | Loosely time-triggered architectures based on communication-by-samplingabstractWe address the problem of mapping a set of processes which communicate synchronously on a distributed platform. The Time Triggered Architecture (TTA) proposed by Kopetz for the communication mechanism of a distributed platform offers a direct mapping that would preserve the semantics of the specification. However, its exact implementation may, at times, be problematic as it requires the distributed platform to have the clocks of its components perfectly synchronized. We propose as implementation architecture a relaxation of TTA called Loosely Time-Triggered Architecture (LTTA), in which computing units perform writes into and reads from the communication medium independently, triggered by local, quasi-periodic but non synchronized, clocks. LTTA offers some of the advantages of TTA with lower hardware cost and greater flexibility. So far LTTA was studied for single directional two-users communications over an LTT bus. General topology was not studied. In this paper we propose a design flow that ensures semantics preservation for an LTT communication network with arbitrary topology. Key elements are two new protocols for clock regeneration and predictive traffic shaping. Our approach relies on a mathematical Model of Communication (MoC) that we describe in detail. Albert Benveniste, Paul Caspi, Marco Di Natale, Claudio Pinello, Alberto L. Sangiovanni-Vincentelli, Stavros Tripakis |
EMSOFT | 1 |
| 2007 | Probabilistic QoS and soft contracts for transaction based Web servicesabstractWeb services orchestrations and choreographies require establishing quality of service (QoS) contracts with the user. This is achieved by performing QoS composition, based on contracts established between the orchestration and the called Web services. These contracts are typically stated in the form of hard guarantees (e.g., response time always less than 5 msec). In this paper we propose using soft contracts instead. Soft contracts are characterized by means of probability distributions for QoS parameters. We show how to compose such contracts, to yield a global contract (probabilistic) for the orchestration. Our approach is implemented by the TOrQuE tool. Experiments on TOrQuE show that overly pessimistic contracts can be avoided and significant room for safe overbooking exists. Sidney Rosario, Albert Benveniste, Stefan Haar, Claude Jard |
ICWS | 2 |
| 2006 | Communication by sampling in time-sensitive distributed systemsabstractIn time-sensitive systems writing to and reading from the communication medium is on a purely time-triggered but asynchronous basis. Writes and reads can occur at any time and the data are stored and sustained until overwritten. We study how to maintain data semantics when the duration of the actions change from specification to implementation.In doing so, we rely on tag systems formerly introduced by the authors. The exibility of tag systems allows handling the problem in a formal, yet tractable way. Albert Benveniste, Benoît Caillaud, Luca P. Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli, Stavros Tripakis |
EMSOFT | 1 |
| 2006 | Foundations for Web Services Orchestrations: Functional and QoS Aspects, JointlyabstractWeb services orchestrations require a firm mathematical basis for their development, regarding both their functional and QoS characteristics. We provide such a basis in the form of a model based on colored Petri net systems. Our approach allows evaluating end-to-end QoS of the orchestration with the help of the QoS of the called sites. Sidney Rosario, Albert Benveniste, Stefan Haar, Claude Jard |
ISoLA | 2 |
| 2006 | Concurrency in Synchronous Systems
Dumitru Potop-Butucaru, Benoît Caillaud, Albert Benveniste |
Formal Methods Syst. Des. | 3 |
| 2006 | True-concurrency probabilistic models: Branching cells and distributed probabilities for event structures
Samy Abbes, Albert Benveniste |
Inf. Comput. | 2 |
| 2005 | Tag machinesabstractHeterogeneity is a challenge to overcome in the design of embedded systems. We presented in the recent past a theory for the composition of heterogeneous components based on tagged systems, a behavioral (denotational) framework. in this paper, we present an operational view of tagged systems, where we focus on tag machines as mathematical artifacts that act as finitary generators of tagged systems. Properties of tag machines are investigated. A fundamental theorem on homogeneous compositionality is given as a first step towards an operational theory of heterogeneous systems. Albert Benveniste, Benoît Caillaud, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 1 |
| 2005 | Branching Cells as Local States for Event Structures and Nets: Probabilistic Applications
Samy Abbes, Albert Benveniste |
FoSSaCS | 2 |
| 2005 | Guidelines for a graduate curriculum on embedded software and systemsabstractThe design of embedded real-time systems requires skills from multiple specific disciplines, including, but not limited to, control, computer science, and electronics. This often involves experts from differing backgrounds, who do not recognize that they address similar, if not identical, issues from complementary angles. Design methodologies are lacking in rigor and discipline so that demonstrating correctness of an embedded design, if at all possible, is a very expensive proposition that may delay significantly the introduction of a critical product. While the economic importance of embedded systems is widely acknowledged, academia has not paid enough attention to the education of a community of high-quality embedded system designers, an obvious difficulty being the need of interdisciplinarity in a period where specialization has been the target of most education systems. This paper presents the reflections that took place in the European Network of Excellence Artist leading us to propose principles and structured contents for building curricula on embedded software and systems. Paul Caspi, Alberto L. Sangiovanni-Vincentelli, Luís Almeida 0001, Albert Benveniste, Bruno Bouyssounouse, Giorgio C. Buttazzo, Ivica Crnkovic, Werner Damm, Jakob Engblom, Gerhard Fohler, Marisol García-Valls, Hermann Kopetz, Yassine Lakhnech, François Laroussinie, Luciano Lavagno, Giuseppe Lipari, Florence Maraninchi, Philipp Peti, Juan Antonio de la Puente, Norman Scaife, Joseph Sifakis, Robert de Simone, Martin Törngren, Paulo Veríssimo, Andy J. Wellings, Reinhard Wilhelm, Tim A. C. Willemse, Wang Yi 0001 |
ACM Trans. Embed. Comput. Syst. | 4 |
| 2004 | Heterogeneous reactive systems modeling: capturing causality and the correctness of loosely time-triggered architectures (LTTA)abstractWe present an extension of a mathematical framework proposed by the authors to deal with the composition of heterogeneous reactive systems. Our extended framework encompasses diverse models of computation and communication such as synchronous, asynchronous, causality-based partial orders, and earliest execution times. We introduce an algebra of tag structures and morphisms between tag sets to define heterogeneous parallel composition formally and we use a result on pullbacks from category theory to handle properly the case of systems derived by composing many heterogeneous components. The extended framework allows us to establish theorems, from which design techniques for correct-by-construction deployment of abstract specifications can be derived. We illustrate this by providing a complete formal support for correct-by-construction distributed deployment of a synchronous design specification over an ltta medium. Albert Benveniste, Benoît Caillaud, Luca P. Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 1 |
| 2003 | Distributed Monitoring of Concurrent and Asynchronous Systems
Albert Benveniste, Stefan Haar, Eric Fabre, Claude Jard |
CONCUR | 1 |
| 2003 | Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment
Albert Benveniste, Luca P. Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 1 |
| 2003 | The synchronous languages 12 years laterabstractTwelve years ago, Proceedings of the IEEE devoted a special section to the synchronous languages. This paper discusses the improvements, difficulties, and successes that have occured with the synchronous languages since then. Today, synchronous languages have been established as a technology of choice for modeling, specifying, validating, and implementing real-time embedded applications. The paradigm of synchrony has emerged as an engineer-friendly design method based on mathematically sound tools. Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul Le Guernic, Robert de Simone |
Proc. IEEE | 1 |
| 2002 | A Protocol for Loosely Time-Triggered Architectures
Albert Benveniste, Paul Caspi, Paul Le Guernic, Hervé Marchand, Jean-Pierre Talpin, Stavros Tripakis |
EMSOFT | 1 |
| 2002 | Toward an Approximation Theory for Computerised Control
Paul Caspi, Albert Benveniste |
EMSOFT | 2 |
| 2002 | Non-massive, Non-high Performance, Distributed Computing: Selected Issues
Albert Benveniste |
Euro-Par | 1 |
| 2001 | Foreword
Albert Benveniste, Axel Poigné |
Formal Methods Syst. Des. | 1 |
| 2000 | A Semantics of UML State-Machines Using Synchronous Pre-Order Transition SystemsabstractThe synchronous model of concurrency has demonstrated its practicality for the design of circuits, embedded systems, reactive and distributed systems. This model allows to design systems around an idealized notion of deterministic concurrency, which is much easier to deal with than classical, nondeterministic, asynchronous concurrency. Compiling, optimizing, and verifying programs are done using powerful techniques. We take advantage of this rich background by presenting a translation of UML state-machines into a pivot synchronous calculus, based on mathematical notions of pre-orders, in the aim of providing an integrated development cycle for the reliable deployment of synchronous system specifications over asynchronous networks. In this paper we first present the structure of UML state-machines. Compared with earlier studies on that matter the structure under consideration supports, e.g., composite transition and history. Then, we give a brief presentation of the pivot formalism, BDL, which is used to finally give a formal semantics of UML state-machines in terms of pre-ordered transition systems. Jean-Pierre Talpin, Albert Benveniste, Paul Le Guernic |
ISORC | 3 |
| 2000 | Compositionality in Dataflow Synchronous Languages: Specification and Distributed Code Generation
Albert Benveniste, Benoît Caillaud, Paul Le Guernic |
Inf. Comput. | 1 |
| 1999 | From Synchrony to Asynchrony
Albert Benveniste, Benoît Caillaud, Paul Le Guernic |
CONCUR | 1 |
| 1998 | Algebraic Techniques for Timed Systems
Albert Benveniste, Claude Jard, Stéphane Gaubert |
CONCUR | 1 |
| 1998 | BDL, A Language of Distributed Reactive ObjectsabstractWe introduce the definition of a language of distributed reactive objects, a Behaviour Description Language (BDL), as a unified medium for specifying, verifying, compiling and validating object-oriented distributed reactive systems. One of the novelties in BDL is its seamless integration into the Unified Modeling Language approach (UML). BDL supports a description of objects interaction which respects both the functional architecture of system designs and the declarative style of diagram descriptions. This support is implemented by means of a partial-order theoretical framework. This framework allows to specify both the causality and the control models of object interactions independently of any hypothesis on the actual configuration of the system. Given the description of such a configuration, the use of BDL offers new perspectives for a flexible verification of systems by modeling them as an asynchronous network of synchronous components. It allows an optimized code generation by using compilation techniques developed for synchronous languages. It permits an accurate validation and test of applications by supporting the manipulation of both causal and control dependencies. BDL aims at maximizing the re-usability of high-level specifications while minimizing programming effort and test-case based validation of distributed systems. Jean-Pierre Talpin, Albert Benveniste, Benoît Caillaud, Claude Jard, Zakaria Bouziane, Hubert Canon |
ISORC | 2 |
| 1995 | A Calculus of Stochastic Systems for the Specification, Simulation, and Hidden State Estimation of Mixed Stochastic/Nonstochastic Systems
Albert Benveniste, Bernard C. Levy, Eric Fabre, Paul Le Guernic |
Theor. Comput. Sci. | 1 |
| 1995 | Accuracy analysis for wavelet approximationsabstract"Constructive wavelet networks" are investigated as a universal tool for function approximation. The parameters of such networks are obtained via some "direct" Monte Carlo procedures. Approximation bounds are given. Typically, it is shown that such networks with one layer of "wavelons" achieve an L(2) error of order O(N(-(rho/d))), where N is the number of nodes, d is the problem dimension and rho is the number of summable derivatives of the approximated function. An algorithm is also proposed to estimate this approximation based on noisy input-output data observed from the function under consideration. Unlike neural network training, this estimation procedure does not rely on stochastic gradient type techniques such as the celebrated "backpropagation" and it completely avoids the problem of poor convergence or undesirable local minima. Bernard Delyon, Anatoli B. Juditsky, Albert Benveniste |
IEEE Trans. Neural Networks | 3 |
| 1992 | SIGNAL as a Model for Real-Time and Hybrid Systems
Albert Benveniste, Michel Le Borgne, Paul Le Guernic |
ESOP | 1 |
| 1992 | A Denotational Theory of Synchronous Reactive Systems
Albert Benveniste, Paul Le Guernic, Yves Sorel, Michel Sorine |
Inf. Comput. | 1 |
| 1992 | Modeling and estimation of multiresolution stochastic processesabstractAn overview is provided of the several components of a research effort aimed at the development of a theory of multiresolution stochastic modeling and associated techniques for optimal multiscale statistical signal and image processing. A natural framework for developing such a theory is the study of stochastic processes indexed by nodes on lattices or trees in which different depths in the tree or lattice correspond to different spatial scales in representing a signal or image. In particular, it is shown how the wavelet transform directly suggests such a modeling paradigm. This perspective then leads directly to the investigation of several classes of dynamic models and related notions of multiscale stationarity in which scale plays the role of a time-like variable. The investigation of models on homogeneous trees is emphasized. The framework examined here allows for consideration, in a very natural way, of the fusion of data from sensors with differing resolutions. Also, thanks to the fact that wavelet transforms do an excellent job of 'compressing' large classes of covariance kernels, it is seen that these modeling paradigms appear to have promise in a far broader context than one might expect.> Michèle Basseville, Albert Benveniste, Kenneth C. Chou, Stuart A. Golden, Ramine Nikoukhah, Alan S. Willsky |
IEEE Trans. Inf. Theory | 2 |
| 1992 | Wavelet networksabstractA wavelet network concept, which is based on wavelet transform theory, is proposed as an alternative to feedforward neural networks for approximating arbitrary nonlinear functions. The basic idea is to replace the neurons by ;wavelons', i.e., computing units obtained by cascading an affine transform and a multidimensional wavelet. Then these affine transforms and the synaptic weights must be identified from possibly noise corrupted input/output data. An algorithm of backpropagation type is proposed for wavelet network training, and experimental results are reported. Albert Benveniste |
IEEE Trans. Neural Networks | 2 |
| 1991 | Approximation by nonlinear wavelet networksabstractBy combining the class of feedforward neural networks and results from the wavelet theory, a class of networks call wavelet networks that can be used to approximate any nonlinear function is proposed. A stochastic gradient procedure for black-box identification of nonlinear static systems based on this class of networks is developed. This method was inspired by both the neural networks and the wavelet decomposition. The basic idea is to replace the neurons by more powerful computing units obtained by cascading an affine transform and a multidimensional wavelet. Then these affine transforms and the synaptic weights must be identified from possibly noise corrupted input/output data. It is pointed out that for comparable number of adjusted coefficients, the complexity of input/output map realized by the wavelet network is much smaller than that realized by the wavelet decomposition, since many more units are needed in the latter case.> Albert Benveniste |
ICASSP | 2 |
| 1991 | The synchronous approach to reactive and real-time systemsabstractThe state of the art in real-time programming is briefly reviewed. The synchronous approach is then introduced informally and its possible impact on the design of real-time and reactive systems is discussed. The authors present and discuss the application fields and the principles of synchronous programming. The major concern of the synchronous approach is to base synchronous programming languages on mathematical models. This makes it possible to handle compilation, logical correctness proofs, and verification of real-time programs in a formal way, leading to a clean and precise methodology for design and programming.> Albert Benveniste, Gerard Berry |
Proc. IEEE | 1 |
| 1991 | Synchronous Programming with Events and Relations: the SIGNAL Language and Its Semantics
Albert Benveniste, Paul Le Guernic, Christian Jacquemot |
Sci. Comput. Program. | 1 |
| 1989 | Multiscale statistical signal processingabstractA novel framework for multiscale statistical signal processing is introduced. Its purpose is to provide a statistical toolbox to analyze properties of signals involving time and scale simultaneously. Stationary processes over the dyadic tree are borrowed from harmonic analysts for this purpose, and a new partial order is proposed to model causality in scale. Autoregressive processes are investigated, and it is shown that Schur-Levinson parameterizations play a crucial role. As expected from the model, the restriction at a given scale (level) of a sample of such processes looks like a fractal, i.e. a random signal appearing similar whether seen from close or far away.> Michèle Basseville, Albert Benveniste |
ICASSP | 2 |
| 1986 | Detection and diagnosis of abrupt changes in modal characteristics of nonstationary digital signalsabstractNew "instrumental" tests for detecting and diagnosing changes in the poles of a signal having unknown time-varying zeros are proposed. Numerical results for nonstationary scalar signals are given. The extension of these tests to the vector case may be used for vibration monitoring. Michèle Basseville, Albert Benveniste, George V. Moustakides |
IEEE Trans. Inf. Theory | 2 |
| 1984 | Modeling of Atmospheric Disturbances in Meteorological PicturesabstractThis paper describes a model-based approach to perform tracking of extratropical atmospheric disturbances from a sequence of satellite cloud-cover images. More precisely, it deals with the estimation of motion of these spiral-shaped cloud systems (both translational and rotational motion), and the measurement of the evolution of their shape. Tracking is achieved by recording from one image to the next the changes of the model parameter values. A maximum likelihood criterion is used in the process of fitting model to sensed data. The defined model takes into account geometric and intensity aspects. Such an approach readily yields global information on the disturbance cloud system of interest. As a requirement in such an application is robustness to noise, to this end two versions of the modeling have been considered. Patrick Bouthemy, Albert Benveniste |
IEEE Trans. Pattern Anal. Mach. Intell. | 2 |
| 1984 | Blind EqualizersabstractBlind equalizers do not require any known training sequence for the startup period, but can rather perform at any time the equalization directly on the data stream. In this paper, a general approach is presented for designing efficient blind equalizers for one and two independent carrier transmission systems; a special algorithm is given for the CCITT V29 constellation. Albert Benveniste, Maurice Goursat |
IEEE Trans. Commun. | 1 |
| 1984 | Recursive Estimation of Local Characteristics of Edges in TV Pictures as Applied to ADPCM CodingabstractIn this paper, an algorithm is presented for extracting edges and estimating their local characteristics in TV pictures; the algorithm is designed for application to adaptive DPCM coding of TV pictures and it has the following properties: 1) it takes into account the causality constraint encountered in DPCM coding; 2) it is fitted to the line-by-line scanning of TV pictures; 3) it is fast, involving only a small amount of computation, and thus allowing real-time implementation. The whole processing is split into a local preprocessing and a global processing where the characteristics of the edges are renewed recursively line by line. This algorithm was used for implementing an adaptive choice of the prediction in DPCM coding of TV pictures. Christian Richard, Albert Benveniste, Francis Kretz |
IEEE Trans. Commun. | 2 |
| 1983 | Sequential segmentation of nonstationary digital signals using spectral analysis
Michèle Basseville, Albert Benveniste |
Inf. Sci. | 2 |
| 1983 | Sequential detection of abrupt changes in spectral characteristics of digital signalsabstractThe problem of sequential detection of abrupt changes in the spectral behavior of a digital signal is addressed. This problem arises, for example, in the sequential segmentation of nonstationary digital signals such as speech, (EEG) electroencepholograms, (ECG) electrocardiogram, and geophysical signals. The limitations of a classical test will be emphasized, and some new algorithms will be presented and compared via a simulation study and from a theoretical point of view. Michèle Basseville, Albert Benveniste |
IEEE Trans. Inf. Theory | 2 |
| 1982 | Motion of edges and motion estimation in a sequence of T.V. picturesabstractWe present in this paper an algorithm for motion estimation pel by pel in a sequence of television pictures. This estimator which will be used for a motion compensated coding, must be fitted any type of scene or motion. Techniques we used, are adaptative algorithm with detectors of ruptures without delays. Hence we estimate an a priori motion information on spatial edges where are chiefly located the abrupt changes in motion. Claude Labit, Albert Benveniste |
ICASSP | 2 |
| 1982 | Identification of vibrating structures subject to non stationary excitation : A non stationary stochastic realization problemabstractThe vector signal delivered by accelerometers measuring the vibrations of a structure subject to a non stationary excitation may be modelled as a Gauss-Markov signal with constant state-transition and observation matrices, but non stationary excitation noise. It is shown that some stochastic realization algorithms remain robust even used on a single (non stationary) sample of the signal ; we developp some algorithms which are recursive in the order of the model and we investigate the effect of model reduction. Marc Prevosto, Albert Benveniste, Bruno Barnouin |
ICASSP | 2 |