检索结果-南通市图书馆

Foreword to the special section on synchronous programming

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2013年第5期7卷 595-597页

作者： Jean-Pierre TALPIN inria rennes-Bretagne-Atlantique Rennes 35042 France

1 Introduction Embedded systems are ubiquitous. In applications ranging from avionics, automotive, and industrial process control all the way to the handheld personal digital assistants （PDAs）, cell phones, and bio-...

关键词：

Polychronous automata and their use for formal validation of AADL models

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2019年第4期13卷 677-697页

作者： Thierry GAUTIER Clement GUY Alexandre HONORAT Paul LE GUERNIC Jean-Pierre TALPIN Loic BESNARD Univ. rennes Inria Rennes-Bretagne-Atlantique Research Centre F-35000 Rennes France Univ. rennes CNRS IRISA F-35000 Rennes France

This paper investigates how state diagrams can be best represented in the polychronous model of computation (MoC) and proposes to use this model for code validation of behavior specifications in architecture analysis & design language (AADL). In this relational MoC, the basic objects are signals, which are related through dataflow equations. Signals are associated with logical clocks, which provide the capability to describe systems in which components obey multiple clock rates. We propose a model of finite-state automata, called polychronous automata, which is based on clock relationships. A specificity of this model is that an automaton is submitted to clock constraints, which allows one to specify a wide range of control-related configurations, being either reactive or restrictive with respect to their control environment. A semantic model is defined for these polychronous automata, which relies on boolean algebra of clocks. Based on a previously defined modeling method for AADL software architectures using the polychronous MoC, the proposed model is used as a formal model for the AADL behavior annex. This is illustrated with a case study involving an adaptive cruise control system.

关键词： architecture modeling formal semantics finitestate automaton polychronous model synchronous concurrency code generation AADL

Long-Time Turbulence Model Deduced from the Navier-Stokes Equations

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Chinese Annals of Mathematics,Series B 2015年第5期36卷 883-894页

作者： Roger LEWANDOWSKI IRMAR and Fluminance Team University of Rennes 1 and INRIA Campus Beaulieu

The author shows the existence of long-time averages to turbulent solutions of the Navier-Stokes equations and determines the equations satisfied by them, involving a Reynolds stress that is shown to be dissipative.

关键词： Navier-Stokes方程湍流模型方程推导雷诺兹应力平均值耗散

Exploring system architectures in AADL via Polychrony and SynDEx

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2013年第5期7卷 627-649页

作者： Huafeng YU Yue MA Thierry GAUTIER Loc BESNARD Jean-Pierre TALPIN Paul Le GUERNIC Yves SOREL inria rennes-Bretagne Atlantique 263 av. du Général LeclercRennes 35042 France IRISA/CNRS 263 av. du Général LeclercRennes 35042 France inria Paris-Rocquencourt Domaine de VoluceauBP 105Le Chesnay Cedex 78153 France

Architecture analysis&design language(AADL)has been increasingly adopted in the design of embedded systems,and corresponding scheduling and formal verification have been well ***,little work takes code distribution and architecture exploration into account,particularly considering clock constraints,for distributed multi-processor *** this paper,we present an overview of our approach to handle these concerns,together with the associated toolchain,***,in order to avoid semantic ambiguities of AADL,the polychronous/multiclock semantics of AADL,based on a polychronous model of computation,is *** synthesis is then carried out in Polychrony,which bridges the gap between the polychronous semantics and the synchronous semantics of *** same timing semantics is always preserved in order to ensure the correctness of the transformations between diferent *** distribution and corresponding scheduling is carried out on the obtained SynDEx model in the last step,which enables the exploration of architectures originally specified in *** contribution provides a fast yet efcient architecture exploration approach for the design of distributed real-time and embedded *** avionic case study is used here to illustrate our approach.

关键词： Polychrony Signal AADL SynDEx architecture exploration modeling timing analysis scheduling distribution

Variance reduction for generalized likelihood ratio method by conditional Monte Carlo and randomized Quasi-Monte Carlo methods

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Journal of Management Science and Engineering 2022年第4期7卷 550-577页

作者： Yijie Peng Michael C.Fu Jiaqiao Hu Pierre L’Ecuyer Bruno Tuffin Peking University Beijing100871China University of Maryland College ParkMD20742USA Stony Brook University Stony BrookNY11794-3600USA University of Montreal MontrealQuebecH3T 1J4Canada inria Univ RennesCNRSIRISACampus de Beaulieu35042Rennes CedexFrance

The generalized likelihood ratio(GLR)method is a recently introduced gradient estimation method for handling discontinuities in a wide range of sample *** put the GLR methods from previous work into a single framework,simplify regularity conditions to justify the unbiasedness of GLR,and relax some of those conditions that are difficult to verify in ***,we combine GLR with conditional Monte Carlo methods and randomized quasi-Monte Carlo methods to reduce the *** experiments show that variance reduction could be significant in various applications.

关键词： Simulation Stochastic gradient estimation Conditional Monte Carlo Randomized quasi-Monte Carlo

TRAP:trace runtime analysis of properties

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2020年第3期14卷 15-29页

作者： Daian YUE Vania JOLOBOFF Frederic MALLET MOE Trustworthy Software International Joint Lab East China Normal UniversityShanghai 200062China inria Rennes 35042France Universite Cote d'Azur CNRSINRIAI3SSophia Antipolis 06900France

We present a method and a tool for the verification of causal and temporal properties for embedded *** analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware and embedded *** main originality lies in the use of logical clocks to abstract away irrelevant information from the *** propose a model-based approach that relies on domain specific languages(DSL).A first DSL,called TISL(trace item specification language),captures the relevant data structures.A second DSL,called STML(simulation trace mapping language),abstracts the simulation raw data into logical clocks,abstracting simulation data into relevant observation probes and thus reducing the trace streams *** third DSL,called TPSL,defines a set of behavioral patterns that include widely used temporal *** is meant for users who are not familiar with temporal *** pattern is transformed into an *** the automata are executed concurrently and each one raises an error if and when the related TPSL property is *** contribution is the integration of this pattern-based property specification language into the SimSoC virtual prototyping framework without requiring to recompile all the simulation models when the properties *** illustrate our approach with experiments that show the possibility to use multi-core platforms to parallelize the simulation and verification processes,thus reducing the verification time.

关键词： runtime verification trace analysis property specification logical clocks simulation virtual prototyping

Rotational Forms of Large Eddy Simulation Turbulence Models:Modeling and Mathematical Theory

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Chinese Annals of Mathematics,Series B 2021年第1期42卷 17-40页

作者： Luigi C.BERSELLI Roger LEWANDOWSKI Dinh Duong NGUYEN Universita di Pisa Dipartimento di MatematicaVia Buonarroti 1/c1-56127 Pisa Italy IRMAR UMR CNRS 6625University of Rennes 1 and FLUMINANCE TeamINRIA RennesFrance

In this paper the authors present a derivation of a back-scatter rotational Large Eddy Simulation model,which is the extension of the Baldwin&Lomax model to nonequilibrium *** model is particularly designed to mathematically describe a fluid filling a domain with solid walls and consequently the differential operators appearing in the smoothing terms are degenerate at the *** the derivation of the model,the authors prove some of the mathematical properties coming from the weighted energy estimates,which allow to prove existence and uniqueness of a class of regular weak solutions.

关键词： Fluid mechanics Turbulence models Rotational Large Eddy Simulation models Navier-Stokes equations

Wavelets and Optical Flow Motion Estimation

在线全文

学校读者我要写书评

暂无评论

Numerical Mathematics(Theory,Methods and Applications) 2013年第1期6卷 116-137页

作者： P.Dérian P.Héas C.Herzet E.Mémin Departments of Physics and Geosciences California State University ChicoChicoCA 95929-0555USA inria rennes-Bretagne Atlantique Campus de Beaulieu35042 Rennes CEDEXFrance

This article describes the implementation of a simple wavelet-based optical-flow motion estimator dedicated to continuous motions such as fluid flows. The waveletrepresentation of the unknown velocity field is considered. This scale-space representation, associated to a simple gradient-based optimization algorithm, sets up a welldefined multiresolution framework for the optical flow estimation. Moreover, a verysimple closure mechanism, approaching locally the solution by high-order polynomialsis provided by truncating the wavelet basis at fine scales. Accuracy and efficiency of theproposed method is evaluated on image sequences of turbulent fluid flows.

关键词： Wavelets optical flow motion estimation large displacements fluid flows

Fluid Flow Estimation with Multiscale Ensemble Filters Based on Motion Measurements Under Location Uncertainty

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Numerical Mathematics(Theory,Methods and Applications) 2013年第1期6卷 21-46页

作者： Sébastien Beyou Thomas Corpetti Sai Gorthi Etienne Mémin inria/FLUMINANCE 35042 Rennes CedexFrance CNRS/LETG-rennes-Costel Campus Villejean Place du recteur Henri Le Moal CS *** Rennes cedexFrance Indian Institute of Space Science and Technology Valiamala P.O.Thiruvananthapuram–695547Kerala India

This paper proposes a novel multi-scale fluid flow data assimilation approach,which integrates and complements the advantages of a Bayesian sequential assimilationtechnique, the Weighted Ensemble Kalman filter (WEnKF) [27]. The data assimilation proposed in this work incorporates measurement brought by an efficient multiscalestochastic formulation of the well-known Lucas-Kanade (LK) estimator. This estimatorhas the great advantage to provide uncertainties associated to the motion measurements at different scales. The proposed assimilation scheme benefits from this multiscale uncertainty information and enables to enforce a physically plausible dynamicalconsistency of the estimated motion fields along the image sequence. Experimentalevaluations are presented on synthetic and real fluid flow sequences.

关键词： Data assimilation stochastic filter particle filters fluid motion estimation