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

Incorporating Symbolic Discrete Controller Synthesis into a Virtual Robot Experimental Platform: An Implementation with Collaborative Unmanned Aerial Vehicle Robots

引用

DRONES 2024年第5期8卷 206-206页

作者： Ozbaltan, Mete Caska, Serkan Erzurum Tech Univ Fac Engn & Architecture Dept Comp Engn TR-25050 Erzurum Turkiye Manisa Celal Bayar Univ Hasan Ferdi Turgutlu Technol Fac Dept Mech Engn TR-45400 Manisa Turkiye

We introduce a modeling framework aimed at incorporating symbolic discrete controller synthesis (DCS) into a virtual robot experimental platform. This framework involves symbolically representing the behaviors of robotic systems along with their control objectives using synchronous programming techniques. We employed DCS algorithms through the reactive synchronous environment ReaX to generate controllers that fulfill specified objectives. These resulting controllers were subsequently deployed on the virtual robot experimental platform Simscape. To demonstrate and validate our approach, we provide an implementation example involving collaborative UAV robots.

关键词： UAV symbolic discrete controller synthesis virtual robot experimental platform collaborative robots reactive systems synchronous programming

来源：评论

学校读者我要写书评

暂无评论

programming microcontrollers through high-level abstractions: The OMicroB project

引用

JOURNAL OF COMPUTER LANGUAGES 2023年 77卷

作者： Varoumas, Steven Pesin, Basile Vaugon, Benoit Chailloux, Emmanuel Huawei Technol Res & Dev UK Ltd Cambridge England Inria Paris France EduSante F-92170 Vanves France Sorbonne Univ LIP6 CNRS F-75005 Paris France

In this paper, we present an approach for programming microcontrollers that provides more expressivity and safety than the low-level language approach traditionally used to program such devices. To this end, we provide various abstraction layers (abstraction of the microcontroller, of the electronic components of the circuit, and of concurrency) which, while being adapted to the scarce resources of the hardware, offer high-level programming traits for the development of embedded applications. The various presented abstractions make use of an OCaml virtual machine, called OMicroB, which is able to run on devices with limited resources. These take advantage of the expressivity and safety of the OCaml language (parameterized modules, advanced type system). Its extensibility allows to define a synchronous extension to manage concurrency while keeping a good level of efficiency at execution. We illustrate the value of our work on both entertainment applications and embedded software examples.

关键词： Microcontrollers Virtual machine High -level programming OCaml Functors synchronous programming

来源：评论

学校读者我要写书评

暂无评论

Model checking of distributed algorithms using synchronous programs ☆

引用

THEORETICAL COMPUTER SCIENCE 2025年 1045卷

作者： Jahier, Erwan Altisen, Karine Devismes, Stephane Sant'Anna, Gabriel B. Univ Grenoble Alpes CNRS Grenoble INP VERIMAG Grenoble France Univ Picardie Jules Verne MIS Amiens France Canonical Sao Paulo Brazil

The development of trustworthy distributed algorithms requires the verification of some key properties with respect to the formal specification of the expected system executions. The atomic-state model (ASM) is the most commonly used computational model to reason on self-stabilizing algorithms. In this work, we propose methods and tools to automatically verify the self-stabilization of distributed algorithms defined in that model. To that goal, we exploit the similarities between the ASM and computational models issued from the synchronous programming area to reuse their associated verification tools, and in particular their model checkers. This allows the automatic verification of all safety properties (including bounded liveness) of any algorithm under various asynchrony assumptions (from fully asynchronous to fully synchronous) and regardless of the hypotheses on the network (e.g., on its topology, its edge and node labeling).

关键词： Self-stabilization synchronous programming Model-checking

来源：评论

学校读者我要写书评

暂无评论

The W-CALCULUS: A synchronous Framework for the Verified Modelling of Digital Signal Processing Algorithms 9

The W-CALCULUS: A Synchronous Framework for the Verified Mod...

引用

9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design (FARM)

作者： Arias, Emilio Jesus Gallego Jouvelot, Pierre Ribstein, Sylvain Desblancs, Dorian Inria Paris Equipe R2 Paris France PSL Univ MINES ParisTech Paris France Ecole Normale Super Paris Saclay Paris France

ISBN: (纸本)9781450386135

We introduce the W-CALCULUS, an extension of the call-by-value lambda-calculus with synchronous semantics, designed to be flexible enough to capture different implementation forms of Digital Signal Processing algorithms, while permitting a direct embedding into the Coq proof assistant for mechanized formal verification. In particular, we are interested in the different implementations of classical DSP algorithms such as audio filters and resonators, and their associated high-level properties such as Linear Time-invariance. We describe the syntax and denotational semantics of the W-CALCULUS, providing a Coq implementation. As a first application of the mechanized semantics, we prove that every program expressed in a restricted syntactic subset of W is linear time-invariant, by means of a characterization of the property using logical relations. This first semantics, while convenient for mechanized reasoning, is still not useful in practice as it requires re-computation of previous steps. To improve on that, we develop an imperative version of the semantics that avoids recomputation of prior stream states. We empirically evaluate the performance of the imperative semantics using a staged interpreter written in OCaml, which, for an input program in W, produces a specialized OCaml program, which is then fed to the optimizing OCaml compiler. The approach provides a convenient path from the high-level semantical description to low-level efficient code.

关键词： Digital Signal Processing programming Language Semantics synchronous programming Formal Verification Linear Time-invariance

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

User-level Threading: Have Your Cake and Eat It Too

引用

PROCEEDINGS OF THE ACM ON MEASUREMENT AND ANALYSIS OF COMPUTING SYSTEMS 2020年第1期4卷 1–30页

作者： Karsten, Martin Barghi, Saman Univ Waterloo Waterloo ON Canada

An important class of computer software, such as network servers, exhibits concurrency through many loosely coupled and potentially long-running communication sessions. For these applications, a long-standing open question is whether thread-per-session programming can deliver comparable performance to event-driven programming. This paper clearly demonstrates, for the first time, that it is possible to employ user-level threading for building thread-per-session applications without compromising functionality, efficiency, performance, or scalability. We present the design and implementation of a general-purpose, yet nimble, user-level M:N threading runtime that is built from scratch to accomplish these objectives. Its key components are efficient and effective load balancing and user-level I/O blocking. While no other runtime exists with comparable characteristics, an important fundamental finding of this work is that building this runtime does not require particularly intricate data structures or algorithms. The runtime is thus a straightforward existence proof for user-level threading without performance compromises and can serve as a reference platform for future research. It is evaluated in comparison to event-driven software, system-level threading, and several other user-level threading runtimes. An experimental evaluation is conducted using benchmark programs, as well as the popular Memcached application. We demonstrate that our user-level runtime outperforms other threading runtimes and enables thread-per-session programming at high levels of concurrency and hardware parallelism without sacrificing performance.

关键词： synchronous programming user-level runtime network server

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Scheduling synchronous Tutoring Sessions in Learning Activities 21st

Scheduling Synchronous Tutoring Sessions in Learning Activit...

引用

21st International Conference on Interactive Collaborative Learning (ICL) / 47th IGIP International Conference on Engineering Pedagogy - Teaching and Learning in a Digital World

作者： Gueye, Amadou Dahirou Faye, Pape Mamadou Djidiack Gueye, Bounama Lishou, Claude Alioune Diop Univ Bambey Senegal Virtual Univ Dakar Senegal Cheikh Anta Diop Univ Dakar Senegal

ISBN: (纸本)9783030119324;9783030119317

This paper deals with a solution allowing digital universities or distance learning structures to extend the functionalities of their distance learning platform to improve not only the management of course session activities but also the organization and synchronous scheduling of these sessions. Indeed, the major problem that is often encountered at the level of distance learning platforms is the management of course hours. This paper proposes a solution for the FOAD Moodle platform to develop a plugin offering teachers the possibility to dynamically choose their course availability and learners the possibility to visualize in real time the week's schedules. The developed plugin is integrated as a new educational resource into the Moodle platform to extend its functionality. This plugin which constitutes the originality of this paper bears the name of Planning.

关键词： Distance learning platform synchronous programming Plugin development Planning

来源：评论

学校读者我要写书评

暂无评论

Towards Secure IoT programming in Haskell 13

Towards Secure IoT Programming in Haskell

引用

13th International Symposium on Haskell (Haskell)

作者： Valliappan, Nachiappan Krook, Robert Russo, Alejandro Claessen, Koen Chalmers Univ Technol Gothenburg Sweden

ISBN: (纸本)9781450380508

IoT applications are often developed in programming languages with low-level abstractions, where a seemingly innocent mistake might lead to severe security vulnerabilities. Current IoT development tools make it hard to identify these vulnerabilities as they do not provide end-to-end guarantees about how data flows within and between appliances. In this work we present Haski, an embedded domain specific language (eDSL) in Haskell for secure programming of IoT devices. Haski enables developers to write Haskell programs that generate C code without falling into many of C's pitfalls. Haski is designed after the synchronous programming language Lustre, and sports a backwards compatible information-flow control extension to restrict how sensitive data is propagated and modified within the application. We present a novel eDSL design which uses recursive monadic bindings and allows a natural use of functions and pattern matching to write embedded programs. To showcase Haski, we implement a simple smart house controller where communication is done via low-energy Bluetooth on the Zephyr IoT OS.

关键词： synchronous programming Information-flow Control eDSL IoT Haskell

来源：评论

学校读者我要写书评

暂无评论

Synchronized Shared Memory and Procedural Abstraction: Towards a Formal Semantics of Blech

Synchronized Shared Memory and Procedural Abstraction: Towar...

引用

Forum for Specification and Design Languages (FDL)

作者： Gretz, F. Grosch, F-J Mendler, M. Scheele, S. Bosch Corp Res Palo Alto CA 94304 USA Bamberg Univ Bamberg Germany

ISBN: (纸本)9781728189284

Traditional imperative synchronous programming languages heavily rely on a strict separation between data memory and communication signals. Signals can be shared between computational units but cannot be overwritten within a synchronous reaction cycle. Memory can be destructively updated but cannot be shared between concurrent threads. This incoherence makes traditional imperative synchronous languages cumbersome for the programmer. The recent definition of sequentially constructive synchronous languages offers an improvement. It removes the separation between data memory and communication signals and unifies both through the notion of clock synchronised shared memory. However, it still depends on global causality analyses which precludes procedural abstraction. This complicates reuse and composition of software components. This paper shows how procedural abstraction can be accommodated inside the sequentially constructive model of computation. We present the Sequentially Constructive Procedural Language (SCPL) and its semantic theory of policy-constructive synchronous processes. SCPL supports procedural abstractions using policy interfaces to ensure that procedure calls are memory safe, wait-free and their scheduling is determinate and causal. At the same time, a policy interface constrains the level of freedom for the implementation and subsequent refactoring of a procedure. As a result, policies enable separate compilation and composition of procedures. We present our extensions abstractly as a formal semantics for SCPL and motivate it concretely in the context of the open-source, embedded, real-time language Blech.

关键词： synchronous programming clock-synchronised shared memory procedural abstraction operational semantics

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：