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

international conference on Reconfigurable Computing and FPGAs (ReConFig)

作者： Streit, Franz-Josef Letras, Martin Wildermann, Stefan Hackenberg, Benjamin Falk, Joachim Becher, Andreas Teich, Juergen Friedrich Alexander Univ Erlangen Nurnberg FAU Dept Comp Sci 12 Erlangen Germany

ISBN: (纸本)9781728119687

Shorter design cycles in FPGA-based Programmable system-on-Chips (PSoCs) development require a higher level of design automation, which has led to a wide acceptance of model driven engineering. However, design and implementation of applications on such heterogeneous PSoC platforms still demand a comprehensive expertise in hardware/software co-design. Therefore, to keep up with this trend, an automated systematic design flow that couples model-based design and simulation with High-Level synthesis (HLS) for hybrid hardware and software implementations is necessary. In order to address this issue, the work at hand makes use of the modeling and simulation environment MATLAB/Simulink, a de facto standard in model-based development. Additionally, we present a novel design flow which automatically synthesizes individual hardware/software solutions for Xilinx Zynq PSoCs based on a manual partitioning of blocks. Thereby, the proposed methodology enables control and system engineers to automatically explore different hardware and software implementation variants from a behavioral model. As a case study, we present a JPEG decoder application and investigate design objectives like resource costs and throughput to show the practicability of our approach.

关键词： FPGA SoC hardware/software Co-Design Model-Based Engineering

来源：评论

学校读者我要写书评

暂无评论

UCLID5: Integrating Modeling, Verification, synthesis and Learning 18

UCLID5: Integrating Modeling, Verification, Synthesis and Le...

引用

16th ACM/IEEE international conference on Formal Methods and Models for system Design (MEMOCODE)

作者： Seshia, Sanjit A. Subramanyan, Pramod Univ Calif Berkeley Dept EECS Berkeley CA 94720 USA Indian Inst Technol CSE Dept Kanpur Uttar Pradesh India

ISBN: (纸本)9781538661956

Formal methods for system design are facing a confluence of transformative trends. First, systems are increasingly heterogeneous, comprising some combination of hardware, software, networking, and physical processes. Second, these systems are increasingly being designed with data-driven methods, in addition to traditional model-based design techniques. Third, traditional automated reasoning techniques based on deduction are being combined with new techniques for inductive inference and machine learning. In this paper, we present UCLID5, a new system for formal modeling, verification, and synthesis that addresses the challenges and opportunities arising from this confluence. UCLID5 can model heterogeneous computational systems, provides term-level abstraction supported by satisfiability modulo theories (SMT) solvers, enables compositional reasoning, and implements the paradigm of verification by reduction to synthesis, leveraging the advances in algorithmic synthesis and machine learning. We describe the key features of UCLID5 using illustrative examples.

关键词： Formal methods machine learning specification verification synthesis hardware software cyber-physical systems security

来源：评论

学校读者我要写书评

暂无评论

Facilitating Model-Based Control Through software-hardware Co-Design

Facilitating Model-Based Control Through Software-Hardware C...

引用

2018 IEEE international conference on Robotics and Automation, ICRA 2018

作者： Ramos, Joao Katz, Benjamin Chuah, Meng Yee Michael Kim, Sangbae Department of Mechanical Engineering Massachusetts Institute of Technology CambridgeMA United States

ISBN: (纸本)9781538630815

This paper exemplifies the design process for legged machines capable of dynamic behaviors. In order to achieve high performance robots, it is crucial to guarantee harmonious integration between software and hardware. Hence, the development of such capable robotic platforms must address design requirements that meet the assumptions of typical model-based controllers but also respect the physical limitations of a real system. First, we show that proper hardware design choices can greatly aid the control algorithm by approximating the physical robot to the template assumptions. We include actuation and sensing design examples that allows a simple model to capture a major portion of the natural dynamic behavior of the physical machine. Results are applied to a real robot (Figure 1) and we show that the adopted methodology is able to address typical problems in legged robots such as high bandwidth force control and robustness to impact. Finally, a simple model-based balance controller that takes advantage of the fidelity of the template model to the real machine is implemented. These are examples of software-hardware codesign processes that vastly facilitate robotic control. © 2018 IEEE.

关键词： Robots

来源：评论

学校读者我要写书评

暂无评论

Will My Program Break on This Faulty Processor?: Formal Analysis of hardware Fault Activations in Concurrent Embedded software

引用

ACM TRANSACTIONS ON EMBEDDED COMPUTING systemS 2019年第5期18卷 89-89页

作者： Bajczi, Levente Voros, Andras Molnar, Vince Budapest Univ Technol & Econ Fault Tolerant Syst Res Grp Dept Measurement & Informat Syst POB 91 H-1521 Budapest Hungary MTA BME Lendulet Cyber Phys Syst Res Grp Budapest Hungary

Formal verification is approaching a point where it will be reliably applicable to embedded software. Even though formal verification can efficiently analyze multi-threaded applications, multi-core processors are often considered too dangerous to use in critical systems, despite the many benefits they can offer. One reason is the advanced memory consistency model of such CPUs. Nowadays, most software verifiers assume strict sequential consistency, which is also the naive view of programmers. Modernmulti-core processors, however, rarely guarantee this assumption by default. In addition, complex processor architectures may easily contain design faults. Thanks to the recent advances in hardware verification, these faults are increasingly visible and can be detected even in existing processors, giving an opportunity to compensate for the problem in software. In this paper, we propose a generic approach to consider inconsistent behavior of the hardware in the analysis of software. Our approach is based on formal methods and can be used to detect the activation of existing hardware faults on the application level and facilitate their mitigation in software. The approach relies heavily on recent results of model checking and hardware verification and offers new, integrative research directions. We propose a partial solution based on existing model checking tools to demonstrate feasibility and evaluate their performance in this context.

关键词： Fault analysis memory consistency model concurrent litmus test

来源：评论

学校读者我要写书评

暂无评论

ICCAD-2005 international conference on Computer Aided Design (IEEE Cat. No. 05CH37700) 05

ICCAD-2005 International Conference on Computer Aided Design...

引用

proceedings of the 2005 IEEE/ACM international conference on Computer-aided design

ISBN: (纸本)9780780392540

The following topics are dealt with: memory and arithmetic optimization; design manufacturing interaction; circuit layout; digital analog and RF test; design for manufacturing; logic synthesis; double-gated devices; network routing and application specific NoC architectures; memory driven codes; arithmetic constructs; buffers and voltage islands; sequential circuit optimization; nanoelectronics; dynamic voltage scaling; biochips and DNA-based nanofabrication; circuit simulation; analog circuit design; power aware system architecture; software optimization; cellular array architectures; variability aware clocking; oscillator analysis; power noise and thermal issues; nanocomputing; extraction and modeling for interconnect structures; system-level variability modeling; high-level synthesis; model order reduction; statistical timing analysis; formal verification; hardware and software design of sensors; formal equivalence checking and system on chip.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Compositional Design of Multi-Robot systems Control software on ROS

引用

ACM TRANSACTIONS ON EMBEDDED COMPUTING systemS 2019年第5期18卷 71-71页

作者： Spellini, Stefano Lora, Michele Fummi, Franco Chattopadhyay, Sudipta Univ Verona Dept Comp Sci Str Grazie 15 I-37134 Verona Italy Singapore Univ Technol & Design ISTD 8 Somapah Rd Singapore 487372 Singapore

This paper presents a methodology that relies on Assume-Guarantee Contracts to decompose the problem of synthesizing control software for a multi-robot system. Initially, each contract describes either a component (e.g., a robot) or an aspect of the system. Then, the design problem is decomposed into different synthesis and verification sub-problems, allowing to tackle the complexity involved in the design process. The design problem is then recomposed by exploiting the rigorousness provided by contracts. This allows us to achieve system-level simulation capable to be used for validating the entire design. Once validated, the software synthesized during the process can be integrated into Robot Operating system (ROS) nodes and executed using state-of-the-practice packages and tools for modern robotic systems. We apply the methodology to generate a control strategy for an autonomous goods transportation system. Our results show a massive reduction of the time required to obtain automatically the control software implementing a multi-robot mission.

关键词： Contract-based design robotic operating system

来源：评论

学校读者我要写书评

暂无评论

Treble: Fast software Updates by Creating an Equilibrium in an Active software Ecosystem of Globally Distributed Stakeholders

引用

ACM TRANSACTIONS ON EMBEDDED COMPUTING systemS 2019年第5期18卷 104-104页

作者： Yim, Keun Soo Malchev, Iliyan Hsieh, Andrew Burke, Dave Google 1600 Amphitheatre Pkwy Mountain View CA 94043 USA

This paper presents our experience with Treble, a two-year initiative to build the modular base in Android, a Java-based mobile platform running on the Linux kernel. Our Treble architecture splits the hardware independent core framework written in Java from the hardware dependent vendor implementations (e.g., user space device drivers, vendor native libraries, and kernel written in C/C++). Cross-layer communications between them are done via versioned, stable inter-process communication interfaces whose backward compatibility is tested by using two API compliance suites. Based on this architecture, we repackage the key Android software components that suffered from crucial post-launch security bugs as separate images. That not only enables separate ownerships but also independent updates of each image by interested ecosystem entities. We discuss our experience of delivering Treble architectural changes to silicon vendors and device makers using a yearly release model. Our experiments and industry rollouts support our hypothesis that giving more freedom to all ecosystem entities and creating an equilibrium are a transformation necessary to further scale the world largest open source ecosystem with over two billion active devices.

关键词： Open source ecosystem software architecture software update

来源：评论

学校读者我要写书评

暂无评论

Work-in-Progress: Runtime Requirements Monitoring for State-based hardware

Work-in-Progress: Runtime Requirements Monitoring for State-...

引用

international conference on hardware/software codesign and system synthesis (CODES)

作者： Minjun Seo Roman Lysecky Department of Electrical and Computer Engineering University of Arizona Tucson AZ USA

This paper presents a requirements-driven methodology enabling efficient runtime monitoring of hardware in embedded systems. We present a novel method for extracting hardware verification requirements from state-based hardware models to construct a hierarchical runtime monitoring graph (HRMG) that can be efficiently used at runtime to verify correctness.

关键词： Monitoring hardware Runtime Embedded systems Timing Unified modeling language

来源：评论

学校读者我要写书评

暂无评论

Cache Locking Content Selection Algorithms for ARINC-653 Compliant RTOS

引用

ACM TRANSACTIONS ON EMBEDDED COMPUTING systemS 2019年第5期18卷 76-76页

作者： Dugo, Alexy Torres Aurora Lefoul, Jean-Baptiste De Magalhaes, Felipe Gohring Assal, Dahman Nicolescu, Gabriela Ecole Polytech Montreal 2900 Boul Edouard Montpetit Montreal PQ Canada Mannarino Syst & Software Inc Montreal PQ Canada

Avionic software is the subject of stringent real time, determinism and safety constraints. software designers face several challenges, one of them being the interferences that appear in common situations, such as resource sharing. The interferences introduce non-determinism and delays in execution time. One of the main interference prone resources are cache memories. In single-core processors, caches comprise multiple private levels. This breaks the isolation principle imposed by avionic standards, such as the ARINC-653. This standard defines partitioned architectures where one partition should never directly interfere with another one. In cache-based architectures, one partition can modify the cache content of another partition. In this paper, we propose a method based on cache locking to reduce the non-determinism and the contention on lower level memories while improving the time performances.

关键词： Critical systems ARINC-653 interference cache locking aerospace

来源：评论

学校读者我要写书评

暂无评论

Exploration of hardware topologies based on functions, variability and timing 18

Exploration of hardware topologies based on functions, varia...

引用

21st ACM/IEEE international conference on Model Driven Engineering Languages and systems (MODELS)

作者： Eder, Johannes Fortiss GmbH Munich Bavaria Germany

ISBN: (纸本)9781450359658

This paper gives an overview over a dissertation project in the area of design space exploration for distributed, embedded systems. As the engineering of distributed embedded systems is getting more and more complex due to increasingly sophisticated functionalities demanding more and more powerful hardware, automation is required in order cope with this rising complexity. Using a model based systems engineering approach enables design space exploration methods which provide such automations, given a formalization of the problem in order to be solvable e.g. by SMT solvers. In this thesis we want to provide an automated synthesis of hardware topologies (E/E architectures) based on the functions which are deployed onto this topology and constraints and optimization objectives which are derived from the requirements of the system. The synthesis shall consider variability aspects (possible variants) of the hardware elements. Additionally, timing aspects of the deployed shall be regarded such that the solution of the synthesis is a hardware topology, a deployment of functions onto this topology and a schedule of these functions. The thesis shall be evaluated by using an automotive industrial use case of realistic size.

关键词： Automation

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：