Auflistung nach Schlagwort "Verifikation"
1 - 7 von 7
Treffer pro Seite
Sortieroptionen
- KonferenzbeitragEin Ansatz zur nachvollziehbaren Verifikation medizinisch-cyber-physikalischer Systeme(Software Engineering und Software Management 2018, 2018) Padberg, Julia; Schlaefer, Alexander; Schupp, SibylleMedizinische cyberphysikalische Systeme erfordern einerseits die Adaption an patientenindividuelle Parameter während einer Behandlung und andererseits den Nachweis eines sicheren Systemverhaltens. Wir schlagen vor, Nachweisbarkeit mittels Online Model-Checking und Nachvollziehbarkeit durch Anwendung von regelbasierten Transformationen zu verbinden.
- Konferenz-AbstractBericht(Softwaretechnik-Trends Band 44, Heft 2, 2024) Sokenou, Dehla; Friske, Mario; Güldali, Baris; Faragó, David; Winter, MarioDas 49. Treffen der GI-Fachgruppe TAV fand am 15. und 16. Februar 2024 statt und stand unter dem Motto Qualität sichtbar, messbar und bewertbar machen. Das Programm umfasste neben der Keynote von Mario Winter acht weitere Vorträge aus den Bereichen Best Practices, KI und Qualitätssicherung und Erfahrungen mit Toolchains.
- KonferenzbeitragBericht vom 42. Treffen der GI-Fachgruppe Test, Analyse & Verifikation von Software (TAV 42)(Softwaretechnik-Trends Band 39, Heft 3, 2019) Pietschker, AndrejDas 42. Treffen der GI-Fachgruppe TAV am Donnerstag und Freitag, den 14. und 15. Juni 2017 bei der IBM Deutschland GmbH in München stand unter dem Motto Testen von IoT. Das Treffen wurde von über 60 Teilnehmenden aus Industrie, öffentlicher Verwaltung und Hochschulen besucht.
- KonferenzbeitragBericht vom Treffen der GI-Fachgruppe Test, Analyse und Verifikation von Software (TAV 48)(Softwaretechnik-Trends Band 43, Heft 3, 2023) Sokenou, D.; Friske, M.; Güldali, B.; Faragó, D.; Moritz, B.; Winter, M.Bericht vom 48. Treffen der Fachgruppe TAV und Berichte aus den Arbeitskreisen
- TextdokumentHolistische Verifikation von Hybriden Quantenprogrammen durch Software Bounded Model Checking(INFORMATIK 2021, 2021) Klamroth,Jonas; Scheerer, Max; Denninger, OliverQuantencomputer erschließen uns durch ihren überpolynomiellem Speedup neue Anwendungsfelder für schwer-berechenbare Probleme. Der Entwurf von Quantenalgorithmen ist bisher allerdings komplex und fehleranfällig. Daher ist zu erwarten, dass vorerst nur einzelne Subroutinen eines Programms auf Quantencomputern umgesetzt werden. Um die Korrektheit solcher Programme garantieren zu können, sind neue Ansätze erforderlich. In dieser Arbeit stellen wir einen Ansatz zum vollautomatischen Nachweis der Korrektheit von Programmen mit eingebetteten Quantenalgorithmen vor. Dazu bauen wir auf Bounded-Model-Checking-Verfahren auf, welche die Fehlerfreiheit hinsichtlich einer gegebenen Spezifikation beweisen können. Als Spezifikationssprache verwenden wir JML. Dabei werden die Quantenalgorithmen als Quantenschaltkreis beschrieben und in Java eingebettet. Wir zeigen die Umsetzbarkeit unseres Ansatzes an zwei etablierten Quantenalgorithmen.
- KonferenzbeitragModellierung, Verifikation und Synthese von validen Planungszuständen für Fernsehausstrahlungen(Modellierung 2020, 2020) Drave, Imke; Henrich, Timo; Hölldobler, Katrin; Kautz, Oliver; Michael, Judith; Rumpe, BernhardFür die Gestaltung von audiovisuellen Medienangeboten wie Fernsehprogramm und Video-On-Demand Angeboten müssen Lizenzverträge abgeschlossen werden. Aus diesen Verträgen ergeben sich Vorgaben, die bei der Planung der Angebote eingehalten werden müssen. Mit wachsender Anzahl an Verträgen und Formulierungen innerhalb der Verträge und ohne eine Möglichkeit diese einheitlich bzw. formal zu beschreiben, besteht das Risiko von Fehlinterpretationen und daraus resultierenden Fehlplanungen, welche zu Nachverhandlungen oder Vertragsstrafen führen können. Diese Arbeit beschreibt eine Domänenspezifische Sprache (DSL), die die Modellierung solcher Restriktionen durch Endanwenderinnen ohne tieferliegende Informatikkenntnisse ermöglicht. Darüber hinaus wurde die Sprache genutzt um eine Verifikation von Planungen sowie die Berechnung von erlaubten Verplanungszeiträumen zu automatisieren. Der praktische Einsatz dieser DSL in der Programmplanung hat gezeigt, dass Missverständnisse im Bezug auf die Bedeutung einer Restriktion minimiert, die Ermittlung erlaubter Verplanungszeiträume automatisiert und somit das Risiko von Fehlplanungen deutlich reduziert werden konnte.
- KonferenzbeitragZukunft durch hybride IT- und KI-Innovationen(INFORMATIK 2023 - Designing Futures: Zukünfte gestalten, 2023) Mainzer, KlausUm Zukünfte zu gestalten, fordert dieser Artikel ein Innovationsportfolio von IT- und KI- Technologien, die als Basis-, Brücken- und Zukunftstechnologien aufeinander abgestimmt sind [M23]. Wie ein Portfolio von Aktien ist auch ein Innovationsportfolio dynamisch und muss ständig gestaltet werden. Methodisch wird dazu auf die mathematische Theorie komplexer Systeme und nichtlinearer Dynamik zurückgegriffen, mit der sich komplexe Systeme und Netzwerke in Natur, Wirtschaft und Gesellschaft modellieren lassen. Chaos und Risiken werden auf dieser Grundlage in Frühwarnsystemen abschätzbar und in strategisches Handeln umsetzbar. Ziel ist ein nachhaltiges Innovationsportfolio (3.), in dem hybride KI mit symbolischer KI und subsymbolische KI des Machine Learning (3.1), hybrides Computing mit klassischem Computing und Quantencomputing (3.2), Hybridrechner mit Analogrechner und Digitalcomputer (3.3), hybride Robotik bzw. Embodied Robotik („Embodied Mind“) mit analoger Robotik und digitaler Robotik (3.4) und neurobiologisch orientiertem Computing (3.5) verbunden werden. Eine große Herausforderung für die Zukunft ist die Sicherung dieser Technologien durch Verifikation und Erklärbarkeit [MK22].