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

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

来源：评论

学校读者我要写书评

暂无评论

Organic computing doctoral dissertation colloquium 2019

Lecture Notes in Informatics (LNI), Proceedings - Series of ...

引用

Lecture Notes in Informatics (LNI), Proceedings - Series of the Gesellschaft fur Informatik (GI) 2019年 295卷 467-467页

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

来源：评论

学校读者我要写书评

暂无评论

Information flow analysis of combined simulink/stateflow models 27

Information flow analysis of combined simulink/stateflow mod...

引用

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

来源：评论

学校读者我要写书评

暂无评论

Towards Self-Explainable Cyber-Physical systems

Towards Self-Explainable Cyber-Physical Systems

引用

ACM/IEEE International Conference on Model Driven engineering Languages and systems Companion

作者： Mathias Blumreiter Joel Greenyer Francisco Javier Chiyah Garcia Verena Klos Maike Schwammberger Christoph Sommer Andreas Vogelsang Andreas Wortmann Institute for Software Systems Hamburg University of Technology Software Engineering Group Leibniz Universitat Hannover Heriot-Watt University Software and Embedded Systems Engineering Technische Universitat Berlin Department of Computing Science University of Oldenburg Heinz Nixdorf Institute and Dept. of Computer Science Paderborn University Automated Systems Engineering Technologies Technische Universitat Berlin Software Engineering RWTH Aachen University

ISBN: (纸本)9781728151267

With the increasing complexity of Cyber-Physical systems, their behavior and decisions become increasingly difficult to understand and comprehend for users and other stakeholders. Our vision is to build self-explainable systems that can, at run-time, answer questions about the system's past, current, and future behavior. As hitherto no design methodology or reference framework exists for building such systems, we propose the Monitor, Analyze, Build, Explain (MAB-EX) framework for building self-explainable systems that leverage requirements- and explainability models at run-time. The basic idea of MAB-EX is to first Monitor and Analyze a certain behavior of a system, then Build an explanation from explanation models and convey this EXplanation in a suitable way to a stakeholder. We also take into account that new explanations can be learned, by updating the explanation models, should new and yet un-explainable behavior be detected by the system.

关键词： Explainability Self-adaptive systems Cyber-physical systems Adaptive systems Cyber-physical systems MONITOR Runtime Buildings

来源：评论

学校读者我要写书评

暂无评论

Towards self-explainable cyber-physical systems

arXiv

引用

arXiv 2019年

作者： Blumreiter, Mathias Greenyer, Joel Garcia, Francisco Javier Chiyah Klös, Verena Schwammberger, Maike Sommer, Christoph Vogelsang, Andreas Wortmannz, Andreas Institute for Software Systems Hamburg University of Technology Software Engineering Group Leibniz Universität Hannover Germany Heriot-Watt University Software and Embedded Systems Engineering Technische Universität Berlin Germany Department of Computing Science University of Oldenburg Heinz Nixdorf Institute Dept. of Computer Science Paderborn University Automated Systems Engineering Technologies Technische Universität Berlin Germany Software Engineering RWTH Aachen University

With the increasing complexity of Cyber-Physical systems, their behavior and decisions become increasingly difficult to understand and comprehend for users and other stakeholders. Our vision is to build self-explainable systems that can, at run-time, answer questions about the system's past, current, and future behavior. As hitherto no design methodology or reference framework exists for building such systems, we propose the Monitor, Analyze, Build, Explain (MAB-EX) framework for building self-explainable systems that leverage requirements- A nd explainability models at run-time. The basic idea of MAB-EX is to first Monitor and Analyze a certain behavior of a system, then Build an explanation from explanation models and convey this EXplanation in a suitable way to a stakeholder. We also take into account that new explanations can be learned, by updating the explanation models, should new and yet unexplainable behavior be detected by the system. Copyright © 2019, The Authors. All rights reserved.

关键词： embedded systems

来源：评论

学校读者我要写书评

暂无评论

Information Flow Analysis of Combined Simulink/Stateflow Models

Information Flow Analysis of Combined Simulink/Stateflow Mod...

引用

IEEE International Conference on Enabling Technologies

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

关键词： Information Flow Analysis Simulink Stateflow

来源：评论

学校读者我要写书评

暂无评论

Self-Awareness for Autonomous systems

引用

PROCEEDINGS OF THE IEEE 2020年第7期108卷 971-975页

作者： Dutt, Nikil Regazzoni, Carlo S. Rinner, Bernhard Yao, Xin Nikil Dutt (Fellow IEEE) received the Ph.D. degree from the University of Illinois at Urbana–Champaign Champaign IL USA in 1989.""He is currently a Distinguished Professor of computer science (CS) cognitive sciences and electrical engineering and computer sciences (EECS) with the University of California at Irvine Irvine CA USA. He is a coauthor of seven books. His research interests include embedded systems electronic design automation (EDA) computer architecture distributed systems healthcare Internet of Things (IoT) and brain-inspired architectures and computing.""Dr. Dutt is a Fellow of ACM. He was a recipient of the IFIP Silver Core Award. He has received numerous best paper awards. He serves as the Steering Committee Chair of the IEEE/ACM Embedded Systems Week (ESWEEK). He is also on the steering organizing and program committees of several premier EDA and embedded system design conferences and workshops. He has served on the Editorial Boards for the IEEE Transactions on Very Large Scale Integration (VLSI) Systems and the ACM Transactions on Embedded Computing Systems and also previously served as the Editor-in-Chief (EiC) for the ACM Transactions on Design Automation of Electronic Systems. He served on the Advisory Boards of the IEEE Embedded Systems Letters the ACM Special Interest Group on Embedded Systems the ACM Special Interest Group on Design Automationt and the ACM Transactions on Embedded Computing Systems. Carlo S. Regazzoni (Senior Member IEEE) received the M.S. and Ph.D. degrees in electronic and telecommunications engineering from the University of Genoa Genoa Italy in 1987 and 1992 respectively.""He is currently a Full Professor of cognitive telecommunications systems with the Department of Electrical Electronics and Telecommunication Engineering and Naval Architecture (DITEN) University of Genoa and a Co-Ordinator of the Joint Doctorate on Interactive and Cognitive Environments (JDICE) international Ph.D. course started initially as EU Erasmus Mundus Project and

Autonomous systems are able to make decisions and potentially take actions without direct human intervention, which requires some knowledge about the system and its environment as well as goal-oriented reasoning. In computer systems, one can derive such behavior from the concept of a rational agent with autonomy (“control over its own actions”), reactivity (“react to events from the environment”), proactivity (“act on its own initiative”), and sociality (“interact with other agents”) as fundamental properties \n[1]\n. Autonomous systems will undoubtedly pervade into our everyday lives, and we will find them in a variety of domains and applications including robotics, transportation, health care, communications, and entertainment to name a few. \nThe articles in this month’s special issue cover concepts and fundamentals, architectures and techniques, and applications and case studies in the exciting area of self-awareness in autonomous systems.

关键词： Special issues and sections Autonomous systems Self-aware Robot sensing systems Computational modeling

来源：评论

学校读者我要写书评

暂无评论

Towards identifying spurious paths in combined Simulink/Stateflow models 46

Towards identifying spurious paths in combined Simulink/Stat...

引用

46. Jahrestagung der Gesellschaft fur Informatik - 46th Annual Meeting of the German Informatics Society, INFORMATIK 2016

作者： Mikulcak, Marcus Göthel, Thomas Herber, Paula Glesner, Sabine Technische Universität Berlin Software and Embedded Systems Engineering Group Ernst-Reuter-Platz 7 Berlin10587 Germany Service and Software Engineering Group Universität Potsdam August-Bebel-Straûe 89 Potsdam14482 Germany

ISBN: (纸本)9783885796534

MATLAB/Simulink and its state machine design toolbox Stateflow are widely-used industrial tools for the development of complex embedded systems. Due to the dynamic as well as heterogeneous nature of models that contain both Simulink and Stateflow components, their analysis poses a difficult challenge. This paper outlines an approach to relate the semantics of both Simulink and Stateflow and how to use it to perform an information flow analysis on a combined Simulink and Stateflow model. In the first step, we analyze the Stateflow automata and generate timed output traces for arbitrary inputs. In the second step, we use an existing timed path condition extraction algorithm for the Simulink components to identify conditions for information flow on paths of interest. Finally, we analyze whether the compiled sets of timed path conditions are contained in the timed output traces that we derive by using a novel trace notation for Stateflow automata. This approach makes it possible to safely rule out the existence of information flow on specific paths through a model. Further, it presents a starting point to reason about non-interference between model parts, compliance with security policies as well as the generation of feasible, efficient test cases.

关键词： Simulink

来源：评论

学校读者我要写书评

暂无评论

Towards the automatic verification of behavior preservation at the transformation level for operational model transformations 4

Towards the automatic verification of behavior preservation ...

引用

4th Workshop on the Analysis of Model Transformations, AMT 2015 - co-located with the 18th International Conference on Model Driven engineering Languages and systems, MODELS 2015

作者： Dyck, Johannes Giese, Holger Lambers, Leen Schlesinger, Sebastian Glesner, Sabine System Analysis and Modeling Group Hasso Plattner Institute at the University of Potsdam Germany Software Engineering for Embedded Systems Technical University of Berlin Germany

The correctness of model transformations and, in particular, behavior preservation is important for model-driven engineering of high quality software. Behavior preservation verification techniques have been pre-sented with automatic tool support for the instance level, i.e. for a given source and target model specified by the model transformation. However, up until now there is no automatic verification approach avail-able for operational model transformations at the transformation level, i.e. for all source and target models specified by an operational model transformation. In this paper, we outline a first approach towards the automatic verification of behavior preservation for operational model transformations at the transformation level extending our previous re-sults for relational model transformations. In particular, we show that in restricted cases the behavior preservation problem for an operational model transformation can be reduced to invariant checking for graph transformation with priorities illustrated by a simple example.

关键词：

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：