checkAll

checkAll

In modern software and systems engineering formal verification gets more and more important to ensure safeness of safety critical systems. Especially, if the systems get in contact with human beings. Therefore, we research for new techniques in the domain of formal verification for software intensive systems.

One method, often used in this context of formal verification is model checking. At the moment, there exists a large number of tools and corresponding theories. Some for qualitative and some for quantitative analysis. However, most of them are not really applicable to real world problems. But if they, only high educated experts are capable to handle the formal models and verification.

In order to make model checking more applicable, we are looking for new theories to be able to verify larger problems. One applicable idea was presented in the master thesis “A Backward Model Checking Approach with slicing”, were we used a SMT representation of the state model to search the state space and verify the model against a given specification.

Another idea is situated in the domain of quantitative model checking, where it is not asked if something bad happen but how probable it is.

Here, the approach is to use monte carlo imulation with importance sampling to get reliable estimations for the hazard probabilities. But in contrast to other researchers also using monte carlo simulation, we try to develop some method, which is applicable for an unknown model, i.e., the sampling technique does not focus on the deeper semantic of the model.

This topic is under ongoing research. For questions please refer to Tim Gonschorek.

Publications

2019

Gonschorek, Tim; Bergt, Philipp; Filax, Marco; Ortmeier, Frank

Integrating Safety Design Artifacts into System Development Models Using SafeDeML Inproceedings

Papadopoulos, Yiannis; Aslansefat, Koorosh; Katsaros, Panagiotis; Bozzano, Marco (Hrsg.): Model-Based Safety and Assessment, S. 93–106, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-32872-6.

Abstract | Links | BibTeX

Gonschorek, Tim; Bergt, Philipp; Filax, Marco; Ortmeier, Frank; von Hoyningen-Hüne, Jan; Piper, Thorsten

SafeDeML: On Integrating the Safety Design into the System Model Inproceedings

Romanovsky, Alexander; Troubitsyna, Elena; Bitsch, Friedemann (Hrsg.): Computer Safety, Reliability, and Security, S. 271–285, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-26601-1.

Abstract | Links | BibTeX

2018

Gonschorek, Tim; Zeller, Marc; Ortmeier, Frank; Höfig, Kai

Fault Trees vs. Component Fault Trees: An Empirical Study Inproceedings

Gallina B. Skavhaug A., Schoitsch Bitsch E F (Hrsg.): Computer Safety, Reliability, and Security. SAFECOMP 2018., Springer, Cham, 2018, ISBN: 978-3-319-99228-0.

Links | BibTeX

Schillreff, Nadia; Ortmeier, Frank

Learning-based Kinematic Calibration using Adjoint Error Model Inproceedings

SciTePress, (Hrsg.): Proceedings of the 15th International Conference on Informatics in Control, Automation and Robotics - Volume 2: ICINCO, 2018, ISBN: 978-989-758-321-6.

Abstract | Links | BibTeX

Gonschorek, Tim; Bedau, Ludwig; Ortmeier, Frank

Automatic Model-based Verification of Railway Interlocking Systems using Model Checking Inproceedings

Haugen, Stein (Hrsg.): Proceedings of ESREL 2018, S. 741-748, CRC Press, London, 2018.

Abstract | Links | BibTeX

Schott, Kevin Michael

Extraktion relevanter API-spezifischer Informationen zur automatischen Korrektur von Softwarefehlern Abschlussarbeit

Otto-von-Guericke-Unviersität Magdeburg, 2018.

Abstract | BibTeX

Bedau, Ludwig; Gonschorek, Tim; Ortmeier, Frank

Sicherheitsanalyse eines Bahnhofstellwerkes Konferenzbericht

Horber Schienen Tage 35 , 2018.

Links | BibTeX

2017

Gonschorek, Tim; Rabeler, Ben Lukas; Ortmeier, Frank; Schomburg, Dirk

On Improving Rare Event Simulation for Probabilistic Safety Analysis Inproceedings

Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, S. 15-24, ACM New York, NY, USA ©2017 , 2017, ISBN: 978-1-4503-5093-8.

Abstract | Links | BibTeX

Gonschorek, Tim; Filax, Marco; Ortmeier, Frank

A Verification Environment for Critical Systems: Integrating Formal Methods into the Safety Development Life-cycle Sonstige

Invited Paper: 5th International Symposium on Model-Based Safety and Assessment (IMBSA 2017), 2017.

Links | BibTeX

Bitsch, Friedemann; Filax, Marco; Gonschorek, Tim; Ortmeier, Frank; Schumacher, Rolf

Effiziente Sicherheitsnachweisführung mithilfe modellbasierter Systemanalyse Artikel

Signal + Draht, 2017.

Abstract | Links | BibTeX

Krüger, Jacob; Nielebock, Sebastian; Krieter, Sebastian; Diedrich, Christian; Leich, Thomas; Saake, Gunter; Zug, Sebastian; Ortmeier, Frank

Beyond Software Product Lines: Variability Modeling in Cyber-Physical Systems Inproceedings

Proceedings of the 21st International Systems and Software Product Line Conference (SPLC 2017) - Vision Track, S. 237-241, 2017.

Abstract | Links | BibTeX

Bedau, Ludwig

Modellbasierte Sicherheitsanalyse eines Bahnhofsstellwerks Abschlussarbeit

Otto-von-Guericke-Universität Magdeburg, 2017.

Abstract | Links | BibTeX

2016

Filax, Marco; Gonschorek, Tim; Ortmeier, Frank

Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models Inproceedings

Publishing, Springer International (Hrsg.): Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings, S. 106 - 122, 2016, ISBN: 978-3-319-33951-1.

Abstract | Links | BibTeX

Filax, Marco; Gonschorek, Tim; Hebecker, Tanja; Lipaczewski, Michael; Madalinski, Agnes; Ortmeier, Frank; Fietze, Mario; Schumacher, Rolf

Bringing formal methods “on the rail” - Modellbasierte Systemanalyse in der Sicherheitsnachweisführung Artikel

Der Eisenbahn Ingenieur, S. 24 -27, 2016.

Abstract | Links | BibTeX

2015

Hamannn, Dominik

Kopplung formaler Modelle mit realweltlichen Umgebungsmodellen Abschlussarbeit

Otto-von-Guericke-Universität Magdeburg, 2015.

Abstract | Links | BibTeX

Heumüller, Robert

Multi-Abstraction Model Based Software Development for Embedded Low-Cost Applications Abschlussarbeit

2015.

Links | BibTeX

Gonschorek, Tim; Ortmeier, Frank

Slice or Unfold - Experiments on Checking Synchronous Models with Backwards Slicing Inproceedings

of Control, International Federation Automatic (Hrsg.): 5th International Workshop on Dependable Control of Discrete Systems (DCDS 2015), 2015, (accepted, will be published this year).

Abstract | Links | BibTeX

Rabeler, Ben

Abstraktion kontinuierlichen Verhaltens zur modellbasierten Sicherheitsanalyse Abschlussarbeit

2015.

Abstract | Links | BibTeX

Lipaczewski, Michael; Prosvirnova, Tatiana; Ortmeier, Frank; Rauzy, Antoine; Struck, Simon

Comparison of Modeling Formalisms for Safety Analyses: SAML and AltaRica Artikel

Reliability Engineering & System Safety, 2015.

Abstract | Links | BibTeX

Gonschorek, Tim

A Backward Model Checking Approach with Slicing Abschlussarbeit

Otto-von-Guericke-University Magdeburg, 2015.

Abstract | BibTeX

2014

Heumüller, Robert

VECS Dataflow - A SAML Language Extension Allowing Intuitive Creation of Formal Automata Specifications Abschlussarbeit

2014.

Links | BibTeX

Nykolaichuk, Mykhaylo; Lipaczewski, Michael; Liebusch, Tino; Ortmeier, Frank

On Efficiently Specifying Models for Model Checking Inproceedings

Proceedings of 4th International Symposium on Model Based Safety and Assessment (IMBSA 2014), 2014.

Abstract | Links | BibTeX

Heumüller, Robert; Lipaczewski, Michael; Ortmeier, Frank

A Dataflow Notation for SAML - Formal Modeling Without Fearing Timing Constraints Inproceedings

IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ., S. 43-50, 2014.

BibTeX

Lipaczewski, Michael; Filax, Marco; Ortmeier, Frank

Bringing VECS to the World - Challenges and Accomplishments in Teaching of Formal Model Analysis Inproceedings

European Conference on Software Engineering Education. - Herzogenrath : Shaker, S. 217-228, 2014.

Links | BibTeX

Filax, Marco; Gonschorek, Tim; Lipaczewski, Michael; Ortmeier, Frank

On Traceability of Informal Specifications for Model-Based Verification Inproceedings

IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment., S. 11-18, Magdeburg : Univ., 2014.

Abstract | Links | BibTeX

Gonschorek, Tim; Filax, Marco; Lipaczewski, Michael; Ortmeier, Frank

VECS - Verification Enviroment for Critical Systems - Tool Supported Formal Modeling an Verification Buchkapitel

IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ., S. 63-64, 2014.

Links | BibTeX

2013

Nielebock, Sebastian

Komposition gewöhnlicher Differentialgleichungen mit sicherheitsrelevanten Zustandsautomaten Abschlussarbeit

2013.

Links | BibTeX

Gonschorek, Tim

Methodik zur Abstraktion kontinuierlicher Differentialgleichungen Abschlussarbeit

Otto-von-Guericke-University Magdeburg, 2013.

Abstract | Links | BibTeX

Ortmeier, Frank; Struck, Simon; Güdemann, Matthias

Efficient Optimization of Large Probabilistic Models Artikel

Elsevier Journal of Systems and Software, 03/78 , 2013.

Abstract | Links | BibTeX

Ortmeier, Frank; Lipaczewski, Michael

Teaching and Training Formal Methods for Safety Critical Systems Konferenz

Proceedings of the 39th Euromicro Conference on Iv Software Engineering and Advanced Applications (SEAA 2013), 2013.

Abstract | Links | BibTeX

2012

Ortmeier, Frank; Struck, Simon; Lipaczewski, Michael

Using Model-Based Analysis in Certification of Critical Software-Intensive Systems Inproceedings

Softwareengineering 2012 Workshopband, 2012, ISBN: 978-3-88579-293-2.

Abstract | Links | BibTeX

Struck, Simon

Approaches to Multi-Objective Optimization of Formal Specifications Abschlussarbeit

2012.

Links | BibTeX

Nielebock, Sebastian; Ortmeier, Frank; Schumann, Marco; Winge, André

From Discrete Event Simulation to Virtual Reality Environments Inproceedings

Ortmeier, Frank; Daniel, Peter (Hrsg.): Computer Safety, Reliability, and Security, S. 508-516, Springer Berlin Heidelberg, 2012, ISBN: 978-3-642-33674-4.

Abstract | Links | BibTeX

Struck, Simon; Güdemann, Matthias; Lipaczewski, Michael; Ortmeier, Frank

Multi-Objective Optimization of Formal Specifications Konferenz

IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE 2012), 2012.

Abstract | Links | BibTeX

Lipaczewski, Michael; Struck, Simon; Ortmeier, Frank

SAML goes Eclipse - Combining Model-Based Safety Analysis and High-Level Editor Support Konferenz

Proceedings of the 2nd International Workshop on Developing Tools as Plug-Ins (TOPI), IEEE, 2012.

Abstract | Links | BibTeX

Lipaczewski, Michael; Struck, Simon; Ortmeier, Frank

Using Tool-Supported Model Based Safety Analysis - Progress and Experiences in SAML Development Konferenz

IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE 2012), 2012.

Abstract | Links | BibTeX

Güdemann, Matthias; Lipaczewski, Michael; Struck, Simon; Ortmeier, Frank

Unifying Probabilistic and Traditional Formal Model-Based Analysis Konferenz

Proceedings of 8. Dagstuhl-Workshop on Model-Based Development of Embedded Systems (MBEES), 2012.

Abstract | Links | BibTeX

2011

Güdemann, Matthias; Ortmeier, Frank

Model-Based Multi-Objective Safety Optimization Konferenz

Proceedings of the 30th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2011), 6894 , LNCS Springer, 2011, ISBN: 978-3642242694.

Abstract | Links | BibTeX

Güdemann, Matthias; Lipaczewski, Michael; Ortmeier, Frank

Tool Supported Model-Based Safety Analysis and Optimization Konferenz

Proceedings of the 17th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC 2011), 2011.

Abstract | Links | BibTeX

Ortmeier, Frank; Lipaczewski, Michael; Güdemann, Matthias

Practical Experiences in Model-Based Safety Analysis Konferenz

proceedings: International Workshop on Digital Engineering, ACM Proceedings, 2011.

Abstract | Links | BibTeX

Güdemann, Matthias

Qualitative and Quantitative Formal Model-Based Safety Analysis Promotionsarbeit

2011.

Links | BibTeX

checkAll