Publications
2024
P. Fiedler, E. Meenzen, H. Diener, J. Löber, J. Simon, M. Wendt, P. Hühner, T. Jostschulte, Q. T. Ta, S. Wertheimer, S. Wanninger, and F. Leitner-Fischer, "Porting a Real-Time Operating System — A Student Endeavour," in Deutscher Luft- und Raumfahrtkongress 2024, Hamburg, 2024.
@inproceedings{fiedler2024porting, address = {Hamburg},
author = {Fiedler, P. and Meenzen, E. and Diener, H. and L{\"o}ber, J. and Simon, J. and Wendt, M. and H{\"u}hner, P. and Jostschulte, T. and Ta, Q.T. and Wertheimer, S. and Wanninger, S. and Leitner-Fischer, F.},
booktitle = {Deutscher Luft- und Raumfahrtkongress 2024},
date-added = {2024-11-12 13:22:30 +0100},
date-modified = {2024-11-12 13:22:30 +0100},
doi = {10.25967/630347},
publisher = {Deutsche Gesellschaft f{\"u}r Luft- und Raumfahrt - Lilienthal-Oberth e.V.},
title = {Porting a Real-Time Operating System -- A Student Endeavour},
url = {https://doi.org/10.25967/630347},
year = {2024},
bdsk-url-1 = {https://doi.org/10.25967/630347}
}
2022
F. Leitner-Fischer, T. Kibler, H. Herpel, H. Selegrad, and B. Petersen, "Die nächste Generation Embedded-Software-Ingenieure — Welche Kompetenzen sind in Zukunft wichtig und wie vermitteln wir diese?," in Tagungsband Embedded Software Engineering Kongress, 2022.
@inproceedings{ese2022,
author = {Leitner-Fischer, Florian and Kibler, Thomas and Herpel, Hans-J{\"u}rgen and Selegrad, Harald and Petersen, Benno},
booktitle = {Tagungsband Embedded Software Engineering Kongress},
date-added = {2022-12-14 09:42:47 +0100},
date-modified = {2022-12-14 09:46:15 +0100},
title = {Die n{\"a}chste Generation Embedded-Software-Ingenieure -- Welche Kompetenzen sind in Zukunft wichtig und wie vermitteln wir diese?},
year = {2022}
}
2016
F. Leitner-Fischer, S. Leue, and S. Liu, "Automated Freedom from Interference Analysis for Automotive Software," in CARS 2016-4th International Workshop on Critical Automotive applications: Robustness \& Safety, 2016.
@inproceedings{leitner2016automated,
author = {Leitner-Fischer, Florian and Leue, Stefan and Liu, Sirui},
booktitle = {CARS 2016-4th International Workshop on Critical Automotive applications: Robustness \& Safety},
date-added = {2016-11-19 12:29:07 +0000},
date-modified = {2016-11-19 12:29:07 +0000},
title = {Automated Freedom from Interference Analysis for Automotive Software},
year = {2016}
}
G. Caltais, F. Leitner-Fischer, S. Leue, and J. Weiser, "SysML to NuSMV Model Transformation via Object-Orientation," in Sixth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems, 2016.
@inproceedings{CyPhy2016,
author = {Georgiana Caltais and Florian Leitner-Fischer and Stefan Leue and Jannis Weiser},
booktitle = {Sixth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems},
date-added = {2016-11-19 12:30:09 +0000},
date-modified = {2016-11-19 12:30:57 +0000},
title = {SysML to NuSMV Model Transformation via Object-Orientation},
year = {2016}
}
2015
F. Leitner-Fischer, "Causality Checking of Safety-Critical Software and Systems," PhD Thesis , Konstanz, 2015.
@phdthesis{Leitner-Fischer2015Causa-30778, address = {Konstanz},
author = {Leitner-Fischer, Florian},
school = {Universit{\"a}t Konstanz},
title = {Causality Checking of Safety-Critical Software and Systems},
url = {http://nbn-resolving.de/urn:nbn:de:bsz:352-0-286535},
year = {2015},
bdsk-url-1 = {http://nbn-resolving.de/urn:nbn:de:bsz:352-0-286535}
}
A. Beer, S. Heidinger, U. Kühne, F. Leitner-Fischer, and S. Leue, "Symbolic Causality Checking Using Bounded Model Checking," in Proceedings of International SPIN Symposium on Model Checking of Software. Model Checking Software, 2015, pp. 203-221.
@inproceedings{beer2015symbolic,
author = {Beer, Adrian and Heidinger, Stephan and K{\"u}hne, Uwe and Leitner-Fischer, Florian and Leue, Stefan},
booktitle = {Proceedings of International SPIN Symposium on Model Checking of Software. Model Checking Software},
pages = {203--221},
publisher = {Springer},
title = {Symbolic Causality Checking Using Bounded Model Checking},
year = {2015}
}
2014
A. Beer, U. Kühne, F. Leitner-Fischer, S. Leue, and R. Prem, "On the Relationship of Event Order Logic and Linear Temporal Logic," Chair for Software Engineering, University of Konstanz, Technical Report soft-14-02, 2014.
@techreport{tech142,
author = {Adrian Beer and Uwe K{\"u}hne and Florian Leitner-Fischer and Stefan Leue and R{\"u}diger Prem},
institution = {Chair for Software Engineering, University of Konstanz},
month = {January},
note = {Available from: \url{http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-14-02.pdf}},
number = {soft-14-02},
title = {On the Relationship of Event Order Logic and Linear Temporal Logic},
type = {Technical Report},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-14-02.pdf},
year = {2014},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-14-02.pdf}
}
F. Leitner-Fischer and S. Leue, "SpinCause: A Tool for Causality Checking," in Proceedings of International SPIN Symposium on Model Checking of Software. (SPIN 2014), 2014.
@inproceedings{LeiLeu14a,
author = {F. Leitner-Fischer and S. Leue},
booktitle = {Proceedings of International SPIN Symposium on Model Checking of Software. (SPIN 2014)},
date-added = {2014-04-15 11:56:40 +0000},
date-modified = {2014-06-03 09:43:27 +0000},
publisher = {ACM},
title = {{SpinCause: A Tool for Causality Checking}},
year = {2014}
}
A. Beer, U. Kuehne, F. Leitner-Fischer, and S. Leue, "Towards Symbolic Causality Checking using SAT-Solving," in Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2014). Dagstuhl, Germany, 2014.
@inproceedings{BeeKueLeiLeu14, abstract = {In this paper we report on work in progress to extend the QuantUM approach to support the quantitative property analysis of Matlab Simulink / Stateflow models. We propose a translation of Simulink / Stateflow models to CTMCs which can be analyzed using the PRISM model checker inside the QuantUM tool. We also illustrate how the information needed to perform probabilistic analysis of dependability properties can be specified at the level of the Simulink / Stateflow model. We demonstrate the applicability of our approach using a case study taken from the MathWorks examples library.},
author = {Beer, Adrian and Kuehne, Uwe and Leitner-Fischer, Florian and Leue, Stefan},
booktitle = {Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2014). Dagstuhl, Germany},
date-added = {2014-02-26 14:31:36 +0000},
date-modified = {2014-02-26 14:32:27 +0000},
title = {Towards Symbolic Causality Checking using SAT-Solving},
year = {2014},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/mbees2013.pdf}
}
A. Beer, F. Leitner-Fischer, and S. Leue, "On the Relationship of Event Order Logic and Linear Temporal Logic," Chair for Software Engineering, University of Konstanz, Technical Report soft-14-01, 2014.
@techreport{BeeLeiLeu14,
author = {A. Beer and F. Leitner-Fischer and S. Leue},
institution = {Chair for Software Engineering, University of Konstanz},
month = {January},
note = {Available from: \url{http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-14-01.pdf}},
number = {soft-14-01},
title = {On the Relationship of Event Order Logic and Linear Temporal Logic},
type = {Technical Report},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-14-01.pdf},
year = {2014},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-14-01.pdf}
}
2013
F. Leitner-Fischer and S. Leue, "Causality Checking for Complex System Models," in Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2013), Rome, Italy, 2013, pp. 248-267.
@inproceedings{flfsl13,
author = {Leitner-Fischer, Florian and Leue, Stefan},
booktitle = {Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2013), Rome, Italy},
doi = {10.1007/978-3-642-35873-9_16},
isbn = {978-3-642-35872-2},
pages = {248-267},
publisher = {Springer Berlin Heidelberg},
series = {LNCS},
title = {Causality Checking for Complex System Models},
url = {http://dx.doi.org/10.1007/978-3-642-35873-9_16},
volume = {7737},
year = {2013},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-35873-9_16}
}
F. Leitner-Fischer and S. Leue, "Probabilistic Fault Tree Synthesis using Causality Computation," Chair for Software Engineering, University of Konstanz, Technical Report soft-13-03, 2013.
@techreport{LeiLeu13c,
author = {Florian Leitner-Fischer and Stefan Leue},
date-added = {2013-05-21 08:35:54 +0000},
date-modified = {2013-05-21 08:36:27 +0000},
institution = {Chair for Software Engineering, University of Konstanz},
note = {Available from \url{http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-03.pdf}},
number = {soft-13-03},
title = {Probabilistic Fault Tree Synthesis using Causality Computation},
type = {Technical Report},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-03.pdf},
year = {2013},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-01.pdf}
}
F. Leitner-Fischer and S. Leue, "Probabilistic Fault Tree Synthesis using Causality Computation," International Journal of Critical Computer-Based Systems, vol. 4, iss. 2, pp. 119-143, 2013.
@article{LeiLeu1313b,
author = {Florian Leitner-Fischer and Stefan Leue},
date-added = {2013-05-21 08:34:18 +0000},
date-modified = {2013-10-14 09:28:37 +0000},
journal = {International Journal of Critical Computer-Based Systems},
number = {2},
pages = {119-143},
title = {Probabilistic Fault Tree Synthesis using Causality Computation},
url = {http://www.inderscience.com/info/inarticle.php?artid=56492},
volume = {4},
year = {2013},
bdsk-url-1 = {http://www.inderscience.com/info/inarticle.php?artid=56492}
}
F. Leitner-Fischer and S. Leue, "On the Synergy of Probabilistic Causality Computation and Causality Checking," in Proceedings of International SPIN Symposium on Model Checking of Software. Stony Brook, NY, USA, 2013.
@inproceedings{LeiLeu13b,
author = {Leitner-Fischer, Florian and Leue, Stefan},
booktitle = {Proceedings of International SPIN Symposium on Model Checking of Software. Stony Brook, NY, USA},
title = {On the Synergy of Probabilistic Causality Computation and Causality Checking},
year = {2013}
}
A. Beer, F. Leitner-Fischer, and S. Leue, "Model-Based Quantitative Safety Analysis of Matlab Simulink / Stateflow Models," in Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2013). Dagstuhl, Germany, 2013.
@inproceedings{BeeKueLeiLeuPre13a, abstract = {In this paper we report on work in progress to extend the QuantUM approach to support the quantitative property analysis of Matlab Simulink / Stateflow models. We propose a translation of Simulink / Stateflow models to CTMCs which can be analyzed using the PRISM model checker inside the QuantUM tool. We also illustrate how the information needed to perform probabilistic analysis of dependability properties can be specified at the level of the Simulink / Stateflow model. We demonstrate the applicability of our approach using a case study taken from the MathWorks examples library.},
author = {Beer, Adrian and Leitner-Fischer, Florian and Leue, Stefan},
booktitle = {Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2013). Dagstuhl, Germany},
date-modified = {2013-05-21 08:41:09 +0000},
title = {Model-Based Quantitative Safety Analysis of Matlab Simulink / Stateflow Models},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/mbees2013.pdf},
year = {2013},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/mbees2013.pdf}
}
A. Beer, U. Kühne, F. Leitner-Fischer, S. Leue, and R. Prem, "Quantitative Safety Analysis of Non-Deterministic System Architectures," Chair for Software Engineering, University of Konstanz, Technical Report soft-13-02, 2013.
@techreport{BeeKueLeiLeuPre13,
author = {Adrian Beer and Uwe K{\"u}hne and Florian Leitner-Fischer and Stefan Leue and R{\"u}diger Prem},
date-modified = {2012-01-20 11:44:55 +0000},
institution = {Chair for Software Engineering, University of Konstanz},
note = {Available from \url{http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-02.pdf}},
number = {soft-13-02},
title = {Quantitative Safety Analysis of Non-Deterministic System Architectures},
type = {Technical Report},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-02.pdf},
year = {2013},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-02.pdf}
}
F. Leitner-Fischer and S. Leue, "On the Synergy of Probabilistic Causality Computation and Causality Checking," Chair for Software Engineering, University of Konstanz, Technical Report soft-13-01, 2013.
@techreport{LeiLeu13a,
author = {Florian Leitner-Fischer and Stefan Leue},
date-modified = {2012-01-20 11:44:55 +0000},
institution = {Chair for Software Engineering, University of Konstanz},
note = {Available from \url{http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-01.pdf}},
number = {soft-13-01},
title = {On the Synergy of Probabilistic Causality Computation and Causality Checking},
type = {Technical Report},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-01.pdf},
year = {2013},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-01.pdf}
}
2012
A. Beer, U. Kühne, F. Leitner-Fischer, S. Leue, and R. Prem, "Model-based Formal Safety Analysis of an Airport Surveillance Radar System (short paper)," in Participant Proceedings of 12th International Workshop on Automated Verification of Critical Systems (AVOCS 2012). Bamberg, Germany, 2012.
@inproceedings{BeeKueLeiLeuPre12a,
author = {Adrian Beer and Uwe K{\"u}hne and Florian Leitner-Fischer and Stefan Leue and R{\"u}diger Prem},
booktitle = {Participant Proceedings of 12th International Workshop on Automated Verification of Critical Systems (AVOCS 2012). Bamberg, Germany},
date-added = {2012-01-23 15:56:09 +0000},
date-modified = {2012-11-02 10:13:39 +0000},
title = {Model-based Formal Safety Analysis of an Airport Surveillance Radar System (short paper)},
year = {2012}
}
F. Leitner-Fischer and S. Leue, "Towards Causality Checking for Complex System Models," in Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2012). Dagstuhl, Germany, 2012.
@inproceedings{LeiLeu12,
author = {Florian Leitner-Fischer and Stefan Leue},
booktitle = {Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2012). Dagstuhl, Germany},
date-added = {2012-01-23 15:56:09 +0000},
date-modified = {2012-11-02 10:13:39 +0000},
title = {Towards Causality Checking for Complex System Models},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/mbees2012.pdf},
year = {2012},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/mbees2012.pdf}
}
F. Leitner-Fischer and S. Leue, "Causality Checking for Complex System Models," Chair for Software Engineering, University of Konstanz, Technical Report soft-12-02, 2012.
@techreport{LeiLeu12a,
author = {Florian Leitner-Fischer and Stefan Leue},
date-added = {2012-01-23 15:56:06 +0000},
date-modified = {2012-01-23 15:59:43 +0000},
institution = {Chair for Software Engineering, University of Konstanz},
number = {soft-12-02},
title = {Causality Checking for Complex System Models},
type = {Technical Report},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-12-02.pdf},
year = {2012},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-12-02.pdf}
}
A. Beer, U. Kühne, F. Leitner-Fischer, S. Leue, and R. Prem, "Analysis of an Airport Surveillance Radar using the QuantUM approach," Chair for Software Engineering, University of Konstanz, Technical Report soft-12-01, 2012.
@techreport{BeeKueLeiLeuPre12,
author = {Adrian Beer and Uwe K{\"u}hne and Florian Leitner-Fischer and Stefan Leue and R{\"u}diger Prem},
date-added = {2012-03-06 08:51:36 +0000},
date-modified = {2012-03-06 08:51:36 +0000},
institution = {Chair for Software Engineering, University of Konstanz},
note = {Available from http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-12-01.pdf},
number = {soft-12-01},
title = {Analysis of an Airport Surveillance Radar using the QuantUM approach},
type = {Technical Report},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-12-01.pdf},
year = {2012},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-12-01.pdf}
}
2011
F. Leitner-Fischer and S. Leue, "QuantUM: Quantitative Safety Analysis of UML Models," in Proceedings of the Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), 2011.
@inproceedings{LeiLeu11a,
author = {Leitner-Fischer, Florian and Leue, Stefan},
booktitle = {Proceedings of the Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011)},
date-modified = {2011-05-16 10:22:30 +0200},
title = {{QuantUM}: Quantitative Safety Analysis of {UML} Models},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/qapl2011.pdf},
year = {2011},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/qapl2011.pdf}
}
M. Kuntz, F. Leitner-Fischer, S. Leue, and B. Reh, "Challenges in the Modelling and Quantitative Analysis of Safety-Critical Automotive Systems," in Accepted for presentation at ROCKS workshop (ROCKS 2011). Saarbrücken, Germany., 2011.
@inproceedings{Kuntz:2011fk,
author = {M. Kuntz and F. Leitner-Fischer and S. Leue and B. Reh},
booktitle = {Accepted for presentation at ROCKS workshop (ROCKS 2011). Saarbr{\"u}cken, Germany.},
title = {Challenges in the Modelling and Quantitative Analysis of Safety-Critical Automotive Systems},
year = {2011}
}
F. Leitner-Fischer and S. Leue, "The QuantUM Approach in the Context of the ISO Standard 26262 for Automotive Systems (Extended Abstract)," Chair for Software Engineering, University of Konstanz, Technical Report soft-11-01, 2011.
@techreport{soft-11-01,
author = {F. Leitner-Fischer and S. Leue},
date-modified = {2011-04-12 16:21:47 +0200},
institution = {Chair for Software Engineering, University of Konstanz},
number = {soft-11-01},
title = {The QuantUM Approach in the Context of the ISO Standard 26262 for Automotive Systems (Extended Abstract)},
type = {Technical Report},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-11-01.pdf},
year = {2011},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-11-01.pdf}
}
F. Leitner-Fischer and S. Leue, "Quantitative Analysis of UML Models," in Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2011). Dagstuhl, Germany., 2011.
@inproceedings{LeiLeu11,
author = {F. Leitner-Fischer and S. Leue},
booktitle = {Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2011). Dagstuhl, Germany.},
date-modified = {2011-05-16 10:21:55 +0200},
title = {Quantitative Analysis of UML Models},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/mbees2011.pdf},
year = {2011},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/mbees2011.pdf}
}
M. Kuntz, F. Leitner-Fischer, and S. Leue, "From Probabilistic Counterexamples via Causality to Fault Trees," Chair for Software Engineering, University of Konstanz, Technical Report soft-11-02, 2011.
@techreport{KunLeiLeu11a,
author = {Matthias Kuntz and Florian Leitner-Fischer and Stefan Leue},
date-added = {2011-04-12 16:18:54 +0200},
date-modified = {2011-04-12 16:19:49 +0200},
institution = {Chair for Software Engineering, University of Konstanz},
number = {soft-11-02},
title = {From Probabilistic Counterexamples via Causality to Fault Trees},
type = {Technical Report},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-11-02.pdf},
year = {2011},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-11-02.pdf}
}
M. Kuntz, F. Leitner-Fischer, and S. Leue, "From Probabilistic Counterexamples via Causality to Fault Trees," in Proceedings of the Computer Safety, Reliability, and Security – 30th International Conference, SAFECOMP 2011, Naples, Italy, 2011.
@inproceedings{KunLeiLeu11b,
author = {Matthias Kuntz and Florian Leitner-Fischer and Stefan Leue},
booktitle = {Proceedings of the Computer Safety, Reliability, and Security - 30th International Conference, SAFECOMP 2011, Naples, Italy},
date-added = {2011-11-15 11:35:54 +0000},
date-modified = {2011-11-15 11:35:54 +0000},
publisher = {Springer},
series = {LNCS},
title = {From Probabilistic Counterexamples via Causality to Fault Trees},
year = {2011}
}
H. Aljazzar, F. Leitner-Fischer, S. Leue, and D. Simeonov, "DiPro – A Tool for Probabilistic Counterexample Generation," in Proceedings of the 18th International SPIN Workshop, Snowbird, UT, USA, 2011, pp. 183-187.
@inproceedings{AljLeiLeuSim11,
author = {Husain Aljazzar and Florian Leitner-Fischer and Stefan Leue and Dimitar Simeonov},
bibsource = {DBLP, http://dblp.uni-trier.de},
booktitle = {Proceedings of the 18th International SPIN Workshop, Snowbird, UT, USA},
crossref = {DBLP:conf/spin/2011},
date-added = {2011-11-15 11:36:25 +0000},
date-modified = {2011-11-15 11:36:25 +0000},
ee = {http://dx.doi.org/10.1007/978-3-642-22306-8_13},
pages = {183-187},
publisher = {Springer},
series = {LNCS},
title = {DiPro - A Tool for Probabilistic Counterexample Generation},
volume = {6823},
year = {2011}
}
2010
F. Leitner-Fischer, "Quantitative Safety Analysis of UML Models," Master’s Dissertation , 2010.
@mastersthesis{mscflf, abstract = {When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Another obstacle is, that the methods often require a profound knowledge of formal methods, which can rarely be found in industrial practice. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.},
author = {Florian Leitner-Fischer},
date-modified = {2011-11-15 11:33:52 +0000},
language = {eng},
school = {University of Konstanz},
title = {Quantitative Safety Analysis of UML Models},
url = {http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-125206},
year = {2010},
bdsk-url-1 = {http://kops.ub.uni-konstanz.de/volltexte/2010/12520/},
bdsk-url-2 = {http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-125206}
}
B. R. Haverkort, M. Kuntz, F. Leitner-Fischer, A. Remke, and S. Roolvink, "Probabilistic Verification of Architectural Software Models using SoftArc and Prism," in Proceedings of ESREL 2010, 2010.
@inproceedings{ESREL2010,
author = {Boudewijn R. Haverkort and Matthias Kuntz and Florian Leitner-Fischer and Anne Remke and Stephan Roolvink},
booktitle = {Proceedings of ESREL 2010},
date-added = {2010-08-16 12:38:44 +0200},
date-modified = {2012-11-02 10:13:55 +0000},
title = {Probabilistic Verification of Architectural Software Models using SoftArc and Prism},
year = 2010}
H. Aljazzar, M. Kuntz, F. Leitner-Fischer, and S. Leue, "Directed and heuristic counterexample generation for probabilistic model checking: a comparative evaluation," in QUOVADIS ’10: Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems, New York, NY, USA, 2010, pp. 25-32.
@inproceedings{1808883, address = {New York, NY, USA},
author = {Aljazzar, Husain and Kuntz, Matthias and Leitner-Fischer, Florian and Leue, Stefan},
booktitle = {QUOVADIS '10: Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems},
date-added = {2010-05-27 14:45:59 +0200},
date-modified = {2010-05-27 14:52:34 +0200},
doi = {http://doi.acm.org/10.1145/1808877.1808883},
isbn = {978-1-60558-972-5},
location = {Cape Town, South Africa},
pages = {25--32},
publisher = {ACM},
title = {Directed and heuristic counterexample generation for probabilistic model checking: a comparative evaluation},
url = {http://doi.acm.org/10.1145/1808877.1808883},
year = {2010},
bdsk-url-1 = {http://doi.acm.org/10.1145/1808877.1808883}
}
F. Wanner, M. Schaefer, F. Leitner-Fischer, F. Zintgraf, M. Atkinson, and D. A. Keim, "DYNEVI – DYnamic News Entity VIsualization," in Proceedings of the International Symposium on Visual Analytics Science and Technology (EuroVAST 2010), 2010, pp. 69-74.
@inproceedings{WSL+10,
author = {Wanner, Franz and Schaefer, Matthias and Leitner-Fischer, Florian and Zintgraf, Fabian and Atkinson, Martin and Keim, Daniel A.},
booktitle = {Proceedings of the International Symposium on Visual Analytics Science and Technology (EuroVAST 2010)},
date-added = {2011-03-15 13:09:54 +0100},
date-modified = {2011-03-15 13:11:44 +0100},
editor = {Kohlhammer, Joern and Keim, Daniel A.},
key = {WSL+10},
pages = {69--74},
publisher = {Eurographics},
title = {{DYNEVI - DYnamic News Entity VIsualization}},
year = {2010}
}
2009
H. Aljazzar, M. Fischer, L. Grunske, M. Kuntz, F. Leitner-Fischer, and S. Leue, "Safety Analysis of an Airbag System Using Probabilistic FMEA and Probabilistic Counterexamples," in Proceedings of the International Conference on Quantitative Evaluation of Systems (QEST 2009), Los Alamitos, CA, USA, 2009, pp. 299-308.
@inproceedings{10.1109/QEST.2009.8, address = {Los Alamitos, CA, USA},
author = {Husain Aljazzar and Manuel Fischer and Lars Grunske and Matthias Kuntz and Florian Leitner-Fischer and Stefan Leue},
booktitle = {Proceedings of the International Conference on Quantitative Evaluation of Systems (QEST 2009)},
date-modified = {2011-11-15 11:40:32 +0000},
doi = {http://doi.ieeecomputersociety.org/10.1109/QEST.2009.8},
isbn = {978-0-7695-3808-2},
pages = {299-308},
publisher = {IEEE Computer Society},
title = {Safety Analysis of an Airbag System Using Probabilistic FMEA and Probabilistic Counterexamples},
url = {http://doi.ieeecomputersociety.org/10.1109/QEST.2009.8},
volume = {0},
year = {2009},
bdsk-url-1 = {http://doi.ieeecomputersociety.org/10.1109/QEST.2009.8}
}
2008
F. Leitner and S. Leue, "Simulink Design Verifier vs. SPIN – A Comparative Case Study," in Participant’s Proceedings of FMICS 2008, ERCIM Working Group on Formal Methods for Industrial Critical Systems, 2008.
@inproceedings{fmics2008,
author = {F. Leitner and S. Leue},
booktitle = {Participant's Proceedings of FMICS 2008, ERCIM Working Group on Formal Methods for Industrial Critical Systems},
title = {Simulink Design Verifier vs. SPIN - A Comparative Case Study},
url = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/FMICS2008_FINAL.pdf},
year = {2008},
bdsk-url-1 = {http://www.inf.uni-konstanz.de/soft/research/publications/pdf/FMICS2008_FINAL.pdf}
}
F. Leitner, "Bachelor Thesis: Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN,", 2008.
@misc{Leitner08,
author = {Florian Leitner},
date-modified = {2010-03-17 15:44:33 +0100},
institution = {Chair for Software Engineering, University of Konstanz},
language = {eng},
school = {University of Konstanz},
title = {"Bachelor Thesis: Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN,"},
url = {http://kops.ub.uni-konstanz.de/volltexte/2008/6125},
year = {2008},
bdsk-url-1 = {http://kops.ub.uni-konstanz.de/volltexte/2008/6125}
}