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

54th IEEE Frontiers in Education Conference, FIE 2024

作者： Läufer, Konstantin Mertin, Gunda Thiruvathukal, George K. Loyola University Software and Systems Laboratory Department of Computer Science Chicago United States Institute for Software Engineering and Programming Languages University of Lübeck Germany

ISBN: (纸本)9798350351507

Background: In this Innovative Practice Work in Progress, we present our initial efforts to integrate formal methods, with a focus on model-checking specifications written in Temporal Logic of Actions (TLA+), into computer science education, targeting undergraduate juniors/seniors and graduate students. Many safety-critical systems and services crucially depend on correct and reliable behavior. Formal methods can play a key role in ensuring correct and safe system behavior, yet remain underutilized in educational and industry contexts. Aims: We aim to (1) qualitatively assess the state of formal methods in computer science programs, (2) construct level-appropriate examples that could be included midway into one's undergraduate studies, (3) demonstrate how to address successive 'failuresy' through progressively stringent safety and liveness requirements, and (4) establish an ongoing framework for assessing interest and relevance among students. Methods: We detail our pedagogical strategy for embedding TLA+ into an intermediate course on formal methods at our institution. After starting with a refresher on mathematical logic, students specify the rules of simple puzzles in TLA+ and use its included model checker (known as TLC) to find a solution. We gradually escalate to more complex, dynamic, event-driven systems, such as the control logic of a microwave oven, where students will study safety and liveness requirements. We subsequently discuss explicit concurrency, along with thread safety and deadlock avoidance, by modeling bounded counters and buffers. Results: Our initial findings suggest that through careful curricular design and choice of examples and tools, it is possible to inspire and cultivate a new generation of software engineers proficient in formal methods. Conclusions: Our initial efforts suggest that 84% of our students had a positive experience in our formal methods course. Our future plans include a longitudinal analysis within our own institution and

关键词： Students

来源：评论

学校读者我要写书评

暂无评论

A Case Study on Data Protection for a Cloud- and AI-Based Homecare Medical Device 43rd

A Case Study on Data Protection for a Cloud- and AI-Based...

引用

43rd International Conference on Application and Theory of Petri Nets and Concurrency , Petri Nets 2022

作者： Bende, Philipp Vovk, Olga Caraveo, David Pechmann, Ludwig Leucker, Martin Institute for Software Engineering and Programming Languages University of Lübeck Lübeck Germany School of Information Technologies Department of Health Technologies Tallinn University of Technology Tallinn Estonia UniTransferKlinik Lübeck GmbH Lübeck Germany

ISBN: (纸本)9783662681909

To improve the treatment of many diseases, continuous monitoring of the patient at home with the ability of doctors to interact with individual cases demands an increasing number of medical devices connected to the cloud. To support the doctor’s duties, such devices may benefit from AI-based diagnosis routines. In order for such devices to be approved and placed on the market, they need to comply with various legal, regulatory, economic, and social requirements. An integral part of these requirements is the protection of the patients’ data. In this paper, based on a current use case, we describe a workflow on how to identify risks and address their mitigations. To this end, we recall the relevant legal, regulatory, economic, and social data protection requirements. We pursue our findings on a Homecare OCT device that is intended to be used by elderly patients on a daily basis, by taking images of their eyes and sending them for further analysis to a cloud- and AI-based system. The patient’s ophthalmologist gets notified for further dedicated treatment depending on the result. We then compare the Homecare OCT device with a clinical OCT System in regard to various risks to patient data which arise when a medical system is used outside of a secure hospital environment. To perform the risk management, we describe (i) the architecture of both systems, (ii) analyze their data flow, (iii) discuss several vectors of attack, (iv) propose ways to mitigate the risks, and (v) discuss the handling of potential data breaches. © 2024, The Author(s), under exclusive license to Springer-Verlag GmbH, DE, part of Springer Nature.

关键词： Decision support systems

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

WIP: An Engaging Undergraduate Intro to Model Checking in software engineering Using TLA+

WIP: An Engaging Undergraduate Intro to Model Checking in So...

引用

Frontiers in Education (FIE) Conference

作者： Konstantin Läufer Gunda Mertin George K. Thiruvathukal Department of Computer Science Software and Systems Laboratory Loyola University Chicago Institute for Software Engineering and Programming Languages University of Lübeck

ISBN: (数字)9798350351507

ISBN: (纸本)9798350363067

Background: In this Innovative Practice Work in Progress, we present our initial efforts to integrate formal methods, with a focus on model-checking specifications written in Temporal Logic of Actions $(\text{TLA}^{+})$ , into computer science education, targeting undergraduate juniors/seniors and graduate students. Many safety-critical systems and services crucially depend on correct and reliable behavior. Formal methods can play a key role in ensuring correct and safe system behavior, yet remain underutilized in educational and industry contexts. Aims: We aim to (1) qualitatively assess the state of formal methods in computer science programs, (2) construct level-appropriate examples that could be included midway into one's undergraduate studies, (3) demonstrate how to address successive “failuresy” through progressively stringent safety and liveness requirements, and (4) establish an ongoing framework for assessing interest and relevance among students. Methods: We detail our pedagogical strategy for embedding $\text { TLA }^{+}$ into an intermediate course on formal methods at our institution. After starting with a refresher on mathematical logic, students specify the rules of simple puzzles in $\text { TLA }^{+}$ and use its included model checker (known as TLC) to find a solution. We gradually escalate to more complex, dynamic, event-driven systems, such as the control logic of a microwave oven, where students will study safety and liveness requirements. We subsequently discuss explicit concurrency, along with thread safety and deadlock avoidance, by modeling bounded counters and buffers. Results: Our initial findings suggest that through careful curricular design and choice of examples and tools, it is possible to inspire and cultivate a new generation of software engineers proficient in formal methods. Conclusions: Our initial efforts suggest that 84% of our students had a positive experience in our formal methods course. Our future plans include a longitudi

关键词： Computer science Open Access Model checking System recovery software Safety Logic Reliability Proposals software engineering

来源：评论

学校读者我要写书评

暂无评论

Optimistic Versioning for Conflict-tolerant Collaborative Blended Modeling 10

Optimistic Versioning for Conflict-tolerant Collaborative Bl...

引用

STAF 2022 Workshop: 10th International Workshop on Bidirectional Transformations, BX 2022, 2nd International Workshop on Foundations and Practice of Visual Modeling, FPVM 2022 and 2nd International Workshop on MDE for Smart IoT Systems, MeSS 2022

作者： Exelmans, Joeri Pietron, Jakob Raschke, Alexander Vangheluwe, Hans Tichy, Matthias Department of Computer Science University of Antwerp - Flanders Make Antwerp Belgium Institute of Software Engineering and Programming Languages Ulm University Ulm Germany

Optimistic versioning is a key component in supporting collaborative workflows. Text-based versioning has been widely adopted for versioning code, but in model-driven engineering, dealing with visual concrete syntaxes, new methods are required. In the case of blended modeling, a mixture of both textual and visual syntaxes, concurrently editable and synchronizable, introduces additional challenges. We propose a type of operation-based versioning to record not only user edits, but also bi-directional change propagations between concrete and abstract syntax. This way we can support blended modeling with layout continuity, and flexible handling of missing information (e. g., layout information) when rendering changes from abstract to concrete syntax. In addition, the proposed versioning approach enables collaborative conflict resolution by allowing partial conflict resolution, thus deferring a final resolution. © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

关键词： Abstracting

来源：评论

学校读者我要写书评

暂无评论

WIP: An Engaging Undergraduate Intro to Model Checking in software engineering Using TLA+

arXiv

引用

arXiv 2024年

作者： Läufer, Konstantin Mertin, Gunda Thiruvathukal, George K. Software and Systems Laboratory Department of Computer Science Loyola University Chicago United States Institute for Software Engineering and Programming Languages University of Lübeck Germany

Background: In this Innovative Practice Work in Progress, we present our initial efforts to integrate formal methods, with a focus on model-checking specifications written in Temporal Logic of Actions (TLA+), into computer science education, targeting undergraduate juniors/seniors and graduate students. Many safety-critical systems and services crucially depend on correct and reliable behavior. Formal methods can play a key role in ensuring correct and safe system behavior, yet remain underutilized in educational and industry contexts. Aims: We aim to (1) qualitatively assess the state of formal methods in computer science programs, (2) construct level-appropriate examples that could be included midway into one’s undergraduate studies, (3) demonstrate how to address successive "failures" through progressively stringent safety and liveness requirements, and (4) establish an ongoing framework for assessing interest and relevance among students. Methods: We detail our pedagogical strategy for embedding TLA+ into an intermediate course on formal methods at our institution. After starting with a refresher on mathematical logic, students specify the rules of simple puzzles in TLA+ and use its included model checker (known as TLC) to find a solution. We gradually escalate to more complex, dynamic, event-driven systems, such as the control logic of a microwave oven, where students will study safety and liveness requirements. We subsequently discuss explicit concurrency, along with thread safety and deadlock avoidance, by modeling bounded counters and buffers. Results: Our initial findings suggest that through careful curricular design and choice of examples and tools, it is possible to inspire and cultivate a new generation of software engineers proficient in formal methods. Conclusions: Our initial efforts suggest that 84% of our students had a positive experience in our formal methods course. Our future plans include a longitudinal analysis within our own institution and

关键词： Students

来源：评论

学校读者我要写书评

暂无评论

Uvlhub: A Feature Model Data Repository Using Uvl and Open Science Principles

SSRN

引用

SSRN 2023年

作者： Romero-Organvidez, David Galindo, José A. Sundermann, Chico Horcas, Jose-Miguel Benavides, David Department of Computer Languages and Systems University of Seville Spain Institute of Software Engineering and Programming Languages Ulm University Germany CAOSD ITIS Software University of Málaga Spain

Feature models are the de facto standard for modelling variabilities and commonalities. Concrete models in different domains exist;however, many are in private or sparse repositories or belong to discontinued projects. The dispersion of knowledge of feature models hinders the study and reuse of these artefacts in different studies. The Universal Variability Language (UVL) is a community effort textual feature model language that promotes a common way of serialising feature models independently of concrete tools. Open science principles promote transparency, accessibility, and collaboration in scientific research. Although some attempts exist to promote feature model sharing, the existing solutions lack open science principles by design. In addition, existing and public feature models are described using formats not always supported by current tools. This paper presents UVLHUB, a repository of feature models in UVL format. UVLHUB provides a front end that facilitates the search, upload, storage, and management of feature model datasets, improving the capabilities of discontinued proposals. Furthermore, the tool communicates with Zenodo providing a permanent save of datasets and following open science principles. UVLHUB includes existing datasets and is readily available to include new data and functionalities in the future. It is maintained by three active universities in variability modelling. © 2023, The Authors. All rights reserved.

关键词： Concretes

来源：评论

学校读者我要写书评

暂无评论

Collaboration And Versioning Framework – A Systematic Top-Down Approach

Collaboration And Versioning Framework – A Systematic Top-D...

引用

Conference on Model Driven engineering languages and Systems Companion (MODELS-C)

作者： Jakob Pietron Alexander Raschke Joeri Exelmans Matthias Tichy Institute of Software Engineering and Programming Languages Ulm University Ulm Germany Department of Computer Science University of Antwerp – Flanders Make Antwerp Belgium

CONTEXT: Versioning allows users to efficiently create and evolve artifacts, not only but especially in the domain of model-driven engineering. Due to collaboration tools, the place and time where users jointly work at their artifacts do not play an important role anymore. Objective: We systematically elaborated a classification framework for collaboration and versioning tools. The intention is threefold: First, it should be possible to classify existing approaches. Second, deriving from user goals requirements to be met, and capabilities to be supported by a new tool. Third, given a set of capabilities, highlight which user goals can be achieved. Method: According to Kang and Lee, we systematically elaborated a problem space and a solution space and created mappings between both spaces and their sub-spaces. To demonstrate the applicability, we classified existing VCS like git, Google Docs, and several MDE-specific approaches. Results: The created feature diagram covers 238 features and contains about 87 constraints. Conclusion: The developed framework supports researchers and developers in classifying their tools, revealing new opportunities to improve their tools, and guiding the development of new tools.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A Case Study on Data Protection for a Cloud- and AI-based Homecare Medical Device

A Case Study on Data Protection for a Cloud- and AI-based Ho...

引用

2022 International Health Data Workshop, HEDA 2022

作者： Bende, Philipp Vovk, Olga Caraveo, David Pechmann, Ludwig Leucker, Martin University of Lübeck Institute for Software Engineering and Programming Languages Lübeck Germany Tallinn University of Technology School of Information Technologies Department of Health Technologies Tallinn Estonia UniTransferKlinik Lübeck GmbH Lübeck Germany

To improve the treatment of many diseases, continuous monitoring of the patient at home with the ability of doctors to interact with individual cases demands an increasing number of medical devices connected to the cloud. To support the doctor’s duties, such devices may benefit from AI-based diagnosis routines. In order for such devices to be approved and placed on the market, they need to comply with various legal, regulatory, economic, and social requirements. An integral part of these requirements is the protection of the patients’ data. In this paper, based on a current use case, we describe a workflow on how to identify risks and address their mitigations. To this end, we recall the relevant legal, regulatory, economic, and social data protection requirements. We pursue our findings on a Homecare OCT device that is intended to be used by elderly patients on a daily basis, by taking images of their eyes and sending them for further analysis to a cloud- and AI-based system. The patient’s ophthalmologist gets notified for further dedicated treatment depending on the result. To perform the risk management, we describe (i) the architecture of the homecare system, (ii) analyze its data flow, (iii) discuss several vectors of attack, and (iv) propose ways to mitigate the risks. © 2022 Copyright for this paper by its authors.

关键词： Risk management

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：