检索结果-内蒙古大学图书馆

1st International Workshop of the ERCIM Working-Group on Formal Methods for Industrial Critical Systems

作者： Poigne, A Morley, M Maffeis, O Holenderski, L Budde, R GMD Forschungszentrum Informat Tech GmbH SET Inst Syst Entwurfstech D-53754 St Augustin Germany

synchronous programming is available through several formally defined languages having very different characteristics: ESTEREL is imperative, while LUSTRE and SIGNAL are declarative in style;STATECHARTS and ARGOS are graphical languages that allow one to program by constructing hierarchical automata. Our motivation for taking the synchronous design paradigm further, integrating imperative, declarative (or dataflow), and graphical programming styles, is that real systems typically have components that match each of these profiles. This paper motivates our interest in the mixed language programming of embedded software around a number of examples, and sketches the semantical foundation of the SYNCHRONIE toolset which ensures a coherent computational model. This toolset supports a design trajectory that incorporates rapid prototyping and systematic testing for early design validation, an object oriented development methodology for long term software management, and formal verification at the level of automatically generated object code.

关键词： embedded software reactive systems synchronous programming synchronous automata

来源：评论

学校读者我要写书评

暂无评论

Hardware Implementation of OCAML Using a synchronous Functional Language 26th

Hardware Implementation of OCAML Using a Synchronous Functio...

引用

26th International Symposium on Practical Aspects of Declarative Languages (PADL)

作者： Sylvestre, Loic Serot, Jocelyn Chailloux, Emmanuel Sorbonne Univ CNRS LIP6 F-75005 Paris France Univ Clermont Auvergne CNRS Inst Pascal Clermont Auvergne INP F-63000 Clermont Ferrand France

ISBN: (纸本)9783031520372;9783031520389

We present a hardware implementation of the high-level multi-paradigm language OCAML using a declarative language called Eclat. Eclat is tailored for programming reactive hardware applications mixing interaction with physical devices and long-running computations. It is compiled to synthesizable hardware descriptions for configuring Field Programmable Gate Arrays (FPGAs). We have implemented the OCAML Virtual Machine as an Eclat function to execute complex computations (programmed in OCAML) in reactive applications (programmed in Eclat). This implementation comprises a bytecode interpreter and a runtime system with automatic memory management. The OCAML programmers can customize this runtime by defining external Eclat functions, i.e., hardware accelerators.

关键词： synchronous programming functional programming language design and implementation FPGA virtual machine OCAML

来源：评论

学校读者我要写书评

暂无评论

On Reconciling Concurrency, Sequentiality and Determinacy for Reactive Systems-A Sequentially Constructive Circuit Semantics for Esterel 18

On Reconciling Concurrency, Sequentiality and Determinacy fo...

引用

18th International Conference on Application of Concurrency to System Design (ACSD)

作者： Schulz-Rosengarten, Alexander Smyth, Steven von Hanxleden, Reinhard Mendler, Michael Univ Kiel Dept Comp Sci Kiel Germany Bamberg Univ Fac Informat Syst & Appl Comp Sci Bamberg Germany

ISBN: (纸本)9781538670132

A classic challenge in designing reactive systems is how to reconcile concurrency with determinacy. synchronous languages, such as Esterel, SyncCharts or SCADE, resolve this by providing a semantics that does not depend on run-time scheduling decisions. Esterel's circuit semantics is grounded in physics: An Esterel program is considered valid (constructive) iff it corresponds to a delay-insensitive circuit. The circuit semantics provides on the one hand a mathematically grounded semantics, based on constructive logic, on the other hand it gives a direct path to a data-flow style software implementation. However, Esterel's constructive semantics entails a rather restricted regime for handling sequential accesses to shared data. Thus many programs are rejected as being non-constructive, even though they have a very natural, determinate interpretation. We here present a sequentially constructive circuit semantics (SCC) that lifts this restriction, by distinguishing sequential and concurrent execution contexts. This permits an imperative style familiar to programmers versed in C, for example, without leaving the sound physical foundation of synchronous programming.

关键词： Reactive systems determinacy synchronous programming sequential constructiveness Esterel circuit semantics

来源：评论

学校读者我要写书评

暂无评论

Bridging the abstraction gap for the design of embedded reactive systems using Esterel - A case study

Bridging the abstraction gap for the design of embedded reac...

引用

ASME International Design Engineering Technical Conferences/Computers and Information in Engineering Conference

作者： Zauner, Martin Kramer, Michael Balog, Peter Univ Appl Sci Technikum Wien Dept Embedded Syst A-1200 Vienna Austria

ISBN: (纸本)9780791848050

New design methodologies at higher abstraction levels are necessary to deal with the increasing complexity of modem embedded systems. As a consequence, new design paradigms must supersede traditional design methods to bridge the abstraction gap which often exists between specification and implementation. This paper examines several examples which evaluate the applicability of Esterel, a language with well-defined semantics for specification and verification of reactive control systems. Implementation size, performance and design effort were selected as measures to assess the benefits of this design approach in comparison to a traditional one.

关键词： Esterel reactive systems FSM synchronous programming abstraction gap system design design methodologies

来源：评论

学校读者我要写书评

暂无评论

Synchronised Shared Memory and Model Checking: A Proof of Concept

Synchronised Shared Memory and Model Checking: A Proof of Co...

引用

Forum on specification and Design Languages (FDL)

作者： Aguado, Joaquin Duenas, Alejandra Otto Friedrich Univ Bamberg Fac Informat Syst & Appl Comp Sci Bamberg Germany ICN Business Sch Supply Chain & Informat Syst Management Nancy France

ISBN: (纸本)9781665418256

synchronous programming (SP) is a model of computation that supports concurrent thread composition and provides deterministic observable behaviour. A recent theory has extended SP with more and higher level clock-synchronised shared memory data types. The present paper implements this clock-synchronised shared memory ( CSM) theory and applies it from a model checking perspective. In the CSM theory, types are equipped with a synchronisation policy prescribing how concurrent calls to its methods must be organised. In a policy-constructive system all access methods of all objects can be scheduled in a policy-conformant manner without deadlocking. A policy-constructive system exhibits deterministic behaviour. In our modelling, synchronous policies get codified as neverclaims in PROMELA allowing the SPIN model checker to be used for searching an execution (interleaving) that satisfies the synchronous product of the never-claims. This interleaving, if exists, provides a policy-conformant schedule for the system model. This schedule verifies that the system is policy-constructive meaning that any policy-conformant schedule results in the same deterministic, observable input-output behaviour for the system.

关键词： synchronous programming clock-synchronised shared memory model checking determinism concurrency

来源：评论

学校读者我要写书评

暂无评论

Declarative Multithreaded programming

Declarative Multithreaded Programming

引用

IEEE 33rd International Computer Software and Applications Conference

作者： Mancilla, Blanca Plaice, John Univ New S Wales Sch Comp Sci & Engn Sydney NSW 2052 Australia

ISBN: (纸本)9781424445257

We demonstrate how TransLucid can be used as a reactive system by introducing sets and privileged dimensions for time and port in the language. At each instant, there is a set of active ports, where sets of equations, demands and threads are all registered. Each thread defines a sequence of (state, demand) pairs, and threads may interact through the overall set of equations. The en tire system remains fully declarative.

关键词： synchronous programming distributed computing declarative programming Cartesian programming multidimensional programming

来源：评论

学校读者我要写书评

暂无评论

A Type System for the Automatic Distribution of Higher-order synchronous Dataflow Programs 08

A Type System for the Automatic Distribution of Higher-order...

引用

Conference on Languages, Compilers, and Tools for Embedded Systems

作者： Delaval, Gwenael Girault, Alain Pouzet, Marc INR1A Rennes France

ISBN: (纸本)9781605581040

We address the design of distributed systems with synchronous dataflow programming languages. As modular design entails handling both architectural and functional modularity, our first contribution is to extend an existing synchronous dataflow programming language with primitives allowing the description of a distributed architecture and the localization of some expressions onto some processors. We also present a distributed semantics to formalize the distributed execution of synchronous programs. Our second contribution is to provide a type system, in order to infer the localization of non-annotated values by means of type inference and to ensure, at compilation time, the consistency of the distribution. Our third contribution is to provide a type-directed projection operation to obtain automatically, from a centralized typed program, the local program to be executed by each computing resource. The type system as well as the automatic distribution mechanism has been fully implemented in the compiler of an existing synchronous data-flow programming language.

关键词： synchronous programming distribution type systems functional programming

来源：评论

学校读者我要写书评

暂无评论

Resource control for synchronous cooperative threads

Resource control for synchronous cooperative threads

引用

15th International Conference on Concurrency Theory

作者： Amadio, Roberto M. Dal Zilio, Silvano Univ Paris 07 PPS UMR CNRS 7126 F-75221 Paris 05 France Lab Informat Fondamentale Marseille Marseille France

ISBN: (纸本)354022940X

We develop new methods to statically bound the resources needed for the execution of systems of concurrent, interactive threads. Our study is concerned with a synchronous model of interaction based on cooperative threads whose execution proceeds in synchronous rounds called instants. Our contribution is a system of compositional static analyses to guarantee that each instant terminates and to bound the size of the values computed by the system as a function of the size of its parameters at the beginning of the instant. Our method generalises an approach designed for first-order functional languages that relies on a combination of standard termination techniques for term rewriting systems and an analysis of the size of the computed values based on the notion of quasi-interpretation. We show that these two methods can be combined to obtain an explicit polynomial bound on the resources needed for the execution of the system during an instant. As a second contribution, we introduce a virtual machine and a related bytecode thus producing a precise description of the resources needed for the execution of a system. In this context, we present a suitable control flow analysis that allows to formulate the static analyses for resource control at bytecode level. (C) 2006 Elsevier B.V. All rights reserved.

关键词： synchronous programming resource bound termination quasi-interpretations virtual machine bytecode verification

来源：评论

学校读者我要写书评

暂无评论

A type system for the automatic distribution of higher-order synchronous dataflow programs

引用

ACM SIGPLAN NOTICES 2008年第7期43卷 101-110页

作者： Delaval, Gwenael Girault, Alain Pouzet, Marc INRIA Rennes France INRIA Rhone Alpes Grenoble France Univ Paris 11 LRI F-91405 Orsay France

关键词： languages synchronous programming distribution type systems functional programming

来源：评论

学校读者我要写书评

暂无评论

Implementing synchronous reactive components upon multiprocessor platforms

引用

JOURNAL OF SYSTEMS ARCHITECTURE 2021年 116卷 102027-102027页

作者： Baruah, Sanjoy Washington Univ St Louis MO 63110 USA

Model-based design methodologies based on the synchrony assumption are widely used in many safety-critical application domains. The synchrony assumption asserts that actions (such as the execution of code) occur instantaneously;however, physical platforms obviously do not possess this property. This paper considers a scheduling problem that arises when one seeks to implement programs that are written under the synchrony assumption upon actual multiprocessor platforms, and proposes algorithms for solving this problem exactly and approximately.

关键词： synchronous programming Multiprocessor scheduling Deadlines Integer Linear Program Approximation algorithm

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：