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

27th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2018

作者： Mikulcak, Marcus Herber, Paula Gothel, Thomas Glesner, Sabine Software and Embedded Systems Engineering Group Technische Universitat Berlin Germany

ISBN: (纸本)9781538669167

Simulink and Stateflow are widely-used industrial tools for the development of embedded systems, e.g. in the automotive domain. In modern automotive control systems, multiple components are typically interconnected, and, nowadays, also have a connection to the internet. This poses severe threats, as safety-critical components may be subject to remote attacks, which divert control or information flow from non-critical to safety-critical components. In this paper, we present a novel approach for the analysis of information flow in combined Simulink/Stateflow models. The key idea of our approach is that we analyze the information flow in a given model by computing an over-approximation of the control flow and deduce whether all control flow conditions on a given path combined permit information flow or not. With our approach, we safely rule out the existence of information flow on specific paths. Thus, it enables us to reason about non-interference and the compliance with security policies. © 2018 IEEE.

关键词： Simulink

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Optimized Hardware/software Co-Verification using the UCLID Satisfiability Modulo Theory Solver 29

Optimized Hardware/Software Co-Verification using the UCLID ...

引用

29th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2020

作者： Schwan, Simon Herber, Paula Technische Universität Berlin Software and Embedded Systems Engineering Group Berlin Germany University of Münster Embedded Systems Group Münster Germany

ISBN: (纸本)9781728169750

embedded systems are often used in safety-critical applications like cars or airplanes. This makes it crucial to verify their hardware and software under all circumstances. In previous work, we have presented an approach for the formal verification of integrated hardware/software systems using the satisfiability modulo theory solving based verification system UCLID. However, the transformation of integrated hardware/software systems into the input language of the UCLID verification system causes a considerable overhead in the number of symbolic simulation steps necessary for k-inductive verification. In this paper, we overcome this problem by presenting two optimizations for the symbolic simulation of cooperatively scheduled concurrent processes: First, we realize a reduction of redundant states in individual functions that respects all data, control and inter-process dependencies. To capture these dependencies precisely, we present the novel concept of a cooperative dominator tree, which extends the classical concept of a dominator tree to cooperatively scheduled concurrent processes. Second, we present a process parallelization for cooperatively scheduled concurrent processes based on a SystemC dependence graph. In our evaluation based on a set of 21 synthetic case studies, we reach an average reduction of the inductive verification times by 40 %. © 2020 IEEE.

关键词： Formal verification

来源：评论

学校读者我要写书评

暂无评论

The organic computing doctoral dissertation colloquium: Status and overview in 2019 49

The organic computing doctoral dissertation colloquium: Stat...

引用

49. Jahrestagung der Gesellschaft fur Informatik: 50 Jahre Gesellschaft fur Informatik - Informatik fur Gesellschaft, INFORMATIK 2019 - 49th Annual Meeting of the German Informatics Society: 50 years of the German Informatics Society - Computer Science for Society, INFORMATICS 2019

作者： Krupitzer, Christian Tomforde, Sven Software Engineering Group Universitat Wurzburg Germany Intelligent Embedded Systems Universitat Kassel Germany

ISBN: (纸本)9783885796893

Today, people are surrounded by smart and connected devices. Gartner Inc. estimated that 8.4 billion devices were connected in the Internet-of-Things worldwide in 2017, reaching 20.4 billion by 2020. The growing number of mobile and embedded devices in combination with the omnipresence of (wireless) network connections facilitates new applications, such as autonomous driving, ambient assisted living/smart home, or Industry 4.0. However, it requires integration of all available, highly specialised, and heterogeneous devices, ranging from embedded sensor nodes to servers in the cloud. Further, the inclusion of data streams with sensor data and web data leads to an increasing complexity in system development. Additionally, as these systems are mobile, changing environmental conditions increase the complexity even further. Organic Computing systems are able to deal with such systems and lower the complexity for their development by introducing methods for integrating adaptiveness and intelligence to computing systems. This workshops brings together PhD students from different research streams related to Organic Computing with the objective to represent the wide Aeld of research in the domain of adaptive and intelligence systems. © 2019 Gesellschaft fur Informatik (GI). All rights reserved.

关键词： Sensor nodes

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Type systems for domain-specific languages

Type systems for domain-specific languages

引用

Multi-Conference on software engineering, SE 2013

作者： Jung, Reiner Schneider, Christian Hasselbring, Wilhelm Software Engineering Research Group Kiel University Germany Embedded and Realtime Systems Research Group Kiel University Germany

ISBN: (纸本)9783885796091

Model-driven software development employs models to describe different aspects of a system on different levels of abstraction. These aspects are driven by technology or application domain. Modeling is often done in specific graphical or textual notations, called domain-specific languages (DSL). In recent years such languages became very popular in the modeling community to describe structure and sometimes behavior. In the context of type systems, these structures are called types and the behavior is modeled with expressions. The programming language community has developed many concepts to model and specify type systems and the semantics of expressions. However, in the modeling community this is often neglected when specifying meta models and describing their semantics, what may cause problems in developing checks and generators for DSLs. To address this issue, we present an approach, that provides guidance and support during DSL development based on established knowledge on type systems and generator construction, to ease the integration of type systems in DSL. We evaluate this approach with the Xtext language engineering framework. © Gesellschaft für Informatik, Bonn 2013.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Scalable multi-core simulation using parallel dynamic binary translation

Scalable multi-core simulation using parallel dynamic binary...

引用

2011 11th International Conference on embedded Computer systems: Architectures, Modeling and Simulation, IC-SAMOS 2011

作者： Almer, Oscar Böhm, Igor Von Koch, Tobias Edler Franke, Björn Kyle, Stephen Seeker, Volker Thompson, Christopher Topham, Nigel Institute for Computing Systems Architecture University of Edinburgh United Kingdom Software Engineering for Embedded Systems Group Technical University Berlin Germany

ISBN: (纸本)9781457708008

In recent years multi-core processors have seen broad adoption in application domains ranging from embedded systems through general-purpose computing to large-scale data centres. Simulation technology for multi-core systems, however, lags behind and does not provide the simulation speed required to effectively support design space exploration and parallel software development. While state-of-the-art instruction set simulators (Iss) for single-core machines reach or exceed the performance levels of speed-optimised silicon implementations of embedded processors, the same does not hold for multi-core simulators where large performance penalties are to be paid. In this paper we develop a fast and scalable simulation methodology for multi-core platforms based on parallel and just-in-time (Jit) dynamic binary translation (Dbt). Our approach can model large-scale multi-core configurations, does not rely on prior profiling, instrumentation, or compilation, and works for all binaries targeting a state-of-the-art embedded multi-core platform implementing the ARCompact instruction set architecture (Isa). We have evaluated our parallel simulation methodology against the industry standard Splash-2 and Eembc MultiBench benchmarks and demonstrate simulation speeds up to 25,307 Mips on a 32-core 86 host machine for as many as 2048 target processors whilst exhibiting minimal and near constant overhead. © 2011 IEEE.

关键词： embedded systems

来源：评论

学校读者我要写书评

暂无评论

VOICE OF EVIDENCE Organizational Culture and Success in SPI Initiatives

引用

IEEE software 2012年第3期29卷 97-99页

作者： Passos, Odette Mestrinho Dias-Neto, Arilo Claudio Barreto, Raimundo da Silva Institute of Exact Sciences and Technology Federal University of Amazonas Brazil Institute of Computing Experimentation and Testing on Software Engineering Group Federal University of Amazonas Brazil Institute of Computing complex embedded systems research group Federal University of Amazonas Brazil

To succeed, a software quality improvement (SQI) initiative must reflect organizational culture and the values that compose it. A study to define these values in software organizations includes proposals for implement... 详细信息

关键词： software Quality software Process Improvement

来源：评论

学校读者我要写书评

暂无评论

Static analysis of run-time modes in synchronous process network

Static analysis of run-time modes in synchronous process net...

引用

8th International Ershov Informatics Conference on Perspectives of System Informatics, PSI 2011

作者： Beyer, Michael Glesner, Sabine Software Engineering for Embedded Systems Group Technische Universität Berlin Ernst-Reuter-Platz 7 Berlin 10587 Germany

ISBN: (纸本)9783642297083

For modeling modern streaming-oriented applications, Process Networks (PNs) are used to describe systems with changing behavior, which must be mapped on a concurrent architecture to meet the performance and energy constraints of embedded devices. Finding an optimal mapping of Process Networks to the constrained architecture presumes that the behavior of the Process Network is statically known. In this paper we present a static analysis for synchronous PNs that extracts different run-time modes by using polyhedral abstraction. The result is a Mealy machine whose states describe different run-time modes and the edges among them represent transitions. This machine can be used to guide optimizing backend mappings from PNs to concurrent architectures. © 2012 Springer-Verlag Berlin Heidelberg.

关键词： Static analysis

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：