During the years, our research lead to a number of publications at conferences and journals. Publishing ideas and results is the main resource for fruitful discussions and feedback from the worldwide research community.
2007 |
Ortmeier, Frank; Güdemann, Matthias; Reif, Wolfgang Formal Failure Models Konferenz Proceedings of the 1st IFAC Workshop on Dependable Control of Discrete Systems (DCDS 07), Elsevier, 2007. @conference{formal-failure-models-dcds07, title = {Formal Failure Models}, author = { Frank Ortmeier and Matthias G\"{u}demann and Wolfgang Reif}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/failure-modeling.pdf}, year = {2007}, date = {2007-01-01}, booktitle = {Proceedings of the 1st IFAC Workshop on Dependable Control of Discrete Systems (DCDS 07)}, publisher = {Elsevier}, abstract = {Formal safety analysis methods have gained a lot of importance during the last years. All these methods have in common, that they rely on a formal model of a system which describes desired, functional behavior as well as unwanted erroneous behavior correctly. Most of the time the formal models are created in an ad hoc manner. This is very error prone and therefore compromises the benefit of the following formal analysis. In this paper we present a systematic approach to formally model failure modes. The approach can be combined with most formal safety analysis. We apply the method to a real world case study: a radio-based railroad crossing. We illustrate the results by applying a formal safety analysis method on the model.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Formal safety analysis methods have gained a lot of importance during the last years. All these methods have in common, that they rely on a formal model of a system which describes desired, functional behavior as well as unwanted erroneous behavior correctly. Most of the time the formal models are created in an ad hoc manner. This is very error prone and therefore compromises the benefit of the following formal analysis. In this paper we present a systematic approach to formally model failure modes. The approach can be combined with most formal safety analysis. We apply the method to a real world case study: a radio-based railroad crossing. We illustrate the results by applying a formal safety analysis method on the model. |
Güdemann, Matthias; Angerer, Andreas; Ortmeier, Frank; Reif, Wolfgang Modeling of Self-Adaptive Systems with SCADE Inproceedings 2007. @inproceedings{oc_scade_iscas07, title = {Modeling of Self-Adaptive Systems with SCADE}, author = { Matthias G\"{u}demann and Andreas Angerer and Frank Ortmeier and Wolfgang Reif}, url = {https://www.researchgate.net/publication/224714868_Modeling_of_self-adaptive_systems_with_SCADE}, year = {2007}, date = {2007-01-01}, abstract = {An important property of embedded systems is dependability. Today this addresses mostly safety and reliability. Guaranteeing these properties is normally done by adding redundancy to the system. This approach is expensive and can not cope with changing environments. Therefore new designs are researched, which allow systems to self-adapt and self-heal. For broad acceptance in industry it is important, that organic systems can be modeled and analyzed with standard modeling tools and languages. We present a case study of an adaptive production automation cell modelled in the Lustre language using the SCADE Suite and the verification of functional properties. SCADE is used widely in industry, especially in safety critical applications. Being able to model and verify adaptive systems in SCADE could increase their acceptance for these target areas.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } An important property of embedded systems is dependability. Today this addresses mostly safety and reliability. Guaranteeing these properties is normally done by adding redundancy to the system. This approach is expensive and can not cope with changing environments. Therefore new designs are researched, which allow systems to self-adapt and self-heal. For broad acceptance in industry it is important, that organic systems can be modeled and analyzed with standard modeling tools and languages. We present a case study of an adaptive production automation cell modelled in the Lustre language using the SCADE Suite and the verification of functional properties. SCADE is used widely in industry, especially in safety critical applications. Being able to model and verify adaptive systems in SCADE could increase their acceptance for these target areas. |
Güdemann, Matthias; Ortmeier, Frank; Reif, Wolfgang Using Deductive Cause Consequence Analysis (DCCA) with SCADE Inproceedings Proceedings of SAFECOMP 2007, Springer LNCS 4680, 2007. @inproceedings{DCCA-SCADE-SafeComp-07, title = {Using Deductive Cause Consequence Analysis (DCCA) with SCADE}, author = {Matthias G\"{u}demann and Frank Ortmeier and Wolfgang Reif}, url = {https://pdfs.semanticscholar.org/3862/b1fefcfbd287635bfcdf69704dd6667a0480.pdf}, year = {2007}, date = {2007-01-01}, booktitle = {Proceedings of SAFECOMP 2007}, publisher = {Springer LNCS 4680}, abstract = {Esterel Technologies' SCADE Suite is one of the most important development tools for software for safety-critical systems. It is used for designing many critical components of aerospace, automotive and transportation applications. For such systems safety analysis is a key requirement in the development process. In this paper we show how one formal safety analysis method -- Deductive Cause-Consequence Analysis (DCCA) -- can be integrated in the SCADE framework. This method allows for performing safety analysis mainly automatically. It uses SCADE's semantical model and SCADE's built in verification engine emphDesign Verifier. So the whole analysis can be done within one tool. This is of big importance, as a key feature for the acceptance of formal methods in broad engineering practice is, that they can be applied in an industrial development suite.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Esterel Technologies' SCADE Suite is one of the most important development tools for software for safety-critical systems. It is used for designing many critical components of aerospace, automotive and transportation applications. For such systems safety analysis is a key requirement in the development process. In this paper we show how one formal safety analysis method -- Deductive Cause-Consequence Analysis (DCCA) -- can be integrated in the SCADE framework. This method allows for performing safety analysis mainly automatically. It uses SCADE's semantical model and SCADE's built in verification engine emphDesign Verifier. So the whole analysis can be done within one tool. This is of big importance, as a key feature for the acceptance of formal methods in broad engineering practice is, that they can be applied in an industrial development suite. |
2006 |
Güdemann, Matthias; Ortmeier, Frank; Reif, Wolfgang Formal Modeling and Verification of Systems with Self-x Properties Konferenz Proceedings of the 3rd International Conference on Autonomic and Trusted Computing (ATC-06), 4158 , Lecture Notes in Computer Science Springer, Berlin/Heidelberg, 2006, ISBN: 978-3-540-38619-3. @conference{selfxGOR2006full, title = {Formal Modeling and Verification of Systems with Self-x Properties}, author = { Matthias G\"{u}demann and Frank Ortmeier and Wolfgang Reif}, editor = {Laurence T. Yang and Hai Jin and Jianhua Ma and Theo Ungerer}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Formal_Modeling_and_Verification_of_Systems_with_Self-x_Properties.pdf}, isbn = {978-3-540-38619-3}, year = {2006}, date = {2006-09-01}, booktitle = {Proceedings of the 3rd International Conference on Autonomic and Trusted Computing (ATC-06)}, volume = {4158}, pages = {38--47}, publisher = {Springer}, address = {Berlin/Heidelberg}, series = {Lecture Notes in Computer Science}, abstract = {In this paper we present a case study in formal modeling and verification of systems with self-x properties. The example is a flexible robot production cell reacting to system failures and changing goals. The self-x mechanisms make the system more flexible and robust but endanger its functional correctness or other quality guarantees. We show how to verify such adaptive systems with a restore-invariant'' approach.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } In this paper we present a case study in formal modeling and verification of systems with self-x properties. The example is a flexible robot production cell reacting to system failures and changing goals. The self-x mechanisms make the system more flexible and robust but endanger its functional correctness or other quality guarantees. We show how to verify such adaptive systems with a restore-invariant'' approach. |
Güdemann, Matthias; Nafz, Florian; Reif, Wolfgang; Seebach, Hella Towards Safe and Secure Organic Computing Applications Konferenz INFORMATIK 2006 -- Informatik f"ur Menschen, P-93 , GI-Edition -- Lecture Notes in Informatics K, Bonn, Germany, 2006, ISBN: 978-3-88579-187-4. @conference{GuNaReSe:2006:SafeSecureApplications, title = {Towards Safe and Secure Organic Computing Applications}, author = { Matthias G\"{u}demann and Florian Nafz and Wolfgang Reif and Hella Seebach}, editor = {Christian Hochberger and R\"{u}diger Liskowsky}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/GI-Workshop-OC-paperID_10.pdf}, isbn = {978-3-88579-187-4}, year = {2006}, date = {2006-09-01}, booktitle = {INFORMATIK 2006 -- Informatik f"ur Menschen}, volume = {P-93}, pages = {153--160}, publisher = {K}, address = {Bonn, Germany}, series = {GI-Edition -- Lecture Notes in Informatics}, abstract = {In this paper we present our ongoing work on organic computing''. We present an illustrative case study from program automation that uses OC-paradigms to be failure tolerant and to produce effectively. We present a way to build and verify a formal model of a self-adaptive system. We also give further ideas for formal modeling and our ideas of safety analysis of such systems. Another topic is how to build descriptive models and devising development processes for them.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } In this paper we present our ongoing work on organic computing''. We present an illustrative case study from program automation that uses OC-paradigms to be failure tolerant and to produce effectively. We present a way to build and verify a formal model of a self-adaptive system. We also give further ideas for formal modeling and our ideas of safety analysis of such systems. Another topic is how to build descriptive models and devising development processes for them. |
Ortmeier, Frank; Schellhorn, Gerhard Formal Fault Tree Analysis - Practical Experiences Konferenz Proceedings of 6th International Workshop On Automated Verification of Critical Systems (AVoCS 06), 2006. @conference{FTAFFB06, title = {Formal Fault Tree Analysis - Practical Experiences}, author = { Frank Ortmeier and Gerhard Schellhorn}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Formal_Fault_Tree_Analysis-Practical_Experiences.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {Proceedings of 6th International Workshop On Automated Verification of Critical Systems (AVoCS 06)}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Güdemann, Matthias; Ortmeier, Frank; Reif, Wolfgang Safety and Dependability Analysis of Self-Adaptive Systems Konferenz Proceedings of the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 06), IEEE CS Press, 2006. @conference{ISoLA06, title = {Safety and Dependability Analysis of Self-Adaptive Systems}, author = { Matthias G\"{u}demann and Frank Ortmeier and Wolfgang Reif}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Safety_and_Dependability_Analysis_of_Self-Adaptive_Systems.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {Proceedings of the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 06)}, publisher = {IEEE CS Press}, abstract = {In this paper we present a technique for safety analysis of self-adaptive systems with formal methods. Self-adaptive systems are characterized by the ability to dynamically (self-)adapt and reorganize. The aim of this approach is to make the systems more dependable. But in general it is unclear how big the benefit is - compared to a traditional design. We propose a dependability analysis based on the results of safety analysis to measure the quality of self-x capabilities of an adaptive system with formal methods. This is important for unbiased and evidence-based decision making in early design phases. To illustrate the results we show the application of the method to a case study from the domain of production automation.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } In this paper we present a technique for safety analysis of self-adaptive systems with formal methods. Self-adaptive systems are characterized by the ability to dynamically (self-)adapt and reorganize. The aim of this approach is to make the systems more dependable. But in general it is unclear how big the benefit is - compared to a traditional design. We propose a dependability analysis based on the results of safety analysis to measure the quality of self-x capabilities of an adaptive system with formal methods. This is important for unbiased and evidence-based decision making in early design phases. To illustrate the results we show the application of the method to a case study from the domain of production automation. |
Güdemann, Matthias; Nafz, Florian; Pietzowski, Andreas; Reif, Wolfgang; Satzger, Benjamin; Seebach, Hella; Ungerer, Theo Applications and Architectures in Organic Comupting Forschungsbericht (21), 2006. @techreport{oc_workshop06, title = {Applications and Architectures in Organic Comupting}, author = { Matthias G\"{u}demann and Florian Nafz and Andreas Pietzowski and Wolfgang Reif and Benjamin Satzger and Hella Seebach and Theo Ungerer}, year = {2006}, date = {2006-01-01}, journal = {DFG SPP 1183 "Organic Computing''}, number = {21}, abstract = {This technical report documents a summary of the SPP-OC Workshop \"Architectures and Applications\" at the University of Augsburg. Architectures and applications of organic computing systems are two of the profile topics of the priority program \"Organic Computing\" of the German Research Foundation (DFG SPP 1183). The report contains the discussion results to the several questions discussed on the mentioned workshop.}, keywords = {}, pubstate = {published}, tppubtype = {techreport} } This technical report documents a summary of the SPP-OC Workshop "Architectures and Applications" at the University of Augsburg. Architectures and applications of organic computing systems are two of the profile topics of the priority program "Organic Computing" of the German Research Foundation (DFG SPP 1183). The report contains the discussion results to the several questions discussed on the mentioned workshop. |
Nafz, Florian; Güdemann, Matthias; Reif, Wolfgang; Seebach, Hella Applications in Organic Computing Forschungsbericht (22), 2006. @techreport{oc_casestudies06, title = {Applications in Organic Computing}, author = { Florian Nafz and Matthias G\"{u}demann and Wolfgang Reif and Hella Seebach}, year = {2006}, date = {2006-01-01}, journal = {DFG SPP 1183 Organic Computing}, number = {22}, abstract = {This technical report provides a summary of the applications and case studies used in the priority program \"Organic Computing\" of the German Research Foundation (DFG SPP 1183). All projects were asked to fill out a consistent form with several points to the respective application. These are presented in this report.}, keywords = {}, pubstate = {published}, tppubtype = {techreport} } This technical report provides a summary of the applications and case studies used in the priority program "Organic Computing" of the German Research Foundation (DFG SPP 1183). All projects were asked to fill out a consistent form with several points to the respective application. These are presented in this report. |
Ortmeier, Frank Formale Sicherheitsanalyse Buch Logos Verlag Berlin, 2006. @book{ortmeier-diss05, title = {Formale Sicherheitsanalyse}, author = { Frank Ortmeier}, editor = {Frank Ortmeier}, url = {http://www.logos-verlag.de/cgi-bin/engbuchmid?isbn=1277&lng=eng&id=}, year = {2006}, date = {2006-01-01}, publisher = {Logos Verlag Berlin}, key = {ISBN 3-8325-1277-2}, keywords = {}, pubstate = {published}, tppubtype = {book} } |
Haneberg, Dominik; Bäumler, Simon; Balser, Michael; Grandy, Holger; Ortmeier, Frank; Reif, Wolfgang; Schellhorn, Gerhard; Schmitt, Jonathan; Stenzel, Kurt The User Interface of the KIV Verification System - A System Description Artikel Electronic Notes in Theoretical Computer Science UITP special issue, 2006. @article{entcs06, title = {The User Interface of the KIV Verification System - A System Description}, author = {Dominik Haneberg and Simon B\"{a}umler and Michael Balser and Holger Grandy and Frank Ortmeier and Wolfgang Reif and Gerhard Schellhorn and Jonathan Schmitt and Kurt Stenzel}, url = {https://www.researchgate.net/publication/200505968_The_User_Interface_of_the_KIV_Verification_System_---_A_System_Description}, year = {2006}, date = {2006-01-01}, journal = {Electronic Notes in Theoretical Computer Science UITP special issue}, abstract = {This article describes the sophisticated graphical user interface (GUI) of the KIV verification system. KIV is a verification system that works on structured algebraic specifications. The KIV GUI provides means for developing and editing structured algebraic specifications and for developing proofs of theorems. The complete development process is performed through the GUI. For editing the specification files XEmacs is used, and for the management of the structured algebraic specifications we use daVinci, an extendable graph drawing tool which has been integrated into the KIV user interface. As proving is the most time-consuming part of formal verification, the most important part of the KIV GUI is our user interface for proof development. The proof is represented as a tree and can be manipulated through context menus. The main proof work is done in a proof window where the sequent of the current goal, the applicable rules and the main menu are displayed. Which rules are applicable depends on the current goal. KIV also supports the context-sensitive application of proof rules.}, keywords = {}, pubstate = {published}, tppubtype = {article} } This article describes the sophisticated graphical user interface (GUI) of the KIV verification system. KIV is a verification system that works on structured algebraic specifications. The KIV GUI provides means for developing and editing structured algebraic specifications and for developing proofs of theorems. The complete development process is performed through the GUI. For editing the specification files XEmacs is used, and for the management of the structured algebraic specifications we use daVinci, an extendable graph drawing tool which has been integrated into the KIV user interface. As proving is the most time-consuming part of formal verification, the most important part of the KIV GUI is our user interface for proof development. The proof is represented as a tree and can be manipulated through context menus. The main proof work is done in a proof window where the sequent of the current goal, the applicable rules and the main menu are displayed. Which rules are applicable depends on the current goal. KIV also supports the context-sensitive application of proof rules. |
2005 |
Ortmeier, Frank; Reif, Wolfgang; Schellhorn, Gerhard Deductive Cause-Consequence Analysis (DCCA) Konferenz Proceedings of the 16th IFAC World Congress, Elsevier, 2005, ISBN: 978-3-902661-75-3. @conference{IFAC05, title = {Deductive Cause-Consequence Analysis (DCCA)}, author = { Frank Ortmeier and Wolfgang Reif and Gerhard Schellhorn}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/DCCA.pdf}, isbn = {978-3-902661-75-3}, year = {2005}, date = {2005-01-01}, booktitle = {Proceedings of the 16th IFAC World Congress}, publisher = {Elsevier}, key = {ISBN: 978-0-08-045108-4 and 0-08-045108-X}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Ortmeier, Frank; Reif, Wolfgang; Schellhorn, Gerhard Formal Safety Analysis of a Radio-Based Railroad Crossing using Deductive Cause-Consequence Analysis (DCCA) Inproceedings Proceedings of 5th European Dependable Computing Conference (EDCC 05), Springer, 2005. @inproceedings{EDCC05, title = {Formal Safety Analysis of a Radio-Based Railroad Crossing using Deductive Cause-Consequence Analysis (DCCA)}, author = { Frank Ortmeier and Wolfgang Reif and Gerhard Schellhorn}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.147.2193&rep=rep1&type=pdf}, year = {2005}, date = {2005-01-01}, booktitle = {Proceedings of 5th European Dependable Computing Conference (EDCC 05)}, volume = {3463}, publisher = {Springer}, series = {LNCS}, abstract = {In this paper we present the formal safety analysis of a radio-based railroad crossing. We use deductive cause-consequence analysis (DCCA) as analysis method. DCCA is a novel technique to analyze safety of embedded systems with formal methods. It substitutes error-prone informal reasoning by mathematical proofs. DCCA allows to rigorously prove whether a failure on component level is the cause for system failure or not. DCCA generalizes the two most common safety analysis techniques: failure modes and effects analysis (FMEA) and fault tree analysis (FTA). We apply the method to a real world case study: a radio-based railroad crossing. We illustrate the results of DCCA for this example and compare them to results of other formal safety analysis methods like formal FTA.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } In this paper we present the formal safety analysis of a radio-based railroad crossing. We use deductive cause-consequence analysis (DCCA) as analysis method. DCCA is a novel technique to analyze safety of embedded systems with formal methods. It substitutes error-prone informal reasoning by mathematical proofs. DCCA allows to rigorously prove whether a failure on component level is the cause for system failure or not. DCCA generalizes the two most common safety analysis techniques: failure modes and effects analysis (FMEA) and fault tree analysis (FTA). We apply the method to a real world case study: a radio-based railroad crossing. We illustrate the results of DCCA for this example and compare them to results of other formal safety analysis methods like formal FTA. |
Ortmeier, Frank; Reif, Wolfgang Formal Safety Analysis of Transportation Control Systems Konferenz Workshop at SEFM 2005, 2005. @conference{fehlermodellierung05, title = {Formal Safety Analysis of Transportation Control Systems}, author = { Frank Ortmeier and Wolfgang Reif}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.147.3208&rep=rep1&type=pdf}, year = {2005}, date = {2005-01-01}, booktitle = {Workshop at SEFM 2005}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Ortmeier, Frank; Schellhorn, Gerhard; Thums, Andreas; Reif, Wolfgang atp - Automatisierungstechnische Praxis, 2 , S. 52-59, 2005. @article{elbtunneldeutsch04, title = {Formale Sicherheitsanalyse - Eine Anwendungsfallstudie: Das H\"{o}henkontrollsystem des Elbtunnels in Hamburg}, author = { Frank Ortmeier and Gerhard Schellhorn and Andreas Thums and Wolfgang Reif}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/atp.doc https://www.researchgate.net/publication/200505988_Formale_Sicherheitsanalyse_-_Eine_Anwendungsfallstudie_Das_Hohenkontrollsystem_des_Elbtunnels_in_Hamburg}, year = {2005}, date = {2005-01-01}, journal = {atp - Automatisierungstechnische Praxis}, volume = {2}, pages = {52-59}, keywords = {}, pubstate = {published}, tppubtype = {article} } |
Haneberg, Dominik; Bäumler, Simon; Balser, Michael; Grandy, Holger; Ortmeier, Frank; Reif, Wolfgang; Schellhorn, Gerhard; Schmitt, Jonathan; Stenzel, Kurt The User Interface of the KIV Verification System --- A System Description Konferenz Proceedings of UITP 05, 2005. @conference{UITP05, title = {The User Interface of the KIV Verification System --- A System Description}, author = { Dominik Haneberg and Simon B\"{a}umler and Michael Balser and Holger Grandy and Frank Ortmeier and Wolfgang Reif and Gerhard Schellhorn and Jonathan Schmitt and Kurt Stenzel}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/uitp05.pdf}, year = {2005}, date = {2005-01-01}, booktitle = {Proceedings of UITP 05}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
2004 |
Ortmeier, Frank; Thums, Andreas; Schellhorn, Gerhard; Reif, Wolfgang Combining Formal Methods and Safety Analysis -- The ForMoSA Approach Buchkapitel mit eigenem Titel Integration of Software Specification Techniques for Applications in Engineering (INT 04), Springer LNCS 3147, 2004. @incollection{formosa04-approach, title = {Combining Formal Methods and Safety Analysis -- The ForMoSA Approach}, author = { Frank Ortmeier and Andreas Thums and Gerhard Schellhorn and Wolfgang Reif}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.93.9263&rep=rep1&type=pdf}, year = {2004}, date = {2004-01-01}, booktitle = {Integration of Software Specification Techniques for Applications in Engineering (INT 04)}, publisher = {Springer LNCS 3147}, abstract = {In the ForMoSA project [18] an integrated approach for safety analysis of critical, embedded systems has been developed. The approach brings together the best of engineering practice, formal methods and mathematics: traditional safety analysis, temporal logics and verification, and statistics and optimization. These three orthogonal techniques cover three different aspects of safety: fault tolerance, functional correctness and quantitative analysis. The ForMoSA approach combines these techniques to answer the safety relevant questions in a structured and formal way. Furthermore, the tight combination of methods from different analysis domains yields results which can not be produced by any single technique. The methodology was applied in form of case studies to different industrial domains. One of them is the height control of the Elbtunnel in Hamburg [17] from the domain of electronic traffic control, which we present as an illustrating example.}, keywords = {}, pubstate = {published}, tppubtype = {incollection} } In the ForMoSA project [18] an integrated approach for safety analysis of critical, embedded systems has been developed. The approach brings together the best of engineering practice, formal methods and mathematics: traditional safety analysis, temporal logics and verification, and statistics and optimization. These three orthogonal techniques cover three different aspects of safety: fault tolerance, functional correctness and quantitative analysis. The ForMoSA approach combines these techniques to answer the safety relevant questions in a structured and formal way. Furthermore, the tight combination of methods from different analysis domains yields results which can not be produced by any single technique. The methodology was applied in form of case studies to different industrial domains. One of them is the height control of the Elbtunnel in Hamburg [17] from the domain of electronic traffic control, which we present as an illustrating example. |
Ortmeier, Frank; Reif, Wolfgang Failure-Sensitive Specification: A Formal Method for Finding Failure Modes Forschungsbericht Institut f (3), 2004. @techreport{ortmeier04:fs-spec, title = {Failure-Sensitive Specification: A Formal Method for Finding Failure Modes}, author = { Frank Ortmeier and Wolfgang Reif}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Failure-Sensitive_Specification_A_Formal_Method_for_Finding_Failure_Modes.pdf}, year = {2004}, date = {2004-01-01}, number = {3}, institution = {Institut f}, keywords = {}, pubstate = {published}, tppubtype = {techreport} } |
Ortmeier, Frank; Reif, Wolfgang; Schellhorn, Gerhard; Thums, Andreas Integrated Formal Methods for safety analysis of train systems Konferenz Kluwer Academic Press, 2004, ISBN: 1-4020-8156-1. @conference{wcc04-toulouse-long, title = {Integrated Formal Methods for safety analysis of train systems}, author = { Frank Ortmeier and Wolfgang Reif and Gerhard Schellhorn and Andreas Thums}, editor = {Ren\'{e} Jacquart}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Integrated_Formal_Methods_for_safety_analysis_of_train_systems.pdf}, isbn = {1-4020-8156-1}, year = {2004}, date = {2004-01-01}, publisher = {Kluwer Academic Press}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Thums, Andreas; Ortmeier, Frank; Reif, Wolfgang; Schellhorn, Gerhard Interactive Verification of Statecharts Inproceedings Ehrig, Hartmut (Hrsg.): Integration of Software Specification Techniques for Applications in Engineering, S. 355 – 373, Springer LNCS 3147, 2004. @inproceedings{formosa04-chartverif, title = {Interactive Verification of Statecharts}, author = { Andreas Thums and Frank Ortmeier and Wolfgang Reif and Gerhard Schellhorn}, editor = {Hartmut Ehrig}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Interactive_Verification_of_Statecharts.pdf https://link.springer.com/chapter/10.1007/978-3-540-27863-4_20}, year = {2004}, date = {2004-01-01}, booktitle = {Integration of Software Specification Techniques for Applications in Engineering}, pages = {355 -- 373}, publisher = {Springer LNCS 3147}, abstract = {In this paper, we present an approach to the interactive verification of statecharts. We use STATEMATE statecharts for the formal specification of safety critical systems and Interval Temporal Logic to formalize the proof conditions. To handle infinite data, complex functions and predicates, we use algebraic specifications. Our verification approach is a basis for the aim of the project ForMoSA to put safety analysis techniques on formal grounds. As part of this approach, fault tree analysis (FTA) has been formalized yielding conditions that can be verified using the calculus defined in this paper. Verification conditions resulting from the formal FTA of the radio-based level crossing control have been successfully verified.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } In this paper, we present an approach to the interactive verification of statecharts. We use STATEMATE statecharts for the formal specification of safety critical systems and Interval Temporal Logic to formalize the proof conditions. To handle infinite data, complex functions and predicates, we use algebraic specifications. Our verification approach is a basis for the aim of the project ForMoSA to put safety analysis techniques on formal grounds. As part of this approach, fault tree analysis (FTA) has been formalized yielding conditions that can be verified using the calculus defined in this paper. Verification conditions resulting from the formal FTA of the radio-based level crossing control have been successfully verified. |
Ortmeier, Frank; Reif, Wolfgang; Schellhorn, Gerhard Introduction to Subject Area "Verification" Buchkapitel mit eigenem Titel Integration of Software Specification Techniques for Applications in Engineering, Springer LNCS 3147, 2004. @incollection{formosa04-intro, title = {Introduction to Subject Area "Verification"}, author = { Frank Ortmeier and Wolfgang Reif and Gerhard Schellhorn}, url = {https://www.isse.uni-augsburg.de/publications/reif/2004-verification_intro/2004-verification-intro-pdf.pdf}, year = {2004}, date = {2004-01-01}, booktitle = {Integration of Software Specification Techniques for Applications in Engineering}, publisher = {Springer LNCS 3147}, abstract = {Over the last two decades the use of software in technical applications has dramatically increased. Almost all real-world systems are now embedded systems consisting of hardware and software components. Just think of modern automobiles; every new car comes equipped with computers that have many tasks in almost all parts of the car: fuel injection rates of the engine, airbags, anti-blocking systems (ABS) for brakes or the anti-theft device are some examples.}, keywords = {}, pubstate = {published}, tppubtype = {incollection} } Over the last two decades the use of software in technical applications has dramatically increased. Almost all real-world systems are now embedded systems consisting of hardware and software components. Just think of modern automobiles; every new car comes equipped with computers that have many tasks in almost all parts of the car: fuel injection rates of the engine, airbags, anti-blocking systems (ABS) for brakes or the anti-theft device are some examples. |
Ortmeier, Frank; Schellhorn, Gerhard; Reif, Wolfgang Safety Optimization of a radio-based railroad crossing Konferenz Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2004), 2004, ISBN: 3-9803363-8-7. @conference{safety-opti-ffb04, title = {Safety Optimization of a radio-based railroad crossing}, author = { Frank Ortmeier and Gerhard Schellhorn and Wolfgang Reif}, editor = {E. Schnieder and G. Tarnai}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Safety_Optimization_forms.pdf}, isbn = {3-9803363-8-7}, year = {2004}, date = {2004-01-01}, booktitle = {Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2004)}, key = {ISBN 3-9803363-8-7}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Ortmeier, Frank; Reif, Wolfgang Safety Optimization: A Combination of Fault Tree Analysis and Optimization Techniques Konferenz Proceedings of the Conference on Dependable Systems and Networks (DSN 04), IEEE Computer Society, Florence, 2004, ISBN: 0-7695-2052-9. @conference{safety-opt04, title = {Safety Optimization: A Combination of Fault Tree Analysis and Optimization Techniques}, author = { Frank Ortmeier and Wolfgang Reif}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/safety-opti.pdf}, isbn = {0-7695-2052-9}, year = {2004}, date = {2004-01-01}, booktitle = {Proceedings of the Conference on Dependable Systems and Networks (DSN 04)}, publisher = {IEEE Computer Society}, address = {Florence}, key = {ISBN 0-7695-2052-9}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
2003 |
Thums, Andreas; Ortmeier, Frank Formal Safety Analysis in Ŧransportation Control Konferenz International Workshop on Software Specification of Safety Relevant Transportation Control Tasks, 12 (no. 535) , VDI Fortschritt-Berichte VDI Verlag GmbH, 2003. @conference{TO03, title = {Formal Safety Analysis in {T}ransportation Control}, author = { Andreas Thums and Frank Ortmeier}, editor = {E. Schnieder}, year = {2003}, date = {2003-01-01}, booktitle = {International Workshop on Software Specification of Safety Relevant Transportation Control Tasks}, volume = {12 (no. 535)}, publisher = {VDI Verlag GmbH}, series = {VDI Fortschritt-Berichte}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Ortmeier, Frank; Reif, Wolfgang; Schellhorn, Gerhard; Thums, Andreas; Hering, Bernhard; Trappschuh, Helmut Safety Analysis of the Ħeight Control System for the Elbtunnel Artikel Reliability Engineering and System Safety, 81 (3), S. 259–268, 2003. @article{OSTRress03, title = {Safety Analysis of the {H}eight Control System for the Elbtunnel}, author = { Frank Ortmeier and Wolfgang Reif and Gerhard Schellhorn and Andreas Thums and Bernhard Hering and Helmut Trappschuh}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Safety_Analysis_of_the_Height_Control_System_for_the_Elbtunnel.pdf}, year = {2003}, date = {2003-01-01}, journal = {Reliability Engineering and System Safety}, volume = {81}, number = {3}, pages = {259--268}, abstract = {A new tunnel tube crossing the river Elbe is currently built in Hamburg. Therefore, a new height control system is required. A computer examines the signals from light barriers and overhead sensors to detect vehicles, which try to drive into a tube with insufficient height. If necessary, it raises an alarm that blocks the road. This paper describes the application of two safety analysis techniques on this embedded system: model checking has been used to prove functional correctness with respect to a formal model. Fault tree analysis has validated the model and considered technical defects. Their combination has uncovered a safety flaw, led to a precise requirement specification for the software, and showed various ways to improve system safety.}, keywords = {}, pubstate = {published}, tppubtype = {article} } A new tunnel tube crossing the river Elbe is currently built in Hamburg. Therefore, a new height control system is required. A computer examines the signals from light barriers and overhead sensors to detect vehicles, which try to drive into a tube with insufficient height. If necessary, it raises an alarm that blocks the road. This paper describes the application of two safety analysis techniques on this embedded system: model checking has been used to prove functional correctness with respect to a formal model. Fault tree analysis has validated the model and considered technical defects. Their combination has uncovered a safety flaw, led to a precise requirement specification for the software, and showed various ways to improve system safety. |
2002 |
Ortmeier, Frank; Thums, Andreas Formale Methoden und Sicherheitsanalyse Forschungsbericht Universit (15), 2002, ((in German)). @techreport{OT02, title = {Formale Methoden und Sicherheitsanalyse}, author = { Frank Ortmeier and Andreas Thums}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Formale_Methoden_und_Sicherheitsanalyse.pdf}, year = {2002}, date = {2002-01-01}, number = {15}, institution = {Universit}, note = {(in German)}, keywords = {}, pubstate = {published}, tppubtype = {techreport} } |
Ortmeier, Frank; Reif, Wolfgang; Schellhorn, Gerhard; Thums, Andreas; Hering, Bernhard; Trappschuh, Helmut Safety Analysis of the Height Control System for the Elbtunnel Konferenz SafeComp 2002, Springer LNCS 2434, Catania, Italy, 2002. @conference{OSTRSafecomp2002, title = {Safety Analysis of the Height Control System for the Elbtunnel}, author = { Frank Ortmeier and Wolfgang Reif and Gerhard Schellhorn and Andreas Thums and Bernhard Hering and Helmut Trappschuh}, url = {http://www.springerlink.com/content/50lvk1grndxja1kd/?p=9599f6e547e44be691c61207e379d3d2&pi=0}, year = {2002}, date = {2002-01-01}, booktitle = {SafeComp 2002}, pages = {296 -- 308}, publisher = {Springer LNCS 2434}, address = {Catania, Italy}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |