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. @inproceedings{10.1007/978-3-030-32872-6_7, title = {Integrating Safety Design Artifacts into System Development Models Using SafeDeML}, author = {Tim Gonschorek and Philipp Bergt and Marco Filax and Frank Ortmeier}, editor = {Yiannis Papadopoulos and Koorosh Aslansefat and Panagiotis Katsaros and Marco Bozzano}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2020/04/SafeDeML_gonschorekEtAl.pdfhttps://link.springer.com/chapter/10.1007/978-3-030-32872-6_7}, doi = {10.1007/978-3-030-32872-6_7}, isbn = {978-3-030-32872-6}, year = {2019}, date = {2019-09-18}, booktitle = {Model-Based Safety and Assessment}, pages = {93--106}, publisher = {Springer International Publishing}, address = {Cham}, abstract = {Applying a safety artifact language as Safety Design Modeling Language SafeDeML integrates the generation of the safety design into the system modeling stage -- directly within the system architecture. In this paper, we present a modeling process and a prototype for the CASE tool Enterprise Architect for SafeDeML. The goal is to support the system designer in developing a standard (in this paper Iso 26262) conform system and safety design containing all relevant safety artifact within one model. Such integration offers several modeling guarantees like consistency checks or computation of coverage and fault metrics. Since all relevant information and artifacts are contained within the model, SafeDeML and the prototype can help to decrease the effect of structural faults during the safety design and further supports the safety assessment. To give an idea to the reader of the complexity of the approach's application, we present an exemplary implementation of the safety design for a brake light system, a real case-study from the Iso 26262 context.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Applying a safety artifact language as Safety Design Modeling Language SafeDeML integrates the generation of the safety design into the system modeling stage -- directly within the system architecture. In this paper, we present a modeling process and a prototype for the CASE tool Enterprise Architect for SafeDeML. The goal is to support the system designer in developing a standard (in this paper Iso 26262) conform system and safety design containing all relevant safety artifact within one model. Such integration offers several modeling guarantees like consistency checks or computation of coverage and fault metrics. Since all relevant information and artifacts are contained within the model, SafeDeML and the prototype can help to decrease the effect of structural faults during the safety design and further supports the safety assessment. To give an idea to the reader of the complexity of the approach's application, we present an exemplary implementation of the safety design for a brake light system, a real case-study from the Iso 26262 context. |
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. @inproceedings{10.1007/978-3-030-26601-1_19, title = {SafeDeML: On Integrating the Safety Design into the System Model}, author = {Tim Gonschorek and Philipp Bergt and Marco Filax and Frank Ortmeier and Jan von Hoyningen-H\"{u}ne and Thorsten Piper}, editor = {Alexander Romanovsky and Elena Troubitsyna and Friedemann Bitsch}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2020/04/GonschorekEtAl_SafeDeML.pdfhttps://link.springer.com/chapter/10.1007/978-3-030-26601-1_19}, doi = {10.1007/978-3-030-26601-1_19}, isbn = {978-3-030-26601-1}, year = {2019}, date = {2019-09-18}, booktitle = {Computer Safety, Reliability, and Security}, pages = {271--285}, publisher = {Springer International Publishing}, address = {Cham}, abstract = {The safety design definition of a safety critical system is a complex task. On the one hand, the system designer must ensure that he addressed all potentially hazardous harwdware faults. This is often defined not(!) in the model but within extra documents (e.g., Excel sheets). On the other hand, all defined safety mechanisms must be transformed back into the system model. We think an improvement for the designer would be given by a modeling extension integrating relevant safety design artifacts into the normal design work-flow and supporting the safety design development directly from within the model.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The safety design definition of a safety critical system is a complex task. On the one hand, the system designer must ensure that he addressed all potentially hazardous harwdware faults. This is often defined not(!) in the model but within extra documents (e.g., Excel sheets). On the other hand, all defined safety mechanisms must be transformed back into the system model. We think an improvement for the designer would be given by a modeling extension integrating relevant safety design artifacts into the normal design work-flow and supporting the safety design development directly from within the model. |
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. @inproceedings{Gonschorek2018b, title = {Fault Trees vs. Component Fault Trees: An Empirical Study}, author = {Tim Gonschorek and Marc Zeller and Frank Ortmeier and Kai H\"{o}fig}, editor = {Gallina B., Skavhaug A., Schoitsch E., Bitsch F. }, doi = {https://doi.org/10.1007/978-3-319-99229-7_21}, isbn = {978-3-319-99228-0}, year = {2018}, date = {2018-08-21}, booktitle = { Computer Safety, Reliability, and Security. SAFECOMP 2018.}, volume = {11094}, publisher = {Springer, Cham}, series = {Lecture Notes in Computer Science}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
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. @inproceedings{Schillreff2018, title = { Learning-based Kinematic Calibration using Adjoint Error Model }, author = {Nadia Schillreff and Frank Ortmeier}, editor = {SciTePress}, doi = {10.5220/0006870403820389}, isbn = {978-989-758-321-6}, year = {2018}, date = {2018-08-01}, booktitle = {Proceedings of the 15th International Conference on Informatics in Control, Automation and Robotics - Volume 2: ICINCO}, abstract = {A learning-based robot kinematic calibration approach based on the product-of-exponentials (POE) formula and Adjoint error model is introduced. To ensure high accuracy this approach combines the geometrical and non-geometrical influences like for e.g. elastic deformations without explicitly defining all physical processes that contribute to them using a polynomial regression method. By using the POE formula for kinematic modeling of the manipulator it is ensured that kinematic parameters vary smoothly and used method is robust and singularity-free. The introduced error parameters are presented in the form of Adjoint transformations on nominal joint twists. The calibration process then becomes finding a set of polynomial functions using regression methods that are able to reflect the actual kinematics of the robot. The proposed method is evaluated on a dataset obtained using a 7-DOF manipulator (KUKA LBR iiwa 7 R800). The experimental results show that this approach significantly reduc es positional errors of the robotic manipulator after calibration.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } A learning-based robot kinematic calibration approach based on the product-of-exponentials (POE) formula and Adjoint error model is introduced. To ensure high accuracy this approach combines the geometrical and non-geometrical influences like for e.g. elastic deformations without explicitly defining all physical processes that contribute to them using a polynomial regression method. By using the POE formula for kinematic modeling of the manipulator it is ensured that kinematic parameters vary smoothly and used method is robust and singularity-free. The introduced error parameters are presented in the form of Adjoint transformations on nominal joint twists. The calibration process then becomes finding a set of polynomial functions using regression methods that are able to reflect the actual kinematics of the robot. The proposed method is evaluated on a dataset obtained using a 7-DOF manipulator (KUKA LBR iiwa 7 R800). The experimental results show that this approach significantly reduc es positional errors of the robotic manipulator after calibration. |
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. @inproceedings{Gonschorek2018, title = {Automatic Model-based Verification of Railway Interlocking Systems using Model Checking}, author = {Tim Gonschorek and Ludwig Bedau and Frank Ortmeier}, editor = {Stein Haugen}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2018/02/Esrel2018_GonschorekEtAl_ModelCheckingRailMLInterlockings.pdf}, year = {2018}, date = {2018-06-17}, booktitle = {Proceedings of ESREL 2018}, pages = {741-748}, publisher = {CRC Press}, address = {London}, abstract = {The theoretic foundations for formally verifying railway interlocking systems have already been studied extensively. There exist a lot of work covering the application of methodologies like model checking in this context. However, some design faults still remain undetected until final on-track evaluation of the system. This is strongly related to missing automation solutions for real-world models and standards as well as the high theoretical expertise required. There exist many well-developed tools each requiring different modeling formalisms and focusing on a different question/scenario. Without specific experience in formal system modeling, it is extremely complicated to model such complex systems. In this paper, we present a methodology for the automatic model generation and verification of railway interlockings in a tool-independent(!) way. Therefore, we define a generic template set of atomic track elements and safety properties in a formal modeling language applicable with precise semantics. This generic template enables us to verify the structure of any given track layout. The already existing tool support of VECS allows to automatically translate these specifications into various model checkers for verification. More important, we present a robust transformation of the upcoming data exchange format for railway interlocking systems railML into the presented specification template. As a consequence, this approach really may help to bridge the gap between formal methods and system design in railway interlockings. We evaluate this approach on a real-world case studies train station of Brain l'Alleud. We also show the tool-independent modeling by automatically translating the specification to different verification engines and compare their performance.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The theoretic foundations for formally verifying railway interlocking systems have already been studied extensively. There exist a lot of work covering the application of methodologies like model checking in this context. However, some design faults still remain undetected until final on-track evaluation of the system. This is strongly related to missing automation solutions for real-world models and standards as well as the high theoretical expertise required. There exist many well-developed tools each requiring different modeling formalisms and focusing on a different question/scenario. Without specific experience in formal system modeling, it is extremely complicated to model such complex systems. In this paper, we present a methodology for the automatic model generation and verification of railway interlockings in a tool-independent(!) way. Therefore, we define a generic template set of atomic track elements and safety properties in a formal modeling language applicable with precise semantics. This generic template enables us to verify the structure of any given track layout. The already existing tool support of VECS allows to automatically translate these specifications into various model checkers for verification. More important, we present a robust transformation of the upcoming data exchange format for railway interlocking systems railML into the presented specification template. As a consequence, this approach really may help to bridge the gap between formal methods and system design in railway interlockings. We evaluate this approach on a real-world case studies train station of Brain l'Alleud. We also show the tool-independent modeling by automatically translating the specification to different verification engines and compare their performance. |
Schott, Kevin Michael Extraktion relevanter API-spezifischer Informationen zur automatischen Korrektur von Softwarefehlern Abschlussarbeit Otto-von-Guericke-Unviersität Magdeburg, 2018. @mastersthesis{SchottExtractionBA2018, title = {Extraktion relevanter API-spezifischer Informationen zur automatischen Korrektur von Softwarefehlern}, author = {Kevin Michael Schott}, editor = {Sebastian Nielebock and Frank Ortmeier}, year = {2018}, date = {2018-03-13}, school = {Otto-von-Guericke-Unviersit\"{a}t Magdeburg}, abstract = {Bekanntlich ist Softwareentwicklung nicht fehlerfrei. W\"{a}hrend der Fokus auf der Entwicklung neuer Komponenten liegen sollte, geht viel Zeit in die Behebung existierender Programmfehler verloren. Jene Programmfehler, welche das Softwaresystem in einen regressiven Zustand versetzen - sodass dieses nicht mehr ordnungsgem\"{a}\ss funktioniert - sind oftmals m\"{u}hselig zu beheben. Dadurch ist der zust\"{a}ndige Programmierer meist auf unbestimmte Zeit verpflichtet, diesen zu beheben, wodurch er dem Unternehmen nicht f\"{u}r die Weiterentwicklung zur Verf\"{u}gung steht. Dieser zeitliche Engpass kann monet\"{a}re R\"{u}ckschl\"{a}ge bedeuten, insbesondere wenn es sich um eine sicherheitskritische L\"{u}cke im Softwaresystem handelt. Die Dom\"{a}ne der automatischen Fehlerkorrektur will solchen Problemen entgegenwirken, indem versucht wird, ein Ansatz zu finden, der den entstandenen Fehler automatisch beheben kann oder dem Programmierer wenigstens einen L\"{o}sungsvorschlag liefert. Heutzutage ist der Umgang mit Application-Programming-Interfaces (kurz APIs) beinahe allt\"{a}glich f\"{u}r jeden Programmierer, was einen Ansatz zur automatischen Korrektur von Softwarefehlern schwer bis gar nicht generalisieren l\"{a}sst. Deren Dokumentation ist oft nicht hinreichend oder unverst\"{a}ndlich. Dadurch wird die API falsch benutzt, sodass unter anderem Methodenaufrufe vergessen oder in falscher Reihenfolge verwendet werden. J\"{u}ngste Studien zeigen zudem, dass bei circa jeder zweiten Fehlerbehebung mindestens eine API-spezifische \"{A}nderung vorgenommen werden muss, um den Fehler ganzheitlich zu beheben. Herk\"{o}mmliche Ans\"{a}tze zur automatischen Korrektur von Softwarefehlern k\"{o}nnen aufgrund ihrer generischen Natur diese Programmfehler oftmals nicht vollst\"{a}ndig beheben und m\"{u}ssen erweitert werden. Im Rahmen dieser Arbeit wird ein Konzept vorgestellt, mit dessen Hilfe diese Programmfehler m\"{o}glicherweise korrigiert werden k\"{o}nnen. Prim\"{a}r wird jedoch erforscht, welche Informationen aus einem API-spezifischen Kontext extrahiert und verarbeitet werden m\"{u}ssen, um eine Korrektur vornehmen zu k\"{o}nnen. Daf\"{u}r wird ein Prototyp entwickelt, der diese Informationsextraktion \"{u}bernimmt und \"{a}hnlichen Quellcode herunterl\"{a}dt, sodass in diesem potenziell eine richtige Benutzung der gesuchten API enthalten ist, welche als Korrektur des Fehlers dienen soll.}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } Bekanntlich ist Softwareentwicklung nicht fehlerfrei. Während der Fokus auf der Entwicklung neuer Komponenten liegen sollte, geht viel Zeit in die Behebung existierender Programmfehler verloren. Jene Programmfehler, welche das Softwaresystem in einen regressiven Zustand versetzen - sodass dieses nicht mehr ordnungsgemäß funktioniert - sind oftmals mühselig zu beheben. Dadurch ist der zuständige Programmierer meist auf unbestimmte Zeit verpflichtet, diesen zu beheben, wodurch er dem Unternehmen nicht für die Weiterentwicklung zur Verfügung steht. Dieser zeitliche Engpass kann monetäre Rückschläge bedeuten, insbesondere wenn es sich um eine sicherheitskritische Lücke im Softwaresystem handelt. Die Domäne der automatischen Fehlerkorrektur will solchen Problemen entgegenwirken, indem versucht wird, ein Ansatz zu finden, der den entstandenen Fehler automatisch beheben kann oder dem Programmierer wenigstens einen Lösungsvorschlag liefert. Heutzutage ist der Umgang mit Application-Programming-Interfaces (kurz APIs) beinahe alltäglich für jeden Programmierer, was einen Ansatz zur automatischen Korrektur von Softwarefehlern schwer bis gar nicht generalisieren lässt. Deren Dokumentation ist oft nicht hinreichend oder unverständlich. Dadurch wird die API falsch benutzt, sodass unter anderem Methodenaufrufe vergessen oder in falscher Reihenfolge verwendet werden. Jüngste Studien zeigen zudem, dass bei circa jeder zweiten Fehlerbehebung mindestens eine API-spezifische Änderung vorgenommen werden muss, um den Fehler ganzheitlich zu beheben. Herkömmliche Ansätze zur automatischen Korrektur von Softwarefehlern können aufgrund ihrer generischen Natur diese Programmfehler oftmals nicht vollständig beheben und müssen erweitert werden. Im Rahmen dieser Arbeit wird ein Konzept vorgestellt, mit dessen Hilfe diese Programmfehler möglicherweise korrigiert werden können. Primär wird jedoch erforscht, welche Informationen aus einem API-spezifischen Kontext extrahiert und verarbeitet werden müssen, um eine Korrektur vornehmen zu können. Dafür wird ein Prototyp entwickelt, der diese Informationsextraktion übernimmt und ähnlichen Quellcode herunterlädt, sodass in diesem potenziell eine richtige Benutzung der gesuchten API enthalten ist, welche als Korrektur des Fehlers dienen soll. |
Bedau, Ludwig; Gonschorek, Tim; Ortmeier, Frank Sicherheitsanalyse eines Bahnhofstellwerkes Konferenzbericht Horber Schienen Tage 35 , 2018. @proceedings{Bedau2018, title = {Sicherheitsanalyse eines Bahnhofstellwerkes}, author = {Ludwig Bedau and Tim Gonschorek and Frank Ortmeier}, editor = {Andreas Brock and Christina Brock and Rudolf Barth}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2018/02/BedauEtAl_HST17.pdf}, year = {2018}, date = {2018-02-28}, volume = {35}, organization = {Horber Schienen Tage}, keywords = {}, pubstate = {published}, tppubtype = {proceedings} } |
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. @inproceedings{Gonschorek2017, title = {On Improving Rare Event Simulation for Probabilistic Safety Analysis}, author = {Tim Gonschorek and Ben Lukas Rabeler and Frank Ortmeier and Dirk Schomburg}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/GonschorekEtAl_OnImprovingRareEventSimulationForProbabilisticSafetyAnalysis_memocode17.pdfhttps://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/GonschorekEtAl_OnImprovingRareEventSimulationForProbabilisticSafetyAnalysis_memocode17.pdf}, doi = {10.1145/3127041.3127057}, isbn = {978-1-4503-5093-8}, year = {2017}, date = {2017-09-29}, booktitle = {Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design}, pages = {15-24}, publisher = {ACM New York, NY, USA ©2017 }, series = {Lecture Notes in Computer Science}, abstract = {This paper presents a new approach for generating probability distributions for Monte Carlo based stochastic model checking. Stochastic approaches are used for quantitative analysis of safety critical systems if numerical model checking tools get overwhelmed by the complexity of the models and the exploding state space. However, sample based stochastic measures get problems when the estimated event is very unlikely (e.g. 10-6 and below). Therefore, rare event techniques, like importance sampling, increase the likelihood of samples representing model executions which depict the desired rare event, e.g., a path leading into a hazardous state. The presented approach uses qualitative counter examples to derive appropriate distributions for the sampling, i.e., a distribution that increases the likelihood of the examined rare event and decreases the variance Therefore, we define the sampling distribution such that transitions included in the counter example become more likely. For keeping the variance small, the new distributions is calculated within an optimization problem which minimizes the variance on the counter example paths by calculating new probability distributions for the related transitions. We have evaluated this approach in four different real-world case studies and compare it to other leading stochastic and numeric model checking tools. It turned out that in the case of rare event properties, the proposed approach outperforms other techniques in run time and, slightly more important, in the accuracy of the estimation result. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } This paper presents a new approach for generating probability distributions for Monte Carlo based stochastic model checking. Stochastic approaches are used for quantitative analysis of safety critical systems if numerical model checking tools get overwhelmed by the complexity of the models and the exploding state space. However, sample based stochastic measures get problems when the estimated event is very unlikely (e.g. 10-6 and below). Therefore, rare event techniques, like importance sampling, increase the likelihood of samples representing model executions which depict the desired rare event, e.g., a path leading into a hazardous state. The presented approach uses qualitative counter examples to derive appropriate distributions for the sampling, i.e., a distribution that increases the likelihood of the examined rare event and decreases the variance Therefore, we define the sampling distribution such that transitions included in the counter example become more likely. For keeping the variance small, the new distributions is calculated within an optimization problem which minimizes the variance on the counter example paths by calculating new probability distributions for the related transitions. We have evaluated this approach in four different real-world case studies and compare it to other leading stochastic and numeric model checking tools. It turned out that in the case of rare event properties, the proposed approach outperforms other techniques in run time and, slightly more important, in the accuracy of the estimation result. |
Gonschorek, Tim; Filax, Marco; Ortmeier, Frank Invited Paper: 5th International Symposium on Model-Based Safety and Assessment (IMBSA 2017), 2017. @misc{Gonschorek2017b, title = {A Verification Environment for Critical Systems: Integrating Formal Methods into the Safety Development Life-cycle}, author = {Tim Gonschorek and Marco Filax and Frank Ortmeier}, editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/GonschorekEtAl_-VECS_imbsa17_poster.pdf https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/GonschorekEtAl_-VECS_imbsa17_poster.pdf}, year = {2017}, date = {2017-09-11}, howpublished = {Invited Paper: 5th International Symposium on Model-Based Safety and Assessment (IMBSA 2017)}, keywords = {}, pubstate = {published}, tppubtype = {misc} } |
Bitsch, Friedemann; Filax, Marco; Gonschorek, Tim; Ortmeier, Frank; Schumacher, Rolf Effiziente Sicherheitsnachweisführung mithilfe modellbasierter Systemanalyse Artikel Signal + Draht, 2017. @article{Bitsch2017, title = {Effiziente Sicherheitsnachweisf\"{u}hrung mithilfe modellbasierter Systemanalyse}, author = {Friedemann Bitsch and Marco Filax and Tim Gonschorek and Frank Ortmeier and Rolf Schumacher}, editor = {DVV Media Group}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/2017_BitschEtAl_EffizienteSicherheitsnachweisf\"{u}hrung.pdf}, year = {2017}, date = {2017-06-01}, journal = {Signal + Draht}, abstract = {This paper introduces a model-based computer-aided methodology for safety analyses in development and as- sessment processes for signalling and train control systems. The objective is to realise the application of model-based for- mal methods and simultaneously to reduce the outlay for us- ing them to a degree acceptable in industrial practice. Instead of performing safety analyses in parallel with the develop- ment process, existing system analyses and design models are used for deriving the necessary safety analyses models as au- tomatically as possible. Therefore, statements on safety and correctness can already be calculated in early development phases with precise results. Those early statements are deci- sive, because they make it possible to adapt and correct the system design at an early stage and to do it cost-efficiently.}, keywords = {}, pubstate = {published}, tppubtype = {article} } This paper introduces a model-based computer-aided methodology for safety analyses in development and as- sessment processes for signalling and train control systems. The objective is to realise the application of model-based for- mal methods and simultaneously to reduce the outlay for us- ing them to a degree acceptable in industrial practice. Instead of performing safety analyses in parallel with the develop- ment process, existing system analyses and design models are used for deriving the necessary safety analyses models as au- tomatically as possible. Therefore, statements on safety and correctness can already be calculated in early development phases with precise results. Those early statements are deci- sive, because they make it possible to adapt and correct the system design at an early stage and to do it cost-efficiently. |
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. @inproceedings{spl-in-cps-splc-vision-2017, title = {Beyond Software Product Lines: Variability Modeling in Cyber-Physical Systems}, author = {Jacob Kr\"{u}ger and Sebastian Nielebock and Sebastian Krieter and Christian Diedrich and Thomas Leich and Gunter Saake and Sebastian Zug and Frank Ortmeier}, url = {https://dl.acm.org/citation.cfm?id=3106217}, year = {2017}, date = {2017-05-11}, booktitle = {Proceedings of the 21st International Systems and Software Product Line Conference (SPLC 2017) - Vision Track}, journal = {21st International Systems and Software Product Line Conference (SPLC 2017) - Vision Track}, pages = {237-241}, abstract = {Smart IT has an increasing influence on the control of daily life. For instance, smart grids manage power supply, autonomous automobiles take part in traffic, and assistive robotics support humans in production cells. We denote such systems as Cyber-physical Systems (CPSs), where cyber addresses the controlling software, while physical describes the controlled hardware. One key aspect of CPSs is their capability to adapt to new situations autonomously or with minimal human intervention. To achieve this, CPSs reuse, reorganize and reconfigure their components during runtime. Some components may even serve in different CPSs and different situations simultaneously. The hardware of a CPS usually consists of a heterogeneous set of variable components. While each component can be designed as a software product line (SPL), which is a well established approach to describe software and hardware variability, it is not possible to describe CPSs' variability solely on a set of separate, non-interacting product lines. To properly manage variability, a CPS must specify dependencies and interactions of its separate components and cope with variable environments, changing requirements, and differing safety properties. In this paper, we i) propose a classification of variability aspects, ii) point out current challenges in variability modeling, and iii) sketch open research questions. Overall, we aim to initiate new research directions for variable CPSs based on existing product-line techniques.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Smart IT has an increasing influence on the control of daily life. For instance, smart grids manage power supply, autonomous automobiles take part in traffic, and assistive robotics support humans in production cells. We denote such systems as Cyber-physical Systems (CPSs), where cyber addresses the controlling software, while physical describes the controlled hardware. One key aspect of CPSs is their capability to adapt to new situations autonomously or with minimal human intervention. To achieve this, CPSs reuse, reorganize and reconfigure their components during runtime. Some components may even serve in different CPSs and different situations simultaneously. The hardware of a CPS usually consists of a heterogeneous set of variable components. While each component can be designed as a software product line (SPL), which is a well established approach to describe software and hardware variability, it is not possible to describe CPSs' variability solely on a set of separate, non-interacting product lines. To properly manage variability, a CPS must specify dependencies and interactions of its separate components and cope with variable environments, changing requirements, and differing safety properties. In this paper, we i) propose a classification of variability aspects, ii) point out current challenges in variability modeling, and iii) sketch open research questions. Overall, we aim to initiate new research directions for variable CPSs based on existing product-line techniques. |
Bedau, Ludwig Modellbasierte Sicherheitsanalyse eines Bahnhofsstellwerks Abschlussarbeit Otto-von-Guericke-Universität Magdeburg, 2017. @mastersthesis{Bedau2017, title = {Modellbasierte Sicherheitsanalyse eines Bahnhofsstellwerks}, author = {Ludwig Bedau}, editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2018/02/BA_2017_BedauLudwig.pdf}, year = {2017}, date = {2017-03-31}, school = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, abstract = {Stellwerke stellen eine zentrale Komponente fu¨r den sicheren Schienenverkehr dar. Um die korrekte Funktionsweise sicherzustellen und sicherheitskritische Zust¨ande auszuschlie\ssen, sind formale Methoden angebracht. In dieser Arbeit soll gezeigt werden, wie in der Modellierungssprache SAML (Sys-tem Analaysis and Modeling Language) ein Baukastensystem erstellt wird, mit dem sich beliebige Stellwerke modellieren lassen. In Rahmen der Arbeit wird beschrie-ben, wie das reale System abstrahiert wurde, um das zu untersuchende Verhal-ten herauszustellen. Die Arbeit beschreibt weiterhin die Sicherheits- und Liveness-Spezifikationen, die zur Verifikation der generierten Bahnhofsstellwerke genutz wer-den. Im Anschluss wird an einem Beispiel die Modellierung eines Bahnhofsstellwerkes auf Basis des vorgestellten Baukastensystems gezeigt. Bei der Verifikation wurde ei-ne kleine Auswahl an Model-Checking-Tools genutzt. Ein Vergleich dieser Tools in Bezug auf das hier gestellte Problem sowie eine Auswertung der Erfahrungen, die w¨ahrend des Projektes gesammelt werden konnten, sollen den Abschluss bilden.}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } Stellwerke stellen eine zentrale Komponente fu¨r den sicheren Schienenverkehr dar. Um die korrekte Funktionsweise sicherzustellen und sicherheitskritische Zust¨ande auszuschließen, sind formale Methoden angebracht. In dieser Arbeit soll gezeigt werden, wie in der Modellierungssprache SAML (Sys-tem Analaysis and Modeling Language) ein Baukastensystem erstellt wird, mit dem sich beliebige Stellwerke modellieren lassen. In Rahmen der Arbeit wird beschrie-ben, wie das reale System abstrahiert wurde, um das zu untersuchende Verhal-ten herauszustellen. Die Arbeit beschreibt weiterhin die Sicherheits- und Liveness-Spezifikationen, die zur Verifikation der generierten Bahnhofsstellwerke genutz wer-den. Im Anschluss wird an einem Beispiel die Modellierung eines Bahnhofsstellwerkes auf Basis des vorgestellten Baukastensystems gezeigt. Bei der Verifikation wurde ei-ne kleine Auswahl an Model-Checking-Tools genutzt. Ein Vergleich dieser Tools in Bezug auf das hier gestellte Problem sowie eine Auswertung der Erfahrungen, die w¨ahrend des Projektes gesammelt werden konnten, sollen den Abschluss bilden. |
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. @inproceedings{MF16-RSSR, title = {Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models}, author = {Marco Filax and Tim Gonschorek and Frank Ortmeier }, editor = {Springer International Publishing }, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/RSSR_CorrectFormalizationOfRequirementSpecifications.pdf}, doi = {10.1007/978-3-319-33951-1_8}, isbn = {978-3-319-33951-1}, year = {2016}, date = {2016-06-15}, booktitle = {Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings}, pages = {106 - 122}, abstract = {In recent years, formal methods have become an important approach to ensure the correct function of complex hardware and software systems. Many standards for safety critical systems recommend or even require the use of formal methods. However, building a formal model for a given specification is challenging. This is, because verification results must be considered with respect to the validity of the model. This leads to the question: “Did I build the right model?”. For system development the analogous question “Did I build the right system?”. This is often answered with requirements traceability through the whole development cycle. For formal verification this question often remains unanswered. The standard model, which is used in development of safety critical applications is the V-model. The core idea is to define tests for each phase during system development. In this paper, we propose an approach - analogously to the V-model for development - which ensures correctness of the formal model with respect to requirements. We will illustrate the approach on a small example from the railways domain.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } In recent years, formal methods have become an important approach to ensure the correct function of complex hardware and software systems. Many standards for safety critical systems recommend or even require the use of formal methods. However, building a formal model for a given specification is challenging. This is, because verification results must be considered with respect to the validity of the model. This leads to the question: “Did I build the right model?”. For system development the analogous question “Did I build the right system?”. This is often answered with requirements traceability through the whole development cycle. For formal verification this question often remains unanswered. The standard model, which is used in development of safety critical applications is the V-model. The core idea is to define tests for each phase during system development. In this paper, we propose an approach - analogously to the V-model for development - which ensures correctness of the formal model with respect to requirements. We will illustrate the approach on a small example from the railways domain. |
Filax, Marco; Gonschorek, Tim; Hebecker, Tanja; Lipaczewski, Michael; Madalinski, Agnes; Ortmeier, Frank; Fietze, Mario; Schumacher, Rolf Der Eisenbahn Ingenieur, S. 24 -27, 2016. @article{ei2016, title = {Bringing formal methods “on the rail” - Modellbasierte Systemanalyse in der Sicherheitsnachweisf\"{u}hrung}, author = {Marco Filax and Tim Gonschorek and Tanja Hebecker and Michael Lipaczewski and Agnes Madalinski and Frank Ortmeier and Mario Fietze and Rolf Schumacher}, editor = {Verband Deutscher Eisenbahn-Ingenieure E.V.}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/Ver\"{o}ffentlichung-Eisenbahningeneur.pdf}, year = {2016}, date = {2016-01-01}, journal = {Der Eisenbahn Ingenieur}, pages = {24 -27}, abstract = {Funktionen sicherheitskritischer Systeme im Eisenbahnsektor werden entsprechend ihrer tolerierbaren Gef\"{a}hrdungsraten in sogenannte Sicherheitsintegrit\"{a}tslevel (SIL 1-4) eingestuft. In der europ\"{a}ischen Norm EN50129 besteht, f\"{u}r die Stufen drei und vier, die dringende Empfehlung, im Entwicklungs- und Spezifikationsprozess, formale Methoden anzuwenden. Die Otto-von-Guericke-Universit\"{a}t Magdeburg hat dazu, begleitet durch das Eisenbahn-Bundesamt (EBA) und Gutachtern des EBA, einen Satz unterst\"{u}tzender Werkzeuge und Verfahren entwickelt, welche in diesem Artikel, am Beispiel der Punktf\"{o}rmigen Zugbeeinflussung (PZB), vorgestellt werden sollen. Diese Werkzeuge erm\"{o}glichen die Portierung einer nat\"{u}rlichsprachlichen Systemanforderungsspezifikation in ein formales Modell, mit dessen Hilfe die Konsistenz und Vollst\"{a}ndigkeit der Systembeschreibung, sowie die definierten Sicherheitsanforderungen formal \"{u}berpr\"{u}ft werden k\"{o}nnen. Bereits in fr\"{u}hen Entwicklungsphasen k\"{o}nnen automatisiert qualitative und quantitative Absch\"{a}tzungen \"{u}ber die Sicherheit und Zuverl\"{a}ssigkeit mit pr\"{a}zisen und aussagekr\"{a}ftigen Resultaten berechnet werden. Gleichzeitig wird der Aufwand zur endg\"{u}ltigen, sicherheitstechnischen Bewertung durch vollst\"{a}ndige Traceability als Teil des Zertifizierungs- und Zulassungsprozesses reduziert.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Funktionen sicherheitskritischer Systeme im Eisenbahnsektor werden entsprechend ihrer tolerierbaren Gefährdungsraten in sogenannte Sicherheitsintegritätslevel (SIL 1-4) eingestuft. In der europäischen Norm EN50129 besteht, für die Stufen drei und vier, die dringende Empfehlung, im Entwicklungs- und Spezifikationsprozess, formale Methoden anzuwenden. Die Otto-von-Guericke-Universität Magdeburg hat dazu, begleitet durch das Eisenbahn-Bundesamt (EBA) und Gutachtern des EBA, einen Satz unterstützender Werkzeuge und Verfahren entwickelt, welche in diesem Artikel, am Beispiel der Punktförmigen Zugbeeinflussung (PZB), vorgestellt werden sollen. Diese Werkzeuge ermöglichen die Portierung einer natürlichsprachlichen Systemanforderungsspezifikation in ein formales Modell, mit dessen Hilfe die Konsistenz und Vollständigkeit der Systembeschreibung, sowie die definierten Sicherheitsanforderungen formal überprüft werden können. Bereits in frühen Entwicklungsphasen können automatisiert qualitative und quantitative Abschätzungen über die Sicherheit und Zuverlässigkeit mit präzisen und aussagekräftigen Resultaten berechnet werden. Gleichzeitig wird der Aufwand zur endgültigen, sicherheitstechnischen Bewertung durch vollständige Traceability als Teil des Zertifizierungs- und Zulassungsprozesses reduziert. |
2015 |
Hamannn, Dominik Kopplung formaler Modelle mit realweltlichen Umgebungsmodellen Abschlussarbeit Otto-von-Guericke-Universität Magdeburg, 2015. @mastersthesis{BAHamann2015, title = {Kopplung formaler Modelle mit realweltlichen Umgebungsmodellen}, author = {Dominik Hamannn}, editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/12/BAHamann2015.pdf}, year = {2015}, date = {2015-12-14}, address = {Universit\"{a}tsplatz 2, 39106 Magdeburg}, school = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, abstract = {Sicherheitskritische technische Systeme werden insbesondere in der Automobilindustrie und der Luftfahrt immer komplexer. Ein Ansatz, um die Sicherheit solcher Systeme zu \"{u}berpr\"{u}fen, besteht darin, ein Modell des Systems zu erstellen und dieses von einem Model Checker auf gef\"{a}hrdende Situationen zu \"{u}berpr\"{u}fen. Die Umgebung eines softwareintensiven Systems muss oft, aufgrund der Funktionsweise von Model Checkern und aufgrund von Restriktionen der verwendeten Sprache, mit einem hohen Abstraktionsgrad modelliert werden. Das betrif t insbesondere Systeme, die nicht nur rein logische Aufgaben ausf\"{u}hren, sondern mittels Sensorik und Aktorik mit der realen Welt interagieren. Herrscht eine zu gro\sse Diskrepanz zwischen der realen Umgebung und dem Modell der Umgebung, tritt in dem Modell Fehlverhalten nicht auf, dass in der realen Welt auftreten w\"{u}rde. Die Ergebnisse eines Model Checkers sind dann f\"{u}r dieses Modell nicht aussagekr\"{a}ftig. In dieser Arbeit wird eine Schnittstelle vorgestellt, mit der formale Modelle mit realweltlichen Umgebungsmodellen gekoppelt werden k\"{o}nnen. Dadurch wird getestet, inwiefern sich das Verhalten des formalen Modells in einer realistischen Umgebung von dem Verhalten einer abstrahierten Umgebung unterscheidet. Dieser Vergleich kann Aufschluss \"{u}ber die Validit\"{a}t des verwendeten Umgebungsmodells bringen.}, howpublished = {Bachelorarbeit}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } Sicherheitskritische technische Systeme werden insbesondere in der Automobilindustrie und der Luftfahrt immer komplexer. Ein Ansatz, um die Sicherheit solcher Systeme zu überprüfen, besteht darin, ein Modell des Systems zu erstellen und dieses von einem Model Checker auf gefährdende Situationen zu überprüfen. Die Umgebung eines softwareintensiven Systems muss oft, aufgrund der Funktionsweise von Model Checkern und aufgrund von Restriktionen der verwendeten Sprache, mit einem hohen Abstraktionsgrad modelliert werden. Das betrif t insbesondere Systeme, die nicht nur rein logische Aufgaben ausführen, sondern mittels Sensorik und Aktorik mit der realen Welt interagieren. Herrscht eine zu große Diskrepanz zwischen der realen Umgebung und dem Modell der Umgebung, tritt in dem Modell Fehlverhalten nicht auf, dass in der realen Welt auftreten würde. Die Ergebnisse eines Model Checkers sind dann für dieses Modell nicht aussagekräftig. In dieser Arbeit wird eine Schnittstelle vorgestellt, mit der formale Modelle mit realweltlichen Umgebungsmodellen gekoppelt werden können. Dadurch wird getestet, inwiefern sich das Verhalten des formalen Modells in einer realistischen Umgebung von dem Verhalten einer abstrahierten Umgebung unterscheidet. Dieser Vergleich kann Aufschluss über die Validität des verwendeten Umgebungsmodells bringen. |
Heumüller, Robert Multi-Abstraction Model Based Software Development for Embedded Low-Cost Applications Abschlussarbeit 2015. @mastersthesis{Heum\"{u}ller2015, title = {Multi-Abstraction Model Based Software Development for Embedded Low-Cost Applications}, author = {Robert Heum\"{u}ller}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/01/thesis-1.pdf}, year = {2015}, date = {2015-11-06}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } |
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). @inproceedings{Gonschorek2015DCDS, title = {Slice or Unfold - Experiments on Checking Synchronous Models with Backwards Slicing}, author = {Tim Gonschorek and Frank Ortmeier}, editor = {International Federation of Automatic Control}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/paper_bwmc_dcds15.pdf}, year = {2015}, date = {2015-05-31}, booktitle = {5th International Workshop on Dependable Control of Discrete Systems (DCDS 2015)}, abstract = {Nowadays, model checking approaches have one major drawback: They suffer from the state space explosion problem. We think one major problem is that the verification tools always must hold some (symbolic) representation, e.g. a BDD or a adjacency list, in the memory during the verification process. In this paper we propose a verification approach that does not need to hold a complete representation while checking the model. This is done by slicing backward the transition rules, which defines the complete state system.%144 Here, we present the basic backward slicing approach for verifying CTL safety properties traversing the state machine by using a given transition model. In the following , we give a little evaluation with special test models and compare the results to the state of the art model checker nuXmv.}, note = {accepted, will be published this year}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Nowadays, model checking approaches have one major drawback: They suffer from the state space explosion problem. We think one major problem is that the verification tools always must hold some (symbolic) representation, e.g. a BDD or a adjacency list, in the memory during the verification process. In this paper we propose a verification approach that does not need to hold a complete representation while checking the model. This is done by slicing backward the transition rules, which defines the complete state system.%144 Here, we present the basic backward slicing approach for verifying CTL safety properties traversing the state machine by using a given transition model. In the following , we give a little evaluation with special test models and compare the results to the state of the art model checker nuXmv. |
Rabeler, Ben Abstraktion kontinuierlichen Verhaltens zur modellbasierten Sicherheitsanalyse Abschlussarbeit 2015. @mastersthesis{BARabeler2015, title = {Abstraktion kontinuierlichen Verhaltens zur modellbasierten Sicherheitsanalyse}, author = {Ben Rabeler}, editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/06/ba_thesis_rabeler.pdf}, year = {2015}, date = {2015-05-18}, abstract = {Die Sicherheit von technischen System ist in vielen Gebieten wie der Luftfahrt oder im Stra\ssenverkehr von elementarer Bedeutung f\"{u}r die Hersteller solcher Systeme wie f\"{u}r die Anwender. Ein Ansatz um die Sicherheit von diskreten Systemen zu zeigen, besteht darin, diese in einem diskreten Modell zu abstrahieren und anschlie\ssend mit einem Model Checker auf gef\"{a}hrdende Situationen zu \"{u}berpr\"{u}fen. Viele Szenarien in den Anwendungsbereichen wie der Luftfahrt oder dem Stra\ssenverkehr beruhen jedoch auf kontinuierlichem Systemverhalten. In dieser Arbeit wird ein Verfahren vorgestellt, das ein kontinuierliches System in diskrete Automaten abstrahiert, sodass diese Automaten mit einem symbolischen Model Checker auf eine Sicherheitsspezifi kation \"{u}berpr\"{u}ft werden k\"{o}nnen. Das Verfahren wurde in Umgebung, in der diskrete Modelle erstellt und \"{u}berpr\"{u}ft werden k\"{o}nnen, als Prototyp umgesetzt. Dieser dient dazu anhand von Experimenten Eigenschaften des Verfahrens herauszufi nden.}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } Die Sicherheit von technischen System ist in vielen Gebieten wie der Luftfahrt oder im Straßenverkehr von elementarer Bedeutung für die Hersteller solcher Systeme wie für die Anwender. Ein Ansatz um die Sicherheit von diskreten Systemen zu zeigen, besteht darin, diese in einem diskreten Modell zu abstrahieren und anschließend mit einem Model Checker auf gefährdende Situationen zu überprüfen. Viele Szenarien in den Anwendungsbereichen wie der Luftfahrt oder dem Straßenverkehr beruhen jedoch auf kontinuierlichem Systemverhalten. In dieser Arbeit wird ein Verfahren vorgestellt, das ein kontinuierliches System in diskrete Automaten abstrahiert, sodass diese Automaten mit einem symbolischen Model Checker auf eine Sicherheitsspezifi kation überprüft werden können. Das Verfahren wurde in Umgebung, in der diskrete Modelle erstellt und überprüft werden können, als Prototyp umgesetzt. Dieser dient dazu anhand von Experimenten Eigenschaften des Verfahrens herauszufi nden. |
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. @article{saml-vs-altarica-ress-elsevier-2015, title = {Comparison of Modeling Formalisms for Safety Analyses: SAML and AltaRica}, author = {Michael Lipaczewski and Tatiana Prosvirnova and Frank Ortmeier and Antoine Rauzy and Simon Struck}, url = {http://www.sciencedirect.com/science/article/pii/S0951832015001040}, year = {2015}, date = {2015-04-08}, journal = {Reliability Engineering & System Safety}, abstract = {Many states/transitions formalisms have been proposed in the literature to perform Safety Analyses. In this paper we compare two of them: SAML and AltaRica. These formalisms have been developed by different communities. Their “look-and-feel” are thus quite different. Yet, their underlying mathematical foundations are very similar: both of them rely on state automata. It is therefore of interest to study their ability to assess the reliability of systems, their respective advantages and drawbacks and to seek for opportunities of a cross fertilization.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Many states/transitions formalisms have been proposed in the literature to perform Safety Analyses. In this paper we compare two of them: SAML and AltaRica. These formalisms have been developed by different communities. Their “look-and-feel” are thus quite different. Yet, their underlying mathematical foundations are very similar: both of them rely on state automata. It is therefore of interest to study their ability to assess the reliability of systems, their respective advantages and drawbacks and to seek for opportunities of a cross fertilization. |
Gonschorek, Tim A Backward Model Checking Approach with Slicing Abschlussarbeit Otto-von-Guericke-University Magdeburg, 2015. @mastersthesis{Gonschorek2015, title = {A Backward Model Checking Approach with Slicing}, author = {Tim Gonschorek}, editor = {Tim Gonschorek }, year = {2015}, date = {2015-02-25}, address = {Universit\"{a}tsplatz 2, 39106 Magdeburg}, school = {Otto-von-Guericke-University Magdeburg}, abstract = {As software intensive safety critical systems are more and more introduced in our daily lives, it must be ensured that those systems safe. One method for ensuring that a system follows its given speci cation, i.e., does not have some unwanted behavior, is model checking. Although, nowadays larger models can be veri ed, model checking algorithms does not perform well in combination with complex real world problems. To overcome this diculties, this thesis proposes a new backward model checking algorithm using SMT programs instead of boolean encodings for representing the systems state. Additionally, it uses model based slicing to reduce the impact of the complexity of a given model. This thesis explains such an algorithm, which can be used for verifying safety properties. Further, this thesis presents a prototypical implementation of this algorithm. This prototype will be used to evaluate the algorithm in comparison to the BDD and the IC3 algorithms implemented in the model checker nuXmv. The evaluation shows that there are some cases where the proposed approach performs better than the given BDD algorithm.}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } As software intensive safety critical systems are more and more introduced in our daily lives, it must be ensured that those systems safe. One method for ensuring that a system follows its given speci cation, i.e., does not have some unwanted behavior, is model checking. Although, nowadays larger models can be veri ed, model checking algorithms does not perform well in combination with complex real world problems. To overcome this diculties, this thesis proposes a new backward model checking algorithm using SMT programs instead of boolean encodings for representing the systems state. Additionally, it uses model based slicing to reduce the impact of the complexity of a given model. This thesis explains such an algorithm, which can be used for verifying safety properties. Further, this thesis presents a prototypical implementation of this algorithm. This prototype will be used to evaluate the algorithm in comparison to the BDD and the IC3 algorithms implemented in the model checker nuXmv. The evaluation shows that there are some cases where the proposed approach performs better than the given BDD algorithm. |
2014 |
Heumüller, Robert VECS Dataflow - A SAML Language Extension Allowing Intuitive Creation of Formal Automata Specifications Abschlussarbeit 2014. @mastersthesis{thesis-heumueller-2014, title = {VECS Dataflow - A SAML Language Extension Allowing Intuitive Creation of Formal Automata Specifications}, author = {Robert Heum\"{u}ller}, url = {/cse/wp-content/uploads/2015/03/thesis.pdf}, year = {2014}, date = {2014-04-10}, type = {Bachelor\'s Thesis}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } |
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. @inproceedings{nykolaychukIMBSA_2014, title = {On Efficiently Specifying Models for Model Checking}, author = { Mykhaylo Nykolaichuk and Michael Lipaczewski and Tino Liebusch and Frank Ortmeier}, url = {http://link.springer.com/chapter/10.1007/978-3-319-12214-4_2 https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Nykolaychuk_IMBSA_2014.pdf }, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of 4th International Symposium on Model Based Safety and Assessment (IMBSA 2014)}, abstract = {Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible. |
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. @inproceedings{FODB:80901349, title = {A Dataflow Notation for SAML - Formal Modeling Without Fearing Timing Constraints}, author = { Robert Heum\"{u}ller and Michael Lipaczewski and Frank Ortmeier}, year = {2014}, date = {2014-01-01}, booktitle = {IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ.}, pages = {43-50}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
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. @inproceedings{FODB:80901605, title = {Bringing VECS to the World - Challenges and Accomplishments in Teaching of Formal Model Analysis}, author = { Michael Lipaczewski and Marco Filax and Frank Ortmeier}, url = {https://doi.org/10.2370/9783844030679}, year = {2014}, date = {2014-01-01}, booktitle = {European Conference on Software Engineering Education. - Herzogenrath : Shaker}, pages = {217-228}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
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. @inproceedings{FODB:80901202, title = {On Traceability of Informal Specifications for Model-Based Verification}, author = { Marco Filax and Tim Gonschorek and Michael Lipaczewski and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/07/filax_IMBSA_2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment.}, pages = {11-18}, publisher = {Magdeburg : Univ.}, abstract = {Safety critical systems are often specified by a set of informal requirements. The fulfillment of those requirements has, in general, to be verified through external assessors. In most cases models (i.e. UML diagrams) are used to communicate system architectures and decide whether a given system meets its requirements. Even though, there already exist multiple approaches to verify safety critical systems and assessors would benefit from the usage of model-based system verifications, they are not commonly used in industry. We propose a traceable modeling approach for verifying safety critical systems specified with a set of informal unstructured requirements. The proposed process is divided into three phases: the analysis of the given set of informal requirements, semi-formalization and formalization.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Safety critical systems are often specified by a set of informal requirements. The fulfillment of those requirements has, in general, to be verified through external assessors. In most cases models (i.e. UML diagrams) are used to communicate system architectures and decide whether a given system meets its requirements. Even though, there already exist multiple approaches to verify safety critical systems and assessors would benefit from the usage of model-based system verifications, they are not commonly used in industry. We propose a traceable modeling approach for verifying safety critical systems specified with a set of informal unstructured requirements. The proposed process is divided into three phases: the analysis of the given set of informal requirements, semi-formalization and formalization. |
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. @inbook{FODB:80901373, title = {VECS - Verification Enviroment for Critical Systems - Tool Supported Formal Modeling an Verification}, author = { Tim Gonschorek and Marco Filax and Michael Lipaczewski and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/07/gonshorek_VECS_2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ.}, pages = {63-64}, keywords = {}, pubstate = {published}, tppubtype = {inbook} } |
2013 |
Nielebock, Sebastian Komposition gewöhnlicher Differentialgleichungen mit sicherheitsrelevanten Zustandsautomaten Abschlussarbeit 2013. @mastersthesis{thesis-nielebock-2013, title = {Komposition gew\"{o}hnlicher Differentialgleichungen mit sicherheitsrelevanten Zustandsautomaten}, author = {Sebastian Nielebock}, url = {/cse/wp-content/uploads/2015/03/MA_Nielebock_final_version.pdf}, year = {2013}, date = {2013-09-17}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } |
Gonschorek, Tim Methodik zur Abstraktion kontinuierlicher Differentialgleichungen Abschlussarbeit Otto-von-Guericke-University Magdeburg, 2013. @mastersthesis{Gonschorek2013, title = {Methodik zur Abstraktion kontinuierlicher Differentialgleichungen}, author = {Tim Gonschorek}, editor = {Tim Gonschorek}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/BA_2013_Gonschorek.pdf}, year = {2013}, date = {2013-06-19}, address = {Universit\"{a}tsplatz 2, 39106 Magdeburg}, school = {Otto-von-Guericke-University Magdeburg}, abstract = {Reale Phanomene aus Natur und Technik konnen oft nur durch kontinuierliche Modelle abgebildet werden. Mithilfe eines Modelchecker konnen Modelle auf Grundlage einer vorgegebenen Spezi kation automatisiert veri ziert werden. Jedoch konnen die meisten Modelchecker nur mit diskreten Modellen umgehen. Deshalb kann ein kontinuierliches Modell nicht direkt mit einem Modelchecker gepruft werden. Diese Arbeit prasentiert eine Methodik, mit der es moglich ist, kontinuierliche Modelle sowohl im Zeitbereich, als auch im Wertebereich zu diskretisieren. Das Modell wird dazu in einen endlichen, diskreten Zustandsautomaten umgewandelt. Es wird ein konkretes Vorgehen erklart, um kontinuierliche Di erentialgleichungen in Di erenzengleichungen umzuwandeln, die in Zustandsubergangen eingebunden werden konnen. Dadurch wird es moglich, die Vorteile eins Modelcheckers fur die Veri kation kontinuierlicher Modelle zu nutzen. Um sicherzustellen, dass der erstellte Automat das kontinuierliche Modell hinreichend abstrahiert, um mithilfe eines Modelcheckers Aussagen tre en zu konnen, wird die Methodik anhand eines Beispielmodells evaluiert. Um die praktische Anwendbarkeit zu zeigen, wird ein komplexe Fallstudie von einem Modelica-Modell in einen SAML-Automaten transformiert. DesWeiteren wird die Architektur einer Java-Komponente vorgestellt, mit der eine Modelica-Datei in eine SAML-Datei transformiert werden kann, um sie mithilfe eines Modelcheckers gegen eine vorgegebene Spezi kation zu veri zieren. Diese Komponente soll als erste Implementation eines Importers fur Modelica-Dateien in eine SAML Umgebung dienen.}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } Reale Phanomene aus Natur und Technik konnen oft nur durch kontinuierliche Modelle abgebildet werden. Mithilfe eines Modelchecker konnen Modelle auf Grundlage einer vorgegebenen Spezi kation automatisiert veri ziert werden. Jedoch konnen die meisten Modelchecker nur mit diskreten Modellen umgehen. Deshalb kann ein kontinuierliches Modell nicht direkt mit einem Modelchecker gepruft werden. Diese Arbeit prasentiert eine Methodik, mit der es moglich ist, kontinuierliche Modelle sowohl im Zeitbereich, als auch im Wertebereich zu diskretisieren. Das Modell wird dazu in einen endlichen, diskreten Zustandsautomaten umgewandelt. Es wird ein konkretes Vorgehen erklart, um kontinuierliche Di erentialgleichungen in Di erenzengleichungen umzuwandeln, die in Zustandsubergangen eingebunden werden konnen. Dadurch wird es moglich, die Vorteile eins Modelcheckers fur die Veri kation kontinuierlicher Modelle zu nutzen. Um sicherzustellen, dass der erstellte Automat das kontinuierliche Modell hinreichend abstrahiert, um mithilfe eines Modelcheckers Aussagen tre en zu konnen, wird die Methodik anhand eines Beispielmodells evaluiert. Um die praktische Anwendbarkeit zu zeigen, wird ein komplexe Fallstudie von einem Modelica-Modell in einen SAML-Automaten transformiert. DesWeiteren wird die Architektur einer Java-Komponente vorgestellt, mit der eine Modelica-Datei in eine SAML-Datei transformiert werden kann, um sie mithilfe eines Modelcheckers gegen eine vorgegebene Spezi kation zu veri zieren. Diese Komponente soll als erste Implementation eines Importers fur Modelica-Dateien in eine SAML Umgebung dienen. |
Ortmeier, Frank; Struck, Simon; Güdemann, Matthias Efficient Optimization of Large Probabilistic Models Artikel Elsevier Journal of Systems and Software, 03/78 , 2013. @article{2013-safety-opti-jss, title = {Efficient Optimization of Large Probabilistic Models}, author = { Frank Ortmeier and Simon Struck and Matthias G\"{u}demann}, url = {http://hal.inria.fr/docs/00/81/66/36/PDF/Struck-Gudemann-Ortmeier-13.pdf}, year = {2013}, date = {2013-01-01}, journal = {Elsevier Journal of Systems and Software}, volume = {03/78}, abstract = {The development of safety critical systems often requires design decisions which influence not only dependability, but also other properties which are often even antagonistic to dependability, e.g., cost. Finding good compromises c onsidering different goals while at the same time guaranteeing sufficiently high saf ety of a system is a very difficult task. We propose an integrated approach for modeling, analysis and optim ization of safety critical systems. It is fully automated with an implementat ion based on the Eclipse platform. The approach is tool-independent, different a nalysis tools can be used and there exists an API for the integration of different optimiza- tion and estimation algorithms. For safety critical systems, a very important criterion is the hazard occurrence probability, whose computation can be quite costly. Therefore we also provide means to speed up optimization by devising different combinations of stochastic estimators and illustrate how t hey can be integrated into the approach. We illustrate the approach on relevant case-studies and provide ex perimental details to validate its effectiveness and applicability.}, keywords = {}, pubstate = {published}, tppubtype = {article} } The development of safety critical systems often requires design decisions which influence not only dependability, but also other properties which are often even antagonistic to dependability, e.g., cost. Finding good compromises c onsidering different goals while at the same time guaranteeing sufficiently high saf ety of a system is a very difficult task. We propose an integrated approach for modeling, analysis and optim ization of safety critical systems. It is fully automated with an implementat ion based on the Eclipse platform. The approach is tool-independent, different a nalysis tools can be used and there exists an API for the integration of different optimiza- tion and estimation algorithms. For safety critical systems, a very important criterion is the hazard occurrence probability, whose computation can be quite costly. Therefore we also provide means to speed up optimization by devising different combinations of stochastic estimators and illustrate how t hey can be integrated into the approach. We illustrate the approach on relevant case-studies and provide ex perimental details to validate its effectiveness and applicability. |
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. @conference{teaching-saml_SEAA2013, title = {Teaching and Training Formal Methods for Safety Critical Systems}, author = { Frank Ortmeier and Michael Lipaczewski}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Teaching_and_Training_Formal_Methods_for_Safety_Critical-_ystems.pdf}, year = {2013}, date = {2013-01-01}, booktitle = {Proceedings of the 39th Euromicro Conference on Iv Software Engineering and Advanced Applications (SEAA 2013)}, abstract = {Embedded systems become a major part in many domains. This also involves systems which might create heavy damages and injuries when they fail. However, because of the rising number of software components used within this embedded hardware, safety-related problems are hard to discover, and it is even harder to prove that there are none. One approach to guarantee the correctness of a system is model-based safety analysis. They rely on an abstract representation of the system which can then be analyzed using model checkers. The results of these analysis are in general much more precise and often reveal surprising results of failure combinations, where no one had ever thought about before. Nevertheless model-based safety analysis is not used widely. Mainly because it is not well-known and hard to apply to current safety standards which rely on manual approaches. Another fact might be, that most approaches are scientific and in most cases prototypes that are hard to use. In this paper we present some ideas and first steps towards an easy to learn and easy to use model based safety approach. Additionally we present different user-interfaces that are supposed to support the user in his learning.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Embedded systems become a major part in many domains. This also involves systems which might create heavy damages and injuries when they fail. However, because of the rising number of software components used within this embedded hardware, safety-related problems are hard to discover, and it is even harder to prove that there are none. One approach to guarantee the correctness of a system is model-based safety analysis. They rely on an abstract representation of the system which can then be analyzed using model checkers. The results of these analysis are in general much more precise and often reveal surprising results of failure combinations, where no one had ever thought about before. Nevertheless model-based safety analysis is not used widely. Mainly because it is not well-known and hard to apply to current safety standards which rely on manual approaches. Another fact might be, that most approaches are scientific and in most cases prototypes that are hard to use. In this paper we present some ideas and first steps towards an easy to learn and easy to use model based safety approach. Additionally we present different user-interfaces that are supposed to support the user in his learning. |
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. @inproceedings{se2012-certification, title = {Using Model-Based Analysis in Certification of Critical Software-Intensive Systems}, author = { Frank Ortmeier and Simon Struck and Michael Lipaczewski}, url = {https://subs.emis.de/LNI/Proceedings/Proceedings199/155.pdf}, isbn = {978-3-88579-293-2}, year = {2012}, date = {2012-02-01}, booktitle = {Softwareengineering 2012 Workshopband}, number = {199}, series = {GI-Edition-Lecture Notes in Informatics (LNI)}, abstract = {Software is taking over more and more functionality in most technical systems, which leads to the term software-intensive or cyber-physical systems. Although this offers many exciting new opportunities, it also makes precise analysis of safety and reliability goals much more complicated. Well-known traditional techniques often reach their limits. Model-based approaches on the other hand can be useful for solving some of these problems. However, in industrial practice answering the question alone is often not sufficient. It is also necessary to explain how answers were found. In this paper, we will show some of the capabilities of modern model-based analysis methods and highlight how they possibly could be used in safety engineering resp. what obstacles need to be avoided.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Software is taking over more and more functionality in most technical systems, which leads to the term software-intensive or cyber-physical systems. Although this offers many exciting new opportunities, it also makes precise analysis of safety and reliability goals much more complicated. Well-known traditional techniques often reach their limits. Model-based approaches on the other hand can be useful for solving some of these problems. However, in industrial practice answering the question alone is often not sufficient. It is also necessary to explain how answers were found. In this paper, we will show some of the capabilities of modern model-based analysis methods and highlight how they possibly could be used in safety engineering resp. what obstacles need to be avoided. |
Struck, Simon Approaches to Multi-Objective Optimization of Formal Specifications Abschlussarbeit 2012. @mastersthesis{thesis-struck-2011, title = {Approaches to Multi-Objective Optimization of Formal Specifications}, author = {Simon Struck}, url = {/cse/wp-content/uploads/2015/03/masterarbeit-struck.pdf}, year = {2012}, date = {2012-01-17}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } |
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. @inproceedings{IWDE2012_NielebockOSW, title = {From Discrete Event Simulation to Virtual Reality Environments}, author = { Sebastian Nielebock and Frank Ortmeier and Marco Schumann and Andr\'{e} Winge}, editor = {Frank Ortmeier and Peter Daniel}, url = {http://dx.doi.org/10.1007/978-3-642-33675-1_48 https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/11/nielebock-iwde-2012.pdf}, doi = {10.1007/978-3-642-33675-1_48}, isbn = {978-3-642-33674-4}, year = {2012}, date = {2012-01-01}, booktitle = {Computer Safety, Reliability, and Security}, volume = {7613}, pages = {508-516}, publisher = {Springer Berlin Heidelberg}, series = {Lecture Notes in Computer Science}, abstract = {Today’s technical systems are often very complex. System dynamics are often hard to predict for humans. However, understanding system behavior is crucial for evaluating design variants and finding errors. One way to cope with this problem is to build logical or virtual simulations. Logical simulations are often very abstract, but can simulate complex behavioral sequences. Virtual reality (VR) simulation is very good for experiencing the system in a view close to reality. However, it is very often static or has only limited dynamics. Until now both approaches exist in relative isolation. In this paper, we report on our experiences in building a mixed simulation, here a discrete event simulator (DES) is coupled with a virtual reality (VR) environment. We will focus on technical and conceptual challenges, but also present possible use cases for user interaction in this strategy to make more detailed investigations possible. Finally a prototype based on the simulation tool ”SLX” and the virtual reality environment ”Virtual Development and Training Platform” is used to evaluate the approach.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Today’s technical systems are often very complex. System dynamics are often hard to predict for humans. However, understanding system behavior is crucial for evaluating design variants and finding errors. One way to cope with this problem is to build logical or virtual simulations. Logical simulations are often very abstract, but can simulate complex behavioral sequences. Virtual reality (VR) simulation is very good for experiencing the system in a view close to reality. However, it is very often static or has only limited dynamics. Until now both approaches exist in relative isolation. In this paper, we report on our experiences in building a mixed simulation, here a discrete event simulator (DES) is coupled with a virtual reality (VR) environment. We will focus on technical and conceptual challenges, but also present possible use cases for user interaction in this strategy to make more detailed investigations possible. Finally a prototype based on the simulation tool ”SLX” and the virtual reality environment ”Virtual Development and Training Platform” is used to evaluate the approach. |
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. @conference{Opti-HASE2012, title = {Multi-Objective Optimization of Formal Specifications}, author = { Simon Struck and Matthias G\"{u}demann and Michael Lipaczewski and Frank Ortmeier}, url = {https://hal.inria.fr/hal-00735640/document}, year = {2012}, date = {2012-01-01}, booktitle = {IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE 2012)}, abstract = {Even in the domain of safety critical systems, safety and reliability are not the only goals and a developing engineer is faced with the problem to find good compromises wrt. other antagonistic objectives, in particular economic aspects of a system. Thus there does not exist a single optimal design variant of a system but only compromises each ``best'' in its own rights . With the rising complexity, especially of cyber-physical systems, the process of manually finding best compromises becomes even more difficult. To cope with this problem, we propose a model-based optimization approach which uses quantitative model-based safety analysis. While the general approach is tool-independent, we implement it technically by introducing well defined variation points to a formal system model. These allow enough variability to cover whole families of systems while still being rigorous enough for formal analysis. From the specification of this family of system variants and a set of objective functions, we compute Pareto optimal sets, which represent best compromises. In this paper we present a framework which allows for optimization of arbitrary quantitative goal functions, in particular probabilistic temporal logic properties used for model-based safety analysis. Nevertheless, the approach itself is well applicable to other domains.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Even in the domain of safety critical systems, safety and reliability are not the only goals and a developing engineer is faced with the problem to find good compromises wrt. other antagonistic objectives, in particular economic aspects of a system. Thus there does not exist a single optimal design variant of a system but only compromises each ``best'' in its own rights . With the rising complexity, especially of cyber-physical systems, the process of manually finding best compromises becomes even more difficult. To cope with this problem, we propose a model-based optimization approach which uses quantitative model-based safety analysis. While the general approach is tool-independent, we implement it technically by introducing well defined variation points to a formal system model. These allow enough variability to cover whole families of systems while still being rigorous enough for formal analysis. From the specification of this family of system variants and a set of objective functions, we compute Pareto optimal sets, which represent best compromises. In this paper we present a framework which allows for optimization of arbitrary quantitative goal functions, in particular probabilistic temporal logic properties used for model-based safety analysis. Nevertheless, the approach itself is well applicable to other domains. |
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. @conference{saml-sde-ICSE2012, title = {SAML goes Eclipse - Combining Model-Based Safety Analysis and High-Level Editor Support}, author = { Michael Lipaczewski and Simon Struck and Frank Ortmeier}, url = {https://www.researchgate.net/profile/Frank_Ortmeier/publication/261095247_SAML_goes_eclipse_-_Combining_model-based_safety_analysis_and_high-level_editor_support/links/5704fb7408ae13eb88b937cb.pdf}, year = {2012}, date = {2012-01-01}, booktitle = {Proceedings of the 2nd International Workshop on Developing Tools as Plug-Ins (TOPI)}, pages = {67-72}, publisher = {IEEE}, abstract = {Software-intensive systems become more and more important in safety critical applications, mainly because of the rising number and complexity of embedded system. Many traditional safety analysis techniques where developeddecades ago and thus cannot cope with the complexity of modern systems. Model based analysis techniques where developed to deal with the complexity of software-intensive systems. However, due to the lack of tool support these techniques are currently limited to highly skilled experts. Thus model-based analysis is rarely used by system engineers. Based on the safety analysis modeling language (SAML) framework we propose the S3E , which integrates a complete safety analysis environment into the eclipse platform. S3E covers the whole safety analysis work flow. This implies a powerful editor for model creation, a seamless integration of model-analysis tools and presentation as well as evaluation of the analysis results into one environment. In this paper we present the current state of S3E and first experiences with the eclipse plug-in development.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Software-intensive systems become more and more important in safety critical applications, mainly because of the rising number and complexity of embedded system. Many traditional safety analysis techniques where developeddecades ago and thus cannot cope with the complexity of modern systems. Model based analysis techniques where developed to deal with the complexity of software-intensive systems. However, due to the lack of tool support these techniques are currently limited to highly skilled experts. Thus model-based analysis is rarely used by system engineers. Based on the safety analysis modeling language (SAML) framework we propose the S3E , which integrates a complete safety analysis environment into the eclipse platform. S3E covers the whole safety analysis work flow. This implies a powerful editor for model creation, a seamless integration of model-analysis tools and presentation as well as evaluation of the analysis results into one environment. In this paper we present the current state of S3E and first experiences with the eclipse plug-in development. |
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. @conference{S3E-HASE2012, title = {Using Tool-Supported Model Based Safety Analysis - Progress and Experiences in SAML Development}, author = { Michael Lipaczewski and Simon Struck and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/11/HAZE2012.pdf}, year = {2012}, date = {2012-01-01}, booktitle = {IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE 2012)}, abstract = {Software controls in technical systems are becoming more and more important and complex. Model based safety analysis can give provably correct and complete results, often in a fully automatic way. These methods can answer both logical and probabilistic questions. In common practice, the needed models must be specified in different input languages of different tools depending on the chosen verification tool for the desired aspect. This is time consuming and error-prone. To cope with this problem we developed the safety analysis modeling language (SAML). In this paper, we present a new tool to intuitively create probabilistic, non-deterministic and deterministic specifications for formal analysis. The goal is to give tool-support during modeling and thus make building a formal model less errorprone. The model is then automatically transformed into the input language of state of the art verification engines. We illustrate the approach on a case-study from nuclear power plant domain.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Software controls in technical systems are becoming more and more important and complex. Model based safety analysis can give provably correct and complete results, often in a fully automatic way. These methods can answer both logical and probabilistic questions. In common practice, the needed models must be specified in different input languages of different tools depending on the chosen verification tool for the desired aspect. This is time consuming and error-prone. To cope with this problem we developed the safety analysis modeling language (SAML). In this paper, we present a new tool to intuitively create probabilistic, non-deterministic and deterministic specifications for formal analysis. The goal is to give tool-support during modeling and thus make building a formal model less errorprone. The model is then automatically transformed into the input language of state of the art verification engines. We illustrate the approach on a case-study from nuclear power plant domain. |
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. @conference{saml-process-MBEES2012, title = {Unifying Probabilistic and Traditional Formal Model-Based Analysis}, author = { Matthias G\"{u}demann and Michael Lipaczewski and Simon Struck and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/11/MBEES2012.pdf}, year = {2012}, date = {2012-01-01}, booktitle = {Proceedings of 8. Dagstuhl-Workshop on Model-Based Development of Embedded Systems (MBEES)}, abstract = {The increasing complexity of modern software-intensive systems makes their analysis much more difficult. At the same time, more and more of theses systems are used in safety-critical environment. Model based safety analysis can help with this problem by giving provably correct and complete results, very often in a fully automatic way. Today, such methods can cope with logical as well as probabilistic questions. However, very often the models used in many model based approaches must be specified in different input languages depending on the chosen verification tool for the desired aspect, which is time consuming and often error-prone. In this paper, we report on our experiences in designing a tool independent specification language (SAML) for model based safety analysis. This allows to use only one model and analyze it with different methods and different verification engines, while guaranteeing the equivalence of the analyzed models. In particular, we discuss challenges and possible solutions to integrate SAML in the development process of real systems.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } The increasing complexity of modern software-intensive systems makes their analysis much more difficult. At the same time, more and more of theses systems are used in safety-critical environment. Model based safety analysis can help with this problem by giving provably correct and complete results, very often in a fully automatic way. Today, such methods can cope with logical as well as probabilistic questions. However, very often the models used in many model based approaches must be specified in different input languages depending on the chosen verification tool for the desired aspect, which is time consuming and often error-prone. In this paper, we report on our experiences in designing a tool independent specification language (SAML) for model based safety analysis. This allows to use only one model and analyze it with different methods and different verification engines, while guaranteeing the equivalence of the analyzed models. In particular, we discuss challenges and possible solutions to integrate SAML in the development process of real systems. |
2011 |
Güdemann, Matthias Qualitative and Quantitative Formal Model-Based Safety Analysis Promotionsarbeit 2011. @phdthesis{Diss-Guedemann-2011, title = {Qualitative and Quantitative Formal Model-Based Safety Analysis}, author = { Matthias G\"{u}demann}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/11/Guedemann-Dissertation.pdf http://nbn-resolving.de/urn:nbn:de:gbv:ma9:1-385}, year = {2011}, date = {2011-01-01}, keywords = {}, pubstate = {published}, tppubtype = {phdthesis} } |
Ortmeier, Frank; Lipaczewski, Michael; Güdemann, Matthias Practical Experiences in Model-Based Safety Analysis Konferenz proceedings: International Workshop on Digital Engineering, ACM Proceedings, 2011. @conference{IWDE2011, title = {Practical Experiences in Model-Based Safety Analysis}, author = { Frank Ortmeier and Michael Lipaczewski and Matthias G\"{u}demann}, url = {https://www.researchgate.net/profile/Frank_Ortmeier/publication/265976291_Practical_Experiences_in_Model-Based_Safety_Analysis/links/55ae256208ae98e661a4d26c.pdf}, year = {2011}, date = {2011-01-01}, booktitle = {proceedings: International Workshop on Digital Engineering}, publisher = {ACM Proceedings}, abstract = {The formal modeling framework Safety Analysis and Modelling Language (SAML) allows for a combined specification of qualitative (non-deterministic) and quantitative (probabilistic) aspects. Using semantically founded model transformations, SAML models can be analyzed using current stateof- the art verification tools while guaranteeing that the analysis results of the different tools are computed on equivalent models. The significance of the results, in particular of computed quantitative occurrence probabilities heavily depends on the accuracy of the modeling. The most important factors are the temporal resolution of the model, the considered mission time for the analysis and if applicable also factors like spatial resolution. The overall results always have to be interpreted depending on the character of the system, the properties under consideration and choice of modeling parameters. In general, unfortunately, an increase in system accuracy is strongly correlated to a more complex, in particular resource intensive, analysis. In this paper we discuss qualitatively, how the dependencies between the relevenat model parameters of SAML models afflict the accuracy of the quantitative analysis results. We conduct some experiments with different parameters and survey the effects on the overall results. This work is triggered primarily with regard to optimization of such systems, where the analysis of many different system variants is necessary. In this use case, in early phases of optimization, a compromise between accuracy and running time can be used to explore many variants, identify the most promising ones and then analyze these with more accuracy.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } The formal modeling framework Safety Analysis and Modelling Language (SAML) allows for a combined specification of qualitative (non-deterministic) and quantitative (probabilistic) aspects. Using semantically founded model transformations, SAML models can be analyzed using current stateof- the art verification tools while guaranteeing that the analysis results of the different tools are computed on equivalent models. The significance of the results, in particular of computed quantitative occurrence probabilities heavily depends on the accuracy of the modeling. The most important factors are the temporal resolution of the model, the considered mission time for the analysis and if applicable also factors like spatial resolution. The overall results always have to be interpreted depending on the character of the system, the properties under consideration and choice of modeling parameters. In general, unfortunately, an increase in system accuracy is strongly correlated to a more complex, in particular resource intensive, analysis. In this paper we discuss qualitatively, how the dependencies between the relevenat model parameters of SAML models afflict the accuracy of the quantitative analysis results. We conduct some experiments with different parameters and survey the effects on the overall results. This work is triggered primarily with regard to optimization of such systems, where the analysis of many different system variants is necessary. In this use case, in early phases of optimization, a compromise between accuracy and running time can be used to explore many variants, identify the most promising ones and then analyze these with more accuracy. |
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. @conference{safecomp-saml-opt, title = {Model-Based Multi-Objective Safety Optimization}, author = {Matthias G\"{u}demann and Frank Ortmeier}, editor = {Francesco Flammini and Sandro Bologna and Valeria Vittorini}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Model-Based_Multi-Objective_Safety_Optimization.pdf http://www.safecomp2011.unina.it/}, isbn = {978-3642242694}, year = {2011}, date = {2011-01-01}, booktitle = {Proceedings of the 30th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2011)}, volume = {6894}, publisher = {Springer}, series = {LNCS}, abstract = {It is well-known that in many safety critical applications safety goals are antagonistic to other design goals or even antagonistic to each other. This is a big challenge for the system designers who have to find the best compromises between different goals. In this paper, we show how model-based safety analysis can be combined with multi-objective optimization to balance a safety critical system wrt. different goals. In general the presented approach may be combined with almost any type of (quantitative) safety analysis technique. For additional goal functions, both analytic and black-box functions are possible, derivative information about the functions is not necessary. As an example, we use our quantitative model-based safety analysis in combination with analytical functions describing different other design goals. The result of the approach is a set of emphbest compromises of possible system variants. Technically, the approach relies on genetic algorithms for the optimization. To improve efficiency and scalability to complex systems, elaborate estimation models based on artificial neural networks are used which speed up convergence. The whole approach is illustrated and evaluated on a real world case study from the railroad domain.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } It is well-known that in many safety critical applications safety goals are antagonistic to other design goals or even antagonistic to each other. This is a big challenge for the system designers who have to find the best compromises between different goals. In this paper, we show how model-based safety analysis can be combined with multi-objective optimization to balance a safety critical system wrt. different goals. In general the presented approach may be combined with almost any type of (quantitative) safety analysis technique. For additional goal functions, both analytic and black-box functions are possible, derivative information about the functions is not necessary. As an example, we use our quantitative model-based safety analysis in combination with analytical functions describing different other design goals. The result of the approach is a set of emphbest compromises of possible system variants. Technically, the approach relies on genetic algorithms for the optimization. To improve efficiency and scalability to complex systems, elaborate estimation models based on artificial neural networks are used which speed up convergence. The whole approach is illustrated and evaluated on a real world case study from the railroad domain. |
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. @conference{modelBasedAnalysisToolPRDC2011, title = {Tool Supported Model-Based Safety Analysis and Optimization}, author = { Matthias G\"{u}demann and Michael Lipaczewski and Frank Ortmeier}, url = {http://ieeexplore.ieee.org/abstract/document/6133100/}, year = {2011}, date = {2011-01-01}, booktitle = {Proceedings of the 17th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC 2011)}, abstract = {Although model-based approaches can yield very precises safety analyses, they are rarely used in practice. The reason is, that most techniques are very difficult to apply and almost always require separate models and tools. In this paper we present an outline for the integration of different model-based safety analysis and safety optimization methods into a single tool framework. We present the envisioned workflow and some of the requirements for the tool integration. Because of its wide acceptance, platform independence and its well-documented API, we chose the Eclipse platform as framework foundation.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Although model-based approaches can yield very precises safety analyses, they are rarely used in practice. The reason is, that most techniques are very difficult to apply and almost always require separate models and tools. In this paper we present an outline for the integration of different model-based safety analysis and safety optimization methods into a single tool framework. We present the envisioned workflow and some of the requirements for the tool integration. Because of its wide acceptance, platform independence and its well-documented API, we chose the Eclipse platform as framework foundation. |
checkAll