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

Hardware support for efficient testing of embedded software

Hardware support for efficient testing of embedded software

ASME 2011 International Design engineering Technical Conferences and Computers and Information in engineering Conference, IDETC/CIE 2011

作者： Reinbacher, Thomas Müller, Tobias Horauer, Martin Brauer, Jörg Kowalewski, Stefan Andreas Steininger ECS Group Inst. of Computer Engineering Vienna University of Technology Treitlstr. 3 1040 Vienna Austria Dept. of Embedded Systems Univ. of Applied Sciences Technikum Wien Hochstadtpl. 5 1200 Vienna Austria Embedded Software Laboratory RWTH Aachen University Ahornstr. 55 52074 Aachen Germany

ISBN: (纸本)9780791854808

Verification of software for embedded systems is crucial for ensuring a product's integrity. Formal approaches like static analysis and model checking are gaining momentum in this context. To make an exhaustive examination of the system's state space tractable in practice, these methods perform an abstraction and over-approximation of the possible behavior. As a side-effect, however, this leads to "false negatives" - property violations that exist only in the model and not on the real system. Ruling out such spurious property violations by manual valuation is a tedious and error-prone process. This paper reports on the concepts and design of a hardware unit to support the identification of false negatives. Our approach has several advantages: (i) It works on microcontroller binary code, thus avoiding the need for availability of high-level source code, and covering compiler bugs as well. (ii) Moving the verification directly to the target platform rules out modeling errors. (iii) The cases suspected to lead to spurious property violations can serve as very efficient test cases for a specific implementation later on. We illustrate principle and benefits of the proposed approach by a worked example. © 2011 by ASME.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

Intelligent task mapping using machine learning

Intelligent task mapping using machine learning

引用

International Conference on Computational Intelligence and software engineering

作者： Tetzlaff, Dirk Glesner, Sabine Group Software Engineering for Embedded Systems Berlin Institute of Technology Germany

ISBN: (纸本)9781424453924

Task scheduling and task allocation, which are vital parts of mapping parallel programs to concurrent architectures, must take into account the interprocessor communication, whose overheads have emerged as the major performance limitation in parallel applications. Furthermore, its power consumption is an important research focus which must be addressed. Finding an optimal solution requires information about the runtime behavior, which is not known at compile time. Moreover, the computational complexity leads to heuristic approaches based on conservative assumptions that are unable to exploit all of the program's optimization potential. In this paper, we propose a novel approach to automatically generate architecture- and application-specific heuristics for power- and communication-aware task mapping using machine learning techniques to predict how programs behave at runtime. The key advantage of machine learning techniques is their ability to find relevant information in a high-dimensional space. This yields more precise heuristics than those based on pure static assumptions, as our experimental results show. Because learning is done in an off-line training phase once per architecture, the compile time itself is not extended as in other heuristic approaches like genetic or evolutionary algorithms. ©2010 IEEE.

关键词： Heuristic methods

来源：评论

学校读者我要写书评

暂无评论

Specification, verification and implementation of business processes using CSP

Specification, verification and implementation of business p...

引用

2010 4th International Symposium on Theoretical Aspects of software engineering, TASE 2010

作者： Kleine, Moritz Göthel, Thomas Technische Universität Berlin Software Engineering Group Germany Technische Universität Berlin Software Engineering for Embedded Systems Germany

ISBN: (纸本)9780769541488

Nowadays, the problem in business process management (BPM) is that BPM systems should both be easy to use for business process developers and be based on a sound formal method. Business process management systems are often based on semiformal modeling techniques such as event-driven process chains (EPC) or UML. Unlike semiformal modeling techniques, the process calculus CSP comes with mature verification support. Surprisingly little work has been done on using CSP for business process modeling and management. In this paper, we present our approach to business process management, which is based on the observation that CSP is well suited not only for specifying business processes and verifying workflows but also for executing workflows using our CSP4J framework. We report on a workflow server, which is specified in CSP and implemented using our CSP4J framework. The server accepts workflows that are modeled in CSP and also implemented using CSP4J. This allows us to integrate the mature verification support of CSP into both the management system itself and the development process of the end users' business process definitions. © 2010 IEEE.

关键词： Calculations

来源：评论

学校读者我要写书评

暂无评论

Proving consistency of VDM models using HOL 10

Proving consistency of VDM models using HOL

引用

25th Annual ACM Symposium on Applied Computing, SAC 2010

作者： Vermolen, Sander D. Hooman, Jozef Larsen, Peter Gorm Software Engineering Research Group Delft University of Technology Delft Netherlands Embedded Systems Institute Radboud University Nijmegen Netherlands Engineering College of Aarhus Dalgas Avenue 2 Aarhus Denmark

ISBN: (纸本)9781605586380

Although consistency of formal models is crucial, consistency proofs should not be a large burden to the user. Hence, it is important to have access to efficient proof support which is able to automate a large part of the consistency proofs. We have developed a tool that automatically translates a large subset of VDM and its associated proof obligations, which ensure model consistency, to the theorem prover HOL. In addition, powerful tactics have been constructed to discard most of the proof obligations automatically. The application of our approach to four case studies shows that a high degree of automation can be achieved. © 2010 ACM.

关键词： Theorem proving

来源：评论

学校读者我要写书评

暂无评论

Intelligent Task Mapping Using Machine Learning

Intelligent Task Mapping Using Machine Learning

引用

International Conference on Computational Intelligence and software engineering (CiSE)

作者： Dirk Tetzlaff Sabine Glesner Group Software Engineering of Embedded Systems Berlin Institute of Technology Germany

关键词： Runtime Machine learning Heuristic algorithms Computer architecture Training Processor scheduling Resource management

来源：评论

学校读者我要写书评

暂无评论

Specification, Verification and Implementation of Business Processes Using CSP

Specification, Verification and Implementation of Business P...

引用

Theoretical Aspects of software engineering (TASE)

作者： Moritz Kleine Thomas Göthel Software Engineering Group Technische Universität Berlin Germany Software Engineering for Embedded Systems Technische Universität Berlin Germany

关键词： Business Unified modeling language Petri nets Semantics Process control Servers Synchronization

来源：评论

学校读者我要写书评

暂无评论

Virtual integration of model-based functions under autosar

引用

AutoTechnology 2010年第1期10卷 46-50页

作者： Michailidis, Alexander Ringler, Thomas Hedenetz, Bernd Kowalewski, Stefan Department of E/E Architectures and Standards Group Research and Advanced Engineering Division Daimler AG Böblingen Germany Team E/E System Design and Applications Group Research and Advanced Engineering Division Daimler AG Böblingen Germany Software for Embedded Systems RWTH Aachen University Germany

The functionality of comfort and interior systems such as interior light, seat heating, central locking is typically distributed on several Electronic Control Units (ECU). These systems very often consist of a central main function and many other smaller so-called client functions. The system or rather the ECU integration and thus the examination of the interplay of the functions with one another or with the hardware specific software is carried out in the right branch of the V-model according to the availability of the real ECUs. The construction of such models was up to now not practical due to the inconsistent ECU software architectures at the different suppliers. With the extensive adoption of the standardized Autosar software architecture and a consistent function-oriented Autosar SWC description, the design of virtual integration models in the earlier stages of development is for the first time possible with a reasonable effort.

关键词： software architecture

来源：评论

学校读者我要写书评

暂无评论

Model checking SystemC designs using timed automata 08

Model checking SystemC designs using timed automata

引用

embedded systems Week 2008 - 6th IEEE/ACM/IFIP International Conference on Hardware/software Codesign and System Synthesis, CODES+ISSS 2008

作者： Herber, Paula Fellmuth, Joachim Glesner, Sabine Software Engineering for Embedded Systems Group Technical University of Berlin Germany

ISBN: (纸本)9781605584706

SystemC is widely used for modeling and simulation in hardware/software co-design. Due to the lack of a complete formal semantics, it is not possible to verify SystemC designs. In this paper, we present an approach to overcome this problem by defining the semantics of SystemC by a mapping from SystemC designs into the well-defined semantics of UPPAAL timed automata. The informally defined behavior and the structure of SystemC designs are completely preserved in the generated UPPAAL models. The resulting UPPAAL models allow us to use the UPPAAL model checker and the UPPAAL tool suite, including simulation and visualization tools. The model checker can be used to verify important properties such as liveness, deadlock freedom or compliance with timing constraints. We have implemented the presented transformation, applied it to two examples and verified liveness, safety and timing properties by model checking, thus showing the applicability of our approach in practice. Copyright 2008 ACM.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

A low-power multithreaded processor for software defined radio

A low-power multithreaded processor for software defined rad...

引用

作者： Schulte, Michael Glossner, John Jinturkar, Sanjay Moudgill, Mayan Mamidi, Suman Vassiliadis, Stamatis University of Wisconsin Dept. of ECE 1415 Engineering Drive Madison WI 53706 United States Sandbridge Technologies 1 North Lexington Ave. White Plains NY 10512 United States Delft University of Technology Electrical Engineering Mathematics and Computer Science Department Delft Netherlands University of Wisconsin Madison Madison Embedded Systems and Architectures Group IEEE IEEE Computer Society Sandbridge Technologies Sandbridge Systems Software and Communications Software Groups Department of Electrical and Computer Engineering University OfWisconsin Madison Netherlands ACM

embedded digital signal processors for software defined radio have stringent design constraints including high computational bandwidth, low power consumption, and low interrupt latency. Furthermore, due to rapidly evolving communication standards with increasing code complexity, these processors must be compiler-friendly, so that code for them can quickly be developed in a high-level language. In this paper, we present the design of the Sandblaster Processor, a low-power multithreaded digital signal processor for software defined radio. The processor uses a unique combination of token triggered threading, powerful compound instructions, and SIMD vector operations to provide real-time baseband processing capabilities with very low power consumption. We describe the processor's architecture and microarchitecture, along with various techniques for achieving high performance and low power dissipation. We also describe the processor's programming environment and the SB3010 platform, a complete system-on-chip solution for software defined radio. Using a super-computer class vectorizing compiler, the SB3010 achieves real-time performance in software on a variety of communication protocols including 802.11b, GPS, AM/FM radio, Bluetooth, GPRS, and WCDMA. In addition to providing a programmable platform for SDR, the processor also provides efficient support for a wide variety of digital signal processing and multimedia applications. © 2006 Springer Science + Business Media, LLC.

关键词： Program processors

来源：评论

学校读者我要写书评

暂无评论

Providing means for precision airdrop delivery from high altitude

Providing means for precision airdrop delivery from high alt...

引用

AIAA Guidance, Navigation, and Control Conference 2006

作者： Hattis, Philip D. Campbell, Darryn P. Carter, David W. McConley, Marc Tavan, Steve Draper Laboratory Cambridge MA 02139 United States US Army Research Development and Engineering Command Natick Soldier Center Natick MA 01760 United States Mission Design and Analysis Group 555 Technology Square Mail Stop 77 AIAA United States Embedded Software Group 555 Technology Square Mail Stop 77 Decision Systems Group 555 Technology Sauare Mail Stop 77 United States Tactics Guidance and Control Group 555 Technology Square Mail Stop 77 Precision Airdrop GN and C Research NSC Airdrop Aerial Delivery Directorate AMSRD-NSC-AD-JP Kansas Street United States

ISBN: (纸本)1563478196

Precision airdrop is essential to insertion of military and humanitarian supplies at remote, globally distributed locations that are involved in conflict or have experienced natural disasters. Enabling precision payload delivery following high altitude release limits risk to carrier aircraft For the past eight years, the Army and Air Force have combined resources to facilitate major advances in precision, high altitude airdrop. This includes new means for on-board airdrop mission planning for an expanding set of ballistic parachute and guided parafoil airdrop systems that realize accuracy improvement by using detailed system dynamics models, high fidelity atmospheric state models, and means to generate and upload revised mission plans for guided airdrop systems. Development and implementation of an open-architecture Guidance, Navigation, and Control (GN&C) system has also been pursued for use on large parafoil airdrop systems. Implementation features of the personal computer-based Precision Airdrop System (PADS) mission planner are reviewed and the parafoil GN&C design features are discussed. A review is provided of payload delivery performance realized using the PADS for a variety of ballistic and guided airdrop systems and using the GN&C system on the Dragonfly 10,000-lb class parafoil. Continued capability development plans for PADS and the GN&C system are also summarized. Copyright © 2006 by the Charles Stark Draper Laboratory, Inc.

关键词： Electronic guidance systems

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：