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

2023 Workshop on Applications of Formal Methods and Digital twins, FMDt 2023

作者： leucker, Martin Sachenbacher, Martin Vosteen, lars B. Institute for Software Engineering and Programming Languages Universität zu Lübeck Lübeck Germany

In this paper, we explain through a case study how to develop a digital twin that can be used for safety analysis of missions in physical contexts. More specifically, we consider a scenario where firefighters are operating inside a building under fire, but communicating online with a mission control station. One of the main tasks of the mission control is to ensure that the firefighters always have enough oxygen to exit the building safely. to this end, a Digital twin can be created that reflects the physical structure of the burning building, the location of the firefighters and the oxygen level in their breathing apparatus. the Digital twin uses these models and a shortest path algorithm to estimate the oxygen required to exit the building, and alerts mission control and the respective firefighter to exit the building on time. the case study is used to illustrate key concepts for building Digital twins in safety-critical contexts. © 2023 CEUR-WS. All rights reserved.

关键词： Safety engineering

来源：评论

学校读者我要写书评

暂无评论

A Model-Based Approach for Monitoring and Diagnosing Digital twin Discrepancies 35

A Model-Based Approach for Monitoring and Diagnosing Digital...

引用

35th International Conference on Principles of Diagnosis and Resilient Systems, DX 2024

作者： Hosseinkhani, Elaheh leucker, Martin Sachenbacher, Martin Streichhahn, Hendrik Vosteen, lars B. Institute for Software Engineering and Programming Languages Universität zu Lübeck Germany Dräger Safety AG & Co. KGaA. Lübeck Germany

ISBN: (纸本)9783959773560

Recent decades have seen the increasing use of Digital twins (Dts) - that is, digital models used over the lifetime of a physical product or system for tasks such as predictive maintenance or optimization - in a number of domains such as buildings, manufacturing, or design. Dts face a challenge known as the Dt synchronization problem;a Dt, often based on machine-learned, or complex simulation models, needs to adequately mirror the physical product or system at all times, as any deviations might affect the quality of predictions or control actions. In this paper, we present a model-based approach that aims to add a level of awareness to Dt models by supervising if they are in sync with the physical counterpart. the approach is agnostic to the type of models used in the Dt, as long as they are compositional, and based on monitoring critical properties (behavioral or functional aspects) of the system at run-time. In the case violations are detected, it reasons on the Dt's structure to localize and identify parts of the model that cause deviations and need to be adapted. We give a formal description and an implementation of this approach, and illustrate it with an example from building climatisation. © Elaheh Hosseinkhani, Martin leucker, Martin Sachenbacher, Hendrik Streichhahn, and lars B. Vosteen.

关键词： Predictive maintenance

来源：评论

学校读者我要写书评

暂无评论

Achieving Complete Structural test Coverage in Embedded Systems Using trace-Based Monitoring 35

Achieving Complete Structural Test Coverage in Embedded Syst...

引用

35th International Conference on Principles of Diagnosis and Resilient Systems, DX 2024

作者： Weiss, Alexander Schulz, Albert Heininger, Martin Sachenbacher, Martin leucker, Martin Accemic Technologies GmbH Kiefersfelden Germany Heicon Global Engineering GmbH Schwendi Germany Institute for Software Engineering and Programming Languages Universität zu Lübeck Germany

ISBN: (纸本)9783959773560

this paper presents a systematic approach to achieving, in a well-defined sense, 100% structural test coverage for large embedded software projects. In embedded systems, high code coverage is a critical part of the testing process to ensure that the system works correctly. Measuring code coverage provides insight into the effectiveness of the testing process, the quality of the software, and can help identify untested or partially tested areas of the code. traditionally, coverage is often measured when unit tests are executed. the proposed approach instead uses integration tests as the starting point for determining test completeness. Measuring code coverage at the integration test level in embedded systems can be challenging due to the limitations of software instrumentation (additional memory requirements and additional CPU load). to overcome these limitations, embedded trace technology is used to measure code coverage continuously and non-intrusively. the use of these techniques will help to increase the reliability of embedded software and reduce the likelihood of missed integration tests, missed high-level requirements, and undetected software defects. © Alexander Weiss, Albert Schulz, Martin Heininger, Martin Sachenbacher, and Martin leucker.

关键词： Integration testing

来源：评论

学校读者我要写书评

暂无评论

Runtime Verification of Autonomous Systems Utilizing Digital twins as a Service 5

Runtime Verification of Autonomous Systems Utilizing Digital...

引用

5th IEEE International Conference on Autonomic Computing and Self-Organizing Systems Companion, ACSOS-C 2024

作者： Kristensen, Morten Haahr Bonizzi, Alberto Gomes, Claudio Hansen, Simon thrane Isasa, Carlos Iven, Hannes Kamburjan, Eduard larsen, Peter Gorm leucker, Martin talasila, Prasad tang, Valdemar trojgard tonetta, Stefano Vosteen, lars B. Wright, thomas Aarhus University Department of Electrical and Computer Engineering Denmark Fondazione Bruno Kessler Italy University of Luxembourg Interdisciplinary Centre for Security Reliability and Trust Luxembourg Institute for Software Engineering and Programming Languages Universität zu Lübeck Germany University of Oslo Department of Informatics Norway

ISBN: (纸本)9798350389760

Autonomous Systems (AS) enable systems to adapt to drastic and unprecedented environmental changes, a capability that can be enhanced through the utilization of Digital twins (Dts). However, the additional capabilities of AS come at the cost of explainability, as the expanding adaptation space complicates the reasoning about the system's behavior. For certain types of systems, it is crucial to ensure that specific properties are upheld despite the system's autonomous behavior. to facilitate the monitoring of these properties, we propose the use of Runtime Verification (RV). this tutorial demonstrates the integration of RV tools into the Digital twins as a Service (DtaaS) platform to monitor and verify the behavior of AS in real-time. By exploring various methods to incorporate RV tools within a Dt context, the tutorial aims to advance the application of RV technologies in autonomic computing and self-adaptive system design. Specifically, we demonstrate how the behavior of a self-configuring Dt can be verified utilizing RV. this is accomplished through the DtaaS platform, which supports seamless deployment of Dt-based AS. © 2024 IEEE.

关键词： Adaptive systems

来源：评论

学校读者我要写书评

暂无评论

Runtime Verification of Autonomous Systems Utilizing Digital twins as a Service

Runtime Verification of Autonomous Systems Utilizing Digital...

引用

Autonomic Computing and Self-Organizing Systems Companion (ACSOS-C), IEEE International Conference on

作者： Morten Haahr Kristensen Alberto Bonizzi Cláudio Gomes Simon thrane Hansen Carlos Isasa Hannes Iven Eduard Kamburjan Peter Gorm larsen Martin leucker Prasad talasila Valdemar trøjgård tang Stefano tonetta lars B. Vosteen thomas Wright Department of Electrical and Computer Engineering Aarhus University Denmark Fondazione Bruno Kessler Italy Interdisciplinary Centre for Security Reliability and Trust University of Luxembourg Institute for Software Engineering and Programming Languages Universität zu Lübeck Germany Department of Informatics University of Oslo Norway

ISBN: (数字)9798350389760

ISBN: (纸本)9798350389777

关键词： Runtime Costs Autonomous systems tutorials Real-time systems Cognition Digital twins Distributed computing Monitoring System analysis and design

来源：评论

学校读者我要写书评

暂无评论

ANAlYZING ROBUStNESS OF ANGlUIN'S l∗ AlGORItHM IN PRESENCE OF NOISE

arXiv

引用

arXiv 2023年

作者： Ye, lina Khmelnitsky, Igor Haddad, Serge Barbot, Benoît Bollig, Benedikt leucker, Martin Neider, Daniel Roy, Rajarshi Université Paris-Saclay CNRS ENS Paris-Saclay CentraleSupélec LMF France Université Paris-Saclay CNRS ENS Paris-Saclay LMF France Université Paris-Est Créteil France Institute for Software Engineering and Programming Languages Universität zu Lübeck Germany TU Dortmund University Germany Center for Trustworthy Data Science and Security University Alliance Ruhr Germany Max Planck Institute for Software Systems Kaiserslautern Germany

Angluin's l∗ algorithm learns the minimal deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively correct (PAC) version substitutes an equivalence query by numerous random membership queries to get a high level confidence to the answer. thus it can be applied to any kind of device and may be viewed as an algorithm for synthesizing an automaton abstracting the behavior of the device based on observations. Here we are interested on how Angluin's PAC learning algorithm behaves for devices which are obtained from a DFA by introducing some noise. More precisely we study whether Angluin's algorithm reduces the noise and produces a DFA closer to the original one than the noisy device. We propose several ways to introduce the noise: (1) the noisy device inverts the classification of words w.r.t. the DFA with a small probability, (2) the noisy device modifies with a small probability the letters of the word before asking its classification w.r.t. the DFA, (3) the noisy device combines the classification of a word w.r.t. the DFA and its classification w.r.t. a counter automaton, and (4) the noisy DFA is obtained by a random process from two DFA such that the language of the first one is included in the second one. then when a word is accepted (resp. rejected) by the first (resp. second) one, it is also accepted (resp. rejected) and in the remaining cases, it is accepted with probability 0.5. Our main experimental contributions consist in showing that: (1) Angluin's algorithm behaves well whenever the noisy device is produced by a random process, (2) but poorly with a structured noise, and, that (3) is able to eliminate pathological behaviours specified in a regular way. theoretically, we show that randomness almost surely yields systems with non-recursively enumerable languages. © 2023, CC BY.

关键词： Random processes

来源：评论

学校读者我要写书评

暂无评论

Analyzing Robustness of Angluin’s l∗ Algorithm in Presence of Noise

arXiv

引用

arXiv 2022年

作者： Khmelnitsky, Igor Haddad, Serge Ye, lina Barbot, Benoît Bollig, Benedikt leucker, Martin Neider, Daniel Roy, Rajarshi Université Paris-Saclay CNRS ENS Paris-Saclay INRIA LMF France Université Paris-Saclay CNRS ENS Paris-Saclay CentraleSupélec LMF France Université Paris-Est Créteil France Université Paris-Saclay CNRS ENS Paris-Saclay LMF France Institute for Software Engineering and Programming Languages Universität zu Lübeck Germany Carl von Ossietzky University of Oldenburg Germany Max Planck Institute for Software Systems Kaiserslautern Germany

Angluin’s l∗ algorithm learns the minimal (complete) deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively correct (PAC) version substitutes an equivalence query by a large enough set of random membership queries to get a high level confidence to the answer. thus it can be applied to any kind of (also non-regular) device and may be viewed as an algorithm for synthesizing an automaton abstracting the behavior of the device based on observations. Here we are interested on how Angluin’s PAC learning algorithm behaves for devices which are obtained from a DFA by introducing some noise. More precisely we study whether Angluin’s algorithm reduces the noise and produces a DFA closer to the original one than the noisy device. We propose several ways to introduce the noise: (1) the noisy device inverts the classification of words w.r.t. the DFA with a small probability, (2) the noisy device modifies with a small probability the letters of the word before asking its classification w.r.t. the DFA, and (3) the noisy device combines the classification of a word w.r.t. the DFA and its classification w.r.t. a counter automaton. Our experiments were performed on several hundred DFAs. Our main contributions, bluntly stated, consist in showing that: (1) Angluin’s algorithm behaves well whenever the noisy device is produced by a random process, (2) but poorly with a structured noise, and, that (3) almost surely randomness yields systems with non-recursively enumerable languages. © 2022, CC BY.

关键词： learning algorithms

来源：评论

学校读者我要写书评

暂无评论

Non-intrusive runtime verification within a system-on-chip

Ada User Journal

引用

Ada User Journal 2018年第4期39卷 296-299页

作者： Rufino, José Casimiro, António lange, Felix Dino leucker, Martin Scheffel, torben Schmitz, Malte thoma, Daniel LASIGE Faculdade de Ciências Universidade de Lisboa Portugal Institute for Software Engineering and Programming Languages Universität zu Lübeck Lübeck Germany

this paper describes how to enrich a System-on-Chip (SoC) design by flexible monitoring capabilities allowing to analyze the system's execution for ensuring safety requirements. to this end, a general SoC architecture is described enriched by observation means. Moreover, it is described how verification properties expressed in a temporal stream-based specification language can be translated into a monitor expressed in a hardware description language (Verilog) checking the underlying property. Finally, the link between the SoC and the monitoring unit is explained. Overall, a self-observing system is obtained that works coherently with the SoC. © 2018 *** rights reserved.

关键词： System-on-chip

来源：评论

学校读者我要写书评

暂无评论

Property-Directed verification of recurrent neural networks

arXiv

引用

arXiv 2020年

作者： Khmelnitsky, Igor Neider, Daniel Roy, Rajarshi Barbot, Benoît Bollig, Benedikt Finkel, Alain Haddad, Serge leucker, Martin Ye, lina LSV CNRS ENS Paris-Saclay Université Paris-Saclay France Inria France Max Planck Institute for Software Systems Kaiserslautern Germany Université Paris-Est Créteil France Institute for Software Engineering and Programming Languages Universität zu Lübeck Germany CentraleSupélec Université Paris-Saclay France Institut Universitaire de France France

this paper presents a property-directed approach to verifying recurrent neural networks (RNNs). to this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning. this model may then be analyzed using model checking as verification technique. the term property-directed reflects the idea that our procedure is guided and controlled by the given property rather than performing the two steps separately. We show that this not only allows us to discover small counterexamples fast, but also to generalize them by pumping towards faulty flows hinting at the underlying error in the *** Codes 68Q60, 68t07 Copyright © 2020, the Authors. All rights reserved.

关键词： Recurrent neural networks

来源：评论

学校读者我要写书评

暂无评论

Secured SOA for the safe interconnection of medical devices (Position paper)

Secured SOA for the safe interconnection of medical devices ...

引用

Workshops der tagung software engineering, SE-WS 2015

作者： leucker, Martin Schmitz, Malte Institute for Software Engineering and Programming Languages Universität zu Lübeck Germany Graduate School for Computing in Medicine and Life Sciences Universität zu Lübeck Germany

this position paper presents a concept on how the dynamic interconnection of medical devices in a service oriented architecture (SOA) can be secured based on formal interface descriptions. In the framework OpenSDC used in the research project *** formal interface descriptions are already used to model medical devices. the new approach is to use this formal descriptions to ensure the correct usage of the interface at runtime and to support developers in implementing medical devices with OpenSDC at the same time.

关键词： Service oriented architecture (SOA)

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：