Publikationen // Universität Oldenburg

2023

[inproceedings] bibtex
R. Kiaghadi, "Optimal Rescue Sequences in Disastrous Incidents" in Proc. Multi-Agent Systems - 20th European Conference, EUMAS 2023, Naples, Italy, September 14-15, 2023, Proceedings, 2023.
doi: 10.1007/978-3-031-43264-4_43
@InProceedings{kiaghadi:rescue-sequences:2023, author = {Rabeaeh Kiaghadi}, title = {Optimal Rescue Sequences in Disastrous Incidents}, booktitle = {Multi-Agent Systems - 20th European Conference, {EUMAS} 2023, Naples, Italy, September 14-15, 2023, Proceedings}, year = {2023}, editor = {Vadim Malvone and Aniello Murano}, volume = {14282}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, pages = {534--539}, doi = {10.1007/978-3-031-43264-4\_43}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/eumas/Kiaghadi23.bib}, timestamp = {Wed, 13 Sep 2023 08:53:59 +0200}, }
[inproceedings] bibtex
A. Rakow, M. Hajnorouzi, und A. Bairy, "What to tell when? - Information Provision as a Game" in Proc. Proceedings Fifth International Workshop on Formal Methods for Autonomous Systems, FMAS@iFM 2023, Leiden, The Netherlands, 15th and 16th of November 2023, 2023.
doi: 10.4204/EPTCS.395.1
@InProceedings{rakow:whattell:2023, author = {Astrid Rakow and Mehrnoush Hajnorouzi and Akhila Bairy}, title = {What to tell when? - Information Provision as a Game}, booktitle = {Proceedings Fifth International Workshop on Formal Methods for Autonomous Systems, FMAS@iFM 2023, Leiden, The Netherlands, 15th and 16th of November 2023}, year = {2023}, editor = {Marie Farrell and Matt Luckcuck and Mario Gleirscher and Maike Schwammberger}, volume = {395}, series = {{EPTCS}}, pages = {1--9}, doi = {10.4204/EPTCS.395.1}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/corr/abs-2311-09776.bib}, timestamp = {Fri, 22 Dec 2023 16:43:30 +0100}, }
[article] bibtex
A. Rakow, "Framing Relevance for Safety-Critical Autonomous Systems" CoRR, vol. abs/2307.14355.
doi: 10.48550/ARXIV.2307.14355
@Article{rakow:framing-relevance:2023, author = {Astrid Rakow}, title = {Framing Relevance for Safety-Critical Autonomous Systems}, journal = {CoRR}, year = {2023}, volume = {abs/2307.14355}, doi = {10.48550/ARXIV.2307.14355}, eprint = {2307.14355}, eprinttype = {arXiv}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/corr/abs-2307-14355.bib}, timestamp = {Wed, 02 Aug 2023 15:37:53 +0200}, }
[article] bibtex
B. Neurohr, T. Koopmann, E. Moehlmann, und M. Fraenzle, "Determining the Validity of Simulation Models for the Verification of Automated Driving Systems" IEEE Access, vol. 11.
doi: 10.1109/ACCESS.2023.3316354
@Article{neurohr:determining-validity:2023, author = {Birte Neurohr and Tjark Koopmann and Eike Moehlmann and Martin Fraenzle}, title = {Determining the Validity of Simulation Models for the Verification of Automated Driving Systems}, journal = {{IEEE} Access}, year = {2023}, volume = {11}, pages = {102949--102960}, doi = {10.1109/ACCESS.2023.3316354}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/access/NeurohrKMF23.bib}, timestamp = {Sat, 14 Oct 2023 20:13:04 +0200}, }
[article] bibtex
J. Weilbach, S. Gerwinn, M. Kandemir, und M. Fraenzle, "Estimation of Counterfactual Interventions under Uncertainties" CoRR, vol. abs/2309.08332.
doi: 10.48550/ARXIV.2309.08332
@Article{weilbach:estimation-counterfactual:2023, author = {Juliane Weilbach and Sebastian Gerwinn and Melih Kandemir and Martin Fraenzle}, title = {Estimation of Counterfactual Interventions under Uncertainties}, journal = {CoRR}, year = {2023}, volume = {abs/2309.08332}, doi = {10.48550/ARXIV.2309.08332}, eprint = {2309.08332}, eprinttype = {arXiv}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/corr/abs-2309-08332.bib}, timestamp = {Fri, 22 Sep 2023 12:57:22 +0200}, }
[inproceedings] bibtex
M. Fraenzle, W. Hagemann, W. Damm, A. Rakow, und M. Swaminathan, "Safer Than Perception: Assuring Confidence in Safety-Critical Decisions of Automated Vehicles" in Proc. Applicable Formal Methods for Safe Industrial Products - Essays Dedicated to Jan Peleska on the Occasion of His 65th Birthday, 2023.
doi: 10.1007/978-3-031-40132-9_12
@InProceedings{fraenzle:safer-than:2023, author = {Martin Fraenzle and Willem Hagemann and Werner Damm and Astrid Rakow and Mani Swaminathan}, title = {Safer Than Perception: Assuring Confidence in Safety-Critical Decisions of Automated Vehicles}, booktitle = {Applicable Formal Methods for Safe Industrial Products - Essays Dedicated to Jan Peleska on the Occasion of His 65th Birthday}, year = {2023}, editor = {Anne E. Haxthausen and Wen{-}ling Huang and Markus Roggenbach}, volume = {14165}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, pages = {180--201}, doi = {10.1007/978-3-031-40132-9\_12}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/birthday/FranzleHDRS23.bib}, timestamp = {Wed, 20 Sep 2023 17:19:14 +0200}, }
[inproceedings] bibtex
F. C. Córdoba, A. Palmisano, M. Fraenzle, R. Bloem, und B. Koenighofer, "Safety Shielding under Delayed Observation" in Proc. Proceedings of the Thirty-Third International Conference on Automated Planning and Scheduling, July 8-13, 2023, Prague, Czech Republic, 2023.
doi: 10.1609/ICAPS.V33I1.27181
@InProceedings{cordoba:safety-shielding:2023, author = {Filip Cano C{\'{o}}rdoba and Alexander Palmisano and Martin Fraenzle and Roderick Bloem and Bettina Koenighofer}, title = {Safety Shielding under Delayed Observation}, booktitle = {Proceedings of the Thirty-Third International Conference on Automated Planning and Scheduling, July 8-13, 2023, Prague, Czech Republic}, year = {2023}, editor = {Sven Koenig and Roni Stern and Mauro Vallati}, publisher = {{AAAI} Press}, pages = {80--85}, doi = {10.1609/ICAPS.V33I1.27181}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/aips/CordobaPFBK23.bib}, timestamp = {Wed, 20 Sep 2023 11:58:30 +0200}, }
[inproceedings] bibtex
M. Fraenzle, S. Winter, und M. Zimmermann, "Strategies Resilient to Delay: Games under Delayed Control vs. Delay Games" in Proc. Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2023, Udine, Italy, 18-20th September 2023, 2023.
doi: 10.4204/EPTCS.390.14
@InProceedings{fraenzle:delay-resilient:2023, author = {Martin Fraenzle and Sarah Winter and Martin Zimmermann}, title = {Strategies Resilient to Delay: Games under Delayed Control vs. Delay Games}, booktitle = {Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2023, Udine, Italy, 18-20th September 2023}, year = {2023}, editor = {Antonis Achilleos and Dario Della Monica}, volume = {390}, series = {{EPTCS}}, pages = {220--235}, doi = {10.4204/EPTCS.390.14}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/corr/abs-2310-01010.bib}, timestamp = {Mon, 06 Nov 2023 15:17:28 +0100}, }
[inproceedings] bibtex
F. Moradkhani, C. Fibich, und M. Fraenzle, "Verification of LSTM Neural Networks with Non-linear Activation Functions" in Proc. NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16-18, 2023, Proceedings, 2023.
doi: 10.1007/978-3-031-33170-1_1
@InProceedings{moradkhani:non-linear-lstm:2023, author = {Farzaneh Moradkhani and Connor Fibich and Martin Fraenzle}, title = {Verification of {LSTM} Neural Networks with Non-linear Activation Functions}, booktitle = {{NASA} Formal Methods - 15th International Symposium, {NFM} 2023, Houston, TX, USA, May 16-18, 2023, Proceedings}, year = {2023}, editor = {Kristin Yvonne Rozier and Swarat Chaudhuri}, volume = {13903}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, pages = {1--15}, doi = {10.1007/978-3-031-33170-1\_1}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/nfm/MoradkhaniFF23.bib}, timestamp = {Fri, 07 Jul 2023 23:30:52 +0200}, }
[article] bibtex
J. Kröger, B. Koopmann, I. Stierand, und M. Fränzle, "Contract-based specification of mode-dependent timing behavior" Innovations in Systems and Software Engineering.
doi: 10.1007/s11334-023-00531-4
@Article{kroeger:mode-dependent:2023, author = {Kröger, Janis and Koopmann, Björn and Stierand, Ingo and Fränzle, Martin}, title = {Contract-based specification of mode-dependent timing behavior}, journal = {Innovations in Systems and Software Engineering}, year = {2023}, month = sep, issn = {1614-5054}, doi = {10.1007/s11334-023-00531-4}, abstract = {The design of safety-critical systems calls for rigorous application of specification and verification methods. In this context, a comprehensive consideration of safety aspects, which inevitably include timing properties, requires explicit addressing of operating modes and their transitions in the system model as well as in the respective specifications. As a side effect, this helps to reduce verification complexity. This paper presents an extension of a framework for the specification of timing properties following the contract-based design paradigm. It provides enhancements of the underlying specification language, which enables specifying modes, mode transitions, and mode-dependent behavior. A formal semantics is given in order to enable reasoning about such specifications as well as about contract operations like refinement and composition, thus enabling to make statements about mode composition. The results are discussed using a real-world example.}, refid = {Kröger2023}, }
[inproceedings] bibtex
A. Bairy und M. Fränzle, "Optimal Explanation Generation using Attention Distribution Model" in Proc. Human Interaction and Emerging Technologies (IHIET-AI 2023): Artificial Intelligence and Future Applications, 2023.
doi: 10.54941/ahfe1002928
@InProceedings{bairy:optimal-explanation:2023, author = {Akhila Bairy and Martin Fr{\"a}nzle}, title = {Optimal Explanation Generation using Attention Distribution Model}, booktitle = {Human Interaction and Emerging Technologies (IHIET-AI 2023): Artificial Intelligence and Future Applications}, year = {2023}, editor = {Tareq Ahram and Redha Taiar}, volume = {70}, doi = {10.54941/ahfe1002928}, }
[article] bibtex
B. Xue, N. Zhan, und M. Fränzle, "Reach-Avoid Analysis for Polynomial Stochastic Differential Equations" IEEE Transactions on Automatic Control, vol. 69, iss. 3.
doi: 10.1109/TAC.2023.3332570
@Article{xue:polynomial-sde:2023, author = {Xue, Bai and Zhan, Naijun and Fränzle, Martin}, title = {Reach-Avoid Analysis for Polynomial Stochastic Differential Equations}, journal = {IEEE Transactions on Automatic Control}, year = {2024}, volume = {69}, number = {3}, pages = {1882-1889}, doi = {10.1109/TAC.2023.3332570}, keywords = {Stochastic processes;Mathematical models;Stochastic systems;Safety;Computational modeling;Upper bound;Probabilistic logic;Inner approximation;reach-avoid analysis;semidefinite programming;stochastic differential equations (SDEs)}, }
[article] bibtex
F. Cano Córdoba, A. Palmisano, M. Fränzle, R. Bloem, und B. Könighofer, "Safety Shielding under Delayed Observation" Proceedings of the International Conference on Automated Planning and Scheduling, vol. 33, iss. 1.
doi: 10.1609/icaps.v33i1.27181
@Article{cordoba:safety-shielding:2023, author = {Cano Córdoba, Filip and Palmisano, Alexander and Fränzle, Martin and Bloem, Roderick and Könighofer, Bettina}, title = {Safety Shielding under Delayed Observation}, journal = {Proceedings of the International Conference on Automated Planning and Scheduling}, year = {2023}, volume = {33}, number = {1}, month = {Jul.}, pages = {80-85}, doi = {10.1609/icaps.v33i1.27181}, abstractnote = {Agents operating in physical environments need to be able to handle delays in the input and output signals since neither data transmission nor sensing or actuating the environment are instantaneous. Shields are correct-by-construction runtime enforcers that guarantee safe execution by correcting any action that may cause a violation of a formal safety specification. Besides providing safety guarantees, shields should interfere minimally with the agent. Therefore, shields should pick the safe corrective actions in such a way that future interferences are most likely minimized. Current shielding approaches do not consider possible delays in the input signals in their safety analyses. In this paper, we address this issue. We propose synthesis algorithms to compute delay-resilient shields that guarantee safety under worst-case assumptions on the delays of the input signals. We also introduce novel heuristics for deciding between multiple corrective actions, designed to minimize future shield interferences caused by delays. As a further contribution, we present the first integration of shields in a realistic driving simulator. We implemented our delayed shields in the driving simulator Carla. We shield potentially unsafe autonomous driving agents in different safety-critical scenarios and show the effect of delays on the safety analysis.}, }
[article] bibtex
B. Xue, N. Zhan, M. Fränzle, J. Wang, und W. Liu, "Reach-Avoid Verification Based on Convex Optimization" IEEE Transactions on Automatic Control, vol. 69, iss. 1.
doi: 10.1109/TAC.2023.3274821
@Article{xue:convex-optimisation:2023, author = {Xue, Bai and Zhan, Naijun and Fränzle, Martin and Wang, Ji and Liu, Wanwei}, title = {Reach-Avoid Verification Based on Convex Optimization}, journal = {IEEE Transactions on Automatic Control}, year = {2023}, volume = {69}, number = {1}, pages = {598-605}, doi = {10.1109/TAC.2023.3274821}, __markedentry = {[pkroeger:]}, keywords = {Trajectory;Reachability analysis;Optimization;Computational modeling;Ordinary differential equations;Continuous time systems;Semidefinite programming;Ordinary differential equations (ODEs);quantified constraints;reach-avoid verification}, }
[inproceedings] bibtex
A. Trende, I. Krefting, L. Weber, J. Rieger, A. Lüdtke, und M. Fränzle, "Investigation of Graphical User Interfaces for Online Driving Style Customization of Highly Automated Vehicles" in Proc. Human Interaction & Emerging Technologies (IHIET 2023): Artificial Intelligence & Future Applications, 2023.
doi: 10.54941/ahfe1004059
@InProceedings{trende:gui:2023, author = {Alexander Trende and Ina Krefting and Lars Weber and Jochem Rieger and Andreas L{\"u}dtke and Martin Fr{\"a}nzle}, title = {Investigation of Graphical User Interfaces for Online Driving Style Customization of Highly Automated Vehicles}, booktitle = {Human Interaction \& Emerging Technologies (IHIET 2023): Artificial Intelligence \& Future Applications}, year = {2023}, editor = {Tareq Ahram and Redha Taiar}, doi = {10.54941/ahfe1004059}, }
[incollection] bibtex
J. Kröger und M. Fränzle, Updates at Runtime for Cyber Physical Systems. A Game Theoretic ApproachBonn: Gesellschaft für Informatik e.V.
doi: 10.18420/se2023-ws-08
@InCollection{kroeger:updates-runtime:2023, author = {Kröger, Janis and Fränzle, Martin}, title = {Updates at Runtime for Cyber Physical Systems. A Game Theoretic Approach}, booktitle = {Software Engineering 2023 Workshops}, year = {2023}, publisher = {Gesellschaft für Informatik e.V.}, pages = {54--65}, doi = {10.18420/se2023-ws-08}, __markedentry = {[pkroeger:]}, address = {Bonn}, }

2022

[inproceedings] bibtex | Dokument aufrufen
A. Bairy, "Modeling Explanations in Autonomous Vehicles" in Proc. Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings, 2022.
doi: 10.1007/978-3-031-07727-2_20
@inproceedings{bairy:explanations:2022, author = {Akhila Bairy}, editor = {Maurice H. ter Beek and Rosemary Monahan}, title = {Modeling Explanations in Autonomous Vehicles}, booktitle = {Integrated Formal Methods - 17th International Conference, {IFM} 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13274}, pages = {347--351}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-07727-2\_20}, doi = {10.1007/978-3-031-07727-2\_20}, }
[inproceedings] bibtex | Dokument aufrufen
A. Bairy, W. Hagemann, A. Rakow, und M. Schwammberger, "Towards Formal Concepts for Explanation Timing and Justifications" in Proc. 30th IEEE International Requirements Engineering Conference Workshops, RE 2022 - Workshops, Melbourne, Australia, August 15-19, 2022, 2022.
doi: 10.1109/REW56159.2022.00025
@inproceedings{bairy:timing:2022, author = {Akhila Bairy and Willem Hagemann and Astrid Rakow and Maike Schwammberger}, title = {Towards Formal Concepts for Explanation Timing and Justifications}, booktitle = {30th {IEEE} International Requirements Engineering Conference Workshops, {RE} 2022 - Workshops, Melbourne, Australia, August 15-19, 2022}, pages = {98--102}, publisher = {{IEEE}}, year = {2022}, url = {https://doi.org/10.1109/REW56159.2022.00025}, doi = {10.1109/REW56159.2022.00025}, }
[inproceedings] bibtex
A. Rakow und J. Kröger, "Roles and Responsibilities for a Predictable Update Process -- A Position Paper" in Proc. Verification and Evaluation of Computer and Communication Systems, Cham, 2022.
@InProceedings{rakow:roles:2022, author = {Rakow, Astrid and Kr{\"o}ger, Janis}, editor = {Nouri, Ayoub and Wu, Weimin and Barkaoui, Kamel and Li, ZhiWu}, title = {Roles and Responsibilities for a Predictable Update Process -- A Position Paper}, booktitle = {Verification and Evaluation of Computer and Communication Systems}, year = {2022}, publisher = {Springer International Publishing}, address = {Cham}, pages = {17--26}, isbn = {978-3-030-98850-0} }
[inproceedings] bibtex
A. Rakow, "A Doxastic Characterisation of Autonomous Decisive Systems" in Proc. Proceedings Fourth International Workshop on Formal Methods for Autonomous Systems (FMAS) and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE), FMAS/ASYDE@SEFM 2022, and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE)Berlin, Germany, 26th and 27th of September 2022, 2022.
doi: 10.4204/eptcs.371.8
@inproceedings{rakow:doxastic:2022, author = {Astrid Rakow}, editor = {Matt Luckcuck and Marie Farrell}, title = {A Doxastic Characterisation of Autonomous Decisive Systems}, booktitle = {Proceedings Fourth International Workshop on Formal Methods for Autonomous Systems {(FMAS)} and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE), FMAS/ASYDE@SEFM 2022, and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE)Berlin, Germany, 26th and 27th of September 2022}, series = {{EPTCS}}, volume = {371}, pages = {77--85}, year = {2022}, doi = {10.4204/eptcs.371.8}, }
[article] bibtex | Dokument aufrufen
M. Schwammberger, C. Harper, G. V. Alves, G. Chance, T. Pipe, und K. Eder, "Integrating Formal Verification and Simulation-based Assertion Checking in a Corroborative V&V Process" CoRR, vol. abs/2208.05273.
doi: 10.48550/arXiv.2208.05273
@article{schwammberger:assertion-checking:2022, author = {Maike Schwammberger and Christopher Harper and Gleifer Vaz Alves and Greg Chance and Tony Pipe and Kerstin Eder}, title = {Integrating Formal Verification and Simulation-based Assertion Checking in a Corroborative V{\&}V Process}, journal = {CoRR}, volume = {abs/2208.05273}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2208.05273}, doi = {10.48550/arXiv.2208.05273}, eprinttype = {arXiv}, eprint = {2208.05273}, }
[inproceedings] bibtex | Dokument aufrufen
M. Schwammberger und V. Klös, "From Specification Models to Explanation Models: An Extraction and Refinement Process for Timed Automata" in Proc. Proceedings Fourth International Workshop on Formal Methods for Autonomous Systems (FMAS) and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE), FMAS/ASYDE@SEFM 2022, and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE)Berlin, Germany, 26th and 27th of September 2022, 2022.
doi: 10.4204/EPTCS.371.2
@inproceedings{schwammberger:refinement:2022, author = {Maike Schwammberger and Verena Kl{\"{o}}s}, editor = {Matt Luckcuck and Marie Farrell}, title = {From Specification Models to Explanation Models: An Extraction and Refinement Process for Timed Automata}, booktitle = {Proceedings Fourth International Workshop on Formal Methods for Autonomous Systems {(FMAS)} and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE), FMAS/ASYDE@SEFM 2022, and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE)Berlin, Germany, 26th and 27th of September 2022}, series = {{EPTCS}}, volume = {371}, pages = {20--37}, year = {2022}, url = {https://doi.org/10.4204/EPTCS.371.2}, doi = {10.4204/EPTCS.371.2}, }
[inproceedings] bibtex | Dokument aufrufen
G. V. Alves und M. Schwammberger, "Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata" in Proc. Proceedings Fourth International Workshop on Formal Methods for Autonomous Systems (FMAS) and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE), FMAS/ASYDE@SEFM 2022, and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE)Berlin, Germany, 26th and 27th of September 2022, 2022.
doi: 10.4204/EPTCS.371.6
@inproceedings{alves:highway-code:2022, author = {Gleifer Vaz Alves and Maike Schwammberger}, editor = {Matt Luckcuck and Marie Farrell}, title = {Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata}, booktitle = {Proceedings Fourth International Workshop on Formal Methods for Autonomous Systems {(FMAS)} and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE), FMAS/ASYDE@SEFM 2022, and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE)Berlin, Germany, 26th and 27th of September 2022}, series = {{EPTCS}}, volume = {371}, pages = {77--85}, year = {2022}, url = {https://doi.org/10.4204/EPTCS.371.6}, doi = {10.4204/EPTCS.371.6}, }
[inproceedings] bibtex | Dokument aufrufen
V. Klös, M. Sadeghi, und M. Schwammberger, "Welcome to the Second International Workshop on Requirements Engineering for Explainable Systems (RE4ES)" in Proc. 30th IEEE International Requirements Engineering Conference Workshops, RE 2022 - Workshops, Melbourne, Australia, August 15-19, 2022, 2022.
doi: 10.1109/REW56159.2022.00021
@inproceedings{kloes:re4es:2022, author = {Verena Kl{\"{o}}s and Mersedeh Sadeghi and Maike Schwammberger}, title = {Welcome to the Second International Workshop on Requirements Engineering for Explainable Systems {(RE4ES)}}, booktitle = {30th {IEEE} International Requirements Engineering Conference Workshops, {RE} 2022 - Workshops, Melbourne, Australia, August 15-19, 2022}, pages = {81--82}, publisher = {{IEEE}}, year = {2022}, url = {https://doi.org/10.1109/REW56159.2022.00021}, doi = {10.1109/REW56159.2022.00021}, }
[article] bibtex | Dokument aufrufen
A. Abate, U. Fahrenberg, und M. Fränzle, "Introduction to the Special Issue on Distributed Hybrid Systems" Leibniz Trans. Embed. Syst. vol. 8, iss. 2.
doi: 10.4230/LITES.8.2.0
@article{abate:lites:2022, author = {Alessandro Abate and Uli Fahrenberg and Martin Fr{\"{a}}nzle}, title = {Introduction to the Special Issue on Distributed Hybrid Systems}, journal = {Leibniz Trans. Embed. Syst.}, volume = {8}, number = {2}, pages = {00:1--00:3}, year = {2022}, url = {https://doi.org/10.4230/LITES.8.2.0}, doi = {10.4230/LITES.8.2.0}, }
[article] bibtex | Dokument aufrufen
B. Xue, N. Zhan, M. Fränzle, J. Wang, und W. Liu, "Reach-avoid Verification Based on Convex Optimization" CoRR, vol. abs/2208.08105.
doi: 10.48550/arXiv.2208.08105
@article{xue:convex-optimisation:2022, author = {Bai Xue and Naijun Zhan and Martin Fr{\"{a}}nzle and Ji Wang and Wanwei Liu}, title = {Reach-avoid Verification Based on Convex Optimization}, journal = {CoRR}, volume = {abs/2208.08105}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2208.08105}, doi = {10.48550/arXiv.2208.08105}, eprinttype = {arXiv}, eprint = {2208.08105}, }
[article] bibtex | Dokument aufrufen
B. Xue, N. Zhan, und M. Fränzle, "Reach-Avoid Analysis for Stochastic Differential Equations" CoRR, vol. abs/2208.10752.
doi: 10.48550/arXiv.2208.10752
@article{xue:stochastic-de:2022, author = {Bai Xue and Naijun Zhan and Martin Fr{\"{a}}nzle}, title = {Reach-Avoid Analysis for Stochastic Differential Equations}, journal = {CoRR}, volume = {abs/2208.10752}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2208.10752}, doi = {10.48550/arXiv.2208.10752}, eprinttype = {arXiv}, eprint = {2208.10752}, }
[article] bibtex | Dokument aufrufen
B. Koopmann, S. Puch, G. Ehmen, und M. Fränzle, "Cooperative Maneuvers of Highly Automated Vehicles at Urban Intersections: A Game-theoretic Approach" CoRR, vol. abs/2211.01633.
doi: 10.48550/arXiv.2211.01633
@article{koopmann:urban-intersections:2022, author = {Bj{\"{o}}rn Koopmann and Stefan Puch and G{\"{u}}nter Ehmen and Martin Fr{\"{a}}nzle}, title = {Cooperative Maneuvers of Highly Automated Vehicles at Urban Intersections: {A} Game-theoretic Approach}, journal = {CoRR}, volume = {abs/2211.01633}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2211.01633}, doi = {10.48550/arXiv.2211.01633}, eprinttype = {arXiv}, eprint = {2211.01633}, }
[inproceedings] bibtex | Dokument aufrufen
G. Fey, M. Fränzle, und R. Drechsler, "Self-Explanation in Systems of Systems" in Proc. 30th IEEE International Requirements Engineering Conference Workshops, RE 2022 - Workshops, Melbourne, Australia, August 15-19, 2022, 2022.
doi: 10.1109/REW56159.2022.00023
@inproceedings{fey:self-explanation:2022, author = {G{\"{o}}rschwin Fey and Martin Fr{\"{a}}nzle and Rolf Drechsler}, title = {Self-Explanation in Systems of Systems}, booktitle = {30th {IEEE} International Requirements Engineering Conference Workshops, {RE} 2022 - Workshops, Melbourne, Australia, August 15-19, 2022}, pages = {85--91}, publisher = {{IEEE}}, year = {2022}, url = {https://doi.org/10.1109/REW56159.2022.00023}, doi = {10.1109/REW56159.2022.00023}, }
[article] bibtex | Dokument aufrufen
B. Finkbeiner, M. Fränzle, F. Kohn, und P. Kröger, "A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation" Algorithms, vol. 15, iss. 4.
doi: 10.3390/a15040126
@article{finkbeiner:monitoring:2022, author = {Bernd Finkbeiner and Martin Fr{\"{a}}nzle and Florian Kohn and Paul Kr{\"{o}}ger}, title = {A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation}, journal = {Algorithms}, volume = {15}, number = {4}, issn = {1999-4893}, article-number = {126}, year = {2022}, url = {https://doi.org/10.3390/a15040126}, doi = {10.3390/a15040126}, }
[inproceedings] bibtex | Dokument aufrufen
M. Fränzle, "The Quest for an Adequate Semantic Basis of Dense-Time Metric Temporal Logic" in Proc. A Journey from Process Algebra via Timed Automata to Model Learning -- Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, 2022.
doi: 10.1007/978-3-031-15629-8_12
@inproceedings{fraenzle:dense-time-logic:2022, author = {Martin Fr{\"{a}}nzle}, editor = {Nils Jansen and Mari{\"{e}}lle Stoelinga and Petra van den Bos}, title = {The Quest for an Adequate Semantic Basis of Dense-Time Metric Temporal Logic}, booktitle = {A Journey from Process Algebra via Timed Automata to Model Learning -- Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday}, series = {Lecture Notes in Computer Science}, volume = {13560}, pages = {201--212}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-15629-8\_12}, doi = {10.1007/978-3-031-15629-8\_12}, }
[article] bibtex | Dokument aufrufen
M. Fränzle, M. Shirmohammadi, M. Swaminathan, und J. Worrell, "Costs and rewards in priced timed automata" Inf. Comput. vol. 282, p. 104656.
doi: 10.1016/j.ic.2020.104656
@article{fraenzle:pta:2022, author = {Martin Fr{\"{a}}nzle and Mahsa Shirmohammadi and Mani Swaminathan and James Worrell}, title = {Costs and rewards in priced timed automata}, journal = {Inf. Comput.}, volume = {282}, pages = {104656}, year = {2022}, url = {https://doi.org/10.1016/j.ic.2020.104656}, doi = {10.1016/j.ic.2020.104656}, }
[article] bibtex | Dokument aufrufen
D. Grundt, S. L. Jurj, W. Hagemann, P. Kröger, und M. Fränzle, "Verification of Sigmoidal Artificial Neural Networks using iSAT" Electronic Proceedings in Theoretical Computer Science, vol. 361.
doi: 10.4204/eptcs.361.6
@Article{grundt:sigmoidal-nets:2022, author = {Dominik Grundt and Sorin Liviu Jurj and Willem Hagemann and Paul Kröger and Martin Fränzle}, title = {Verification of Sigmoidal Artificial Neural Networks using {iSAT}}, journal = {Electronic Proceedings in Theoretical Computer Science}, year = {2022}, volume = {361}, pages = {45--60}, month = {jul}, doi = {10.4204/eptcs.361.6}, publisher = {Open Publishing Association}, url = {https://doi.org/10.4204%2Feptcs.361.6}, editor = {Anne Remke and Dung Hoang Tran}, booktitle = {Proceedings of The 7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT}, }
[article] bibtex | Dokument aufrufen
A. Trende, A. Unni, M. Jablonski, B. Biebl, A. Lüdtke, M. Fränzle, und J. W. Rieger, "Driver's turning intent recognition model based on brain activation and contextual information" Frontiers in Neuroergonomics, vol. 3.
doi: 10.3389/fnrgo.2022.956863
@article{trende:turning-intent:2022, author = {Trende, Alexander and Unni, Anirudh and Jablonski, Mischa and Biebl, Bianca and Lüdtke, Andreas and Fränzle, Martin and Rieger, Jochem W.}, title = {Driver's turning intent recognition model based on brain activation and contextual information}, journal = {Frontiers in Neuroergonomics}, volume = {3}, year = {2022}, url = {https://www.frontiersin.org/articles/10.3389/fnrgo.2022.956863}, doi = {10.3389/fnrgo.2022.956863}, issn = {2673-6195}, }
[article] bibtex | Dokument aufrufen
A. Unni, A. Trende, C. Pauley, L. Weber, B. Biebl, S. Kacianka, A. Lüdtke, K. Bengler, A. Pretschner, M. Fränzle, und J. W. Rieger, "Investigating Differences in Behavior and Brain in Human-Human and Human-Autonomous Vehicle Interactions in Time-Critical Situations" Frontiers in Neuroergonomics, vol. 3.
doi: 10.3389/fnrgo.2022.836518
@article{unni:differences:2022, author = {Unni, Anirudh and Trende, Alexander and Pauley, Claire and Weber, Lars and Biebl, Bianca and Kacianka, Severin and Lüdtke, Andreas and Bengler, Klaus and Pretschner, Alexander and Fränzle, Martin and Rieger, Jochem W.}, title = {Investigating Differences in Behavior and Brain in Human-Human and Human-Autonomous Vehicle Interactions in Time-Critical Situations}, journal = {Frontiers in Neuroergonomics}, volume = {3}, year = {2022}, url = {https://www.frontiersin.org/articles/10.3389/fnrgo.2022.836518}, doi = {10.3389/fnrgo.2022.836518}, issn = {2673-6195}, }
[inproceedings] bibtex
J. Kröger, B. Koopmann, I. Stierand, N. Tabassam, und M. Fränzle, "Handling of Operating Modes in Contract-Based Timing Specifications" in Proc. Verification and Evaluation of Computer and Communication Systems, Cham, 2022.
@inproceedings{kroeger:modes:2022, author = {Kr{\"o}ger, Janis and Koopmann, Bj{\"o}rn and Stierand, Ingo and Tabassam, Nadra and Fr{\"a}nzle, Martin}, editor = {Nouri, Ayoub and Wu, Weimin and Barkaoui, Kamel and Li, ZhiWu}, title = {Handling of Operating Modes in Contract-Based Timing Specifications}, booktitle = {Verification and Evaluation of Computer and Communication Systems}, year = {2022}, publisher = {Springer International Publishing}, address = {Cham}, pages = {59--74}, isbn = {978-3-030-98850-0} }
[inproceedings] bibtex
N. Tabassam und M. G. Fränzle, "Scenario-Oriented Contract Based Design for Safety of Autonomous Vehicles" in Proc. Smart Transportation Systems 2022, Singapore, 2022.
@inproceedings{tabassam:scenario-oriented:2022, author = {Tabassam, Nadra and Fr{\"a}nzle, Martin Georg}, editor = {Bie, Yiming and Qu, Bob X. and Howlett, Robert J. and Jain, Lakhmi C.}, title = {Scenario-Oriented Contract Based Design for Safety of Autonomous Vehicles}, booktitle = {Smart Transportation Systems 2022}, year = {2022}, publisher = {Springer Nature Singapore}, address = {Singapore}, pages = {171--183}, isbn = {978-981-19-2813-0} }
[inproceedings] bibtex
B. Xue, Q. Wang, N. Zhan, M. Fränzle, und S. Feng, "Differential Games Based on Invariant Sets Generation" in Proc. 2022 American Control Conference (ACC), 2022.
doi: 10.23919/ACC53348.2022.9867496
@inproceedings{xue:differential-games:2022, author = {Xue, Bai and Wang, Qiuye and Zhan, Naijun and Fränzle, Martin and Feng, Shenghua}, booktitle = {2022 American Control Conference (ACC)}, title = {Differential Games Based on Invariant Sets Generation}, year = {2022}, pages = {1285-1292}, doi = {10.23919/ACC53348.2022.9867496} }
[inproceedings] bibtex
A. Trende, I. Krefting, A. Unni, J. Rieger, und M. Fränzle, "A Case-Study for a Human-Centered Approach to Traffic Management Systems" in Proc. HCI International 2022 Posters, Cham, 2022.
@inproceedings{trende:case-study:2022, author = {Trende, Alexander and Krefting, Ina and Unni, Anirudh and Rieger, Jochem W. and Fr{\"a}nzle, Martin}, editor = {Stephanidis, Constantine and Antona, Margherita and Ntoa, Stavroula}, title = {A Case-Study for a Human-Centered Approach to Traffic Management Systems}, booktitle = {HCI International 2022 Posters}, year = {2022}, publisher = {Springer International Publishing}, address = {Cham}, pages = {259--266}, isbn = {978-3-031-06394-7} }
[article] bibtex
M. Fränzle, "Affine Encodings for Optimal Monitoring of Temporal Properties under Uncertain Observation."
doi: 10.15488/13211
@article{franzle2022affine, title = {Affine Encodings for Optimal Monitoring of Temporal Properties under Uncertain Observation}, author = {Fr{\"a}nzle, Martin}, year = {2022}, doi = {10.15488/13211}, publisher = {Hannover: Gottfried Wilhelm Leibniz Universit{\"a}t}, booktitle = {13th Summer Workshop on Interval Methods --- Book of Abstracts}, }
[article] bibtex | Dokument aufrufen
P. Kröger und M. Fränzle, "Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation" Leibniz Transaction on Embedded Systems, vol. 8, iss. 2.
doi: 10.4230/LITES.8.2.5
@article{kroeger:bha:2022, author = {Paul Kr{\"o}ger and Martin Fr{\"a}nzle}, title = {Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation}, journal = {Leibniz Transaction on Embedded Systems}, year = {2022}, volume = {8}, number = {2}, pages = {05:01--05:27}, doi = {10.4230/LITES.8.2.5}, url = {https://doi.org/10.4230/LITES.8.2.5},

2021

[inproceedings] bibtex
A. Trende, A. Unni, J. Rieger, und M. Fränzle, "Modelling Turning Intention in Unsignalized Intersections with Bayesian Networks" in Proc. HCI International 2021 - Posters, Cham, 2021.
@InProceedings{trende:modelling-intention:2021, author = {Trende, Alexander and Unni, Anirudh and Rieger, Jochem and Fr{\"a}nzle, Martin}, title = {Modelling Turning Intention in Unsignalized Intersections with Bayesian Networks}, booktitle = {HCI International 2021 - Posters}, year = {2021}, editor = {Stephanidis, Constantine and Antona, Margherita and Ntoa, Stavroula}, pages = {289--296}, address = {Cham}, publisher = {Springer International Publishing}, isbn = {978-3-030-78645-8}, }
[inproceedings] bibtex
S. vom Dorff, C. Cheng, H. Esen, und M. Fränzle, "Mixed-Neighborhood, Multi-speed Cellular Automata for Safety-Aware Pedestrian Prediction" in Proc. Software Engineering and Formal Methods, Cham, 2021.
@InProceedings{dorff:cellular-automata:2021, author = {Dorff, Sebastian vom and Cheng, Chih-Hong and Esen, Hasan and Fr{\"a}nzle, Martin}, title = {Mixed-Neighborhood, Multi-speed Cellular Automata for Safety-Aware Pedestrian Prediction}, booktitle = {Software Engineering and Formal Methods}, year = {2021}, editor = {Calinescu, Radu and P{\u{a}}s{\u{a}}reanu, Corina S.}, pages = {501--520}, address = {Cham}, publisher = {Springer International Publishing}, isbn = {978-3-030-92124-8}, }
[inproceedings] bibtex
A. Rakow und J. Kröger, "Roles and Responsibilities for a Predictable Update Process -- A Position Paper" in Proc. Verification and Evaluation of Computer and Communication Systems, Cham, 2022.
@InProceedings{rakow:responsibilities:2021, author = {Rakow, Astrid and Kr{\"o}ger, Janis}, title = {Roles and Responsibilities for a Predictable Update Process -- A Position Paper}, booktitle = {Verification and Evaluation of Computer and Communication Systems}, year = {2022}, editor = {Nouri, Ayoub and Wu, Weimin and Barkaoui, Kamel and Li, ZhiWu}, pages = {17--26}, address = {Cham}, publisher = {Springer International Publishing}, isbn = {978-3-030-98850-0}, }
[inproceedings] bibtex
J. Kröger, B. Koopmann, I. Stierand, N. Tabassam, und M. Fränzle, "Handling of Operating Modes in Contract-Based Timing Specifications" in Proc. Verification and Evaluation of Computer and Communication Systems, Cham, 2022.
@InProceedings{kroeger:mode-handling:2021, author = {Kr{\"o}ger, Janis and Koopmann, Bj{\"o}rn and Stierand, Ingo and Tabassam, Nadra and Fr{\"a}nzle, Martin}, title = {Handling of Operating Modes in Contract-Based Timing Specifications}, booktitle = {Verification and Evaluation of Computer and Communication Systems}, year = {2022}, editor = {Nouri, Ayoub and Wu, Weimin and Barkaoui, Kamel and Li, ZhiWu}, pages = {59--74}, address = {Cham}, publisher = {Springer International Publishing}, isbn = {978-3-030-98850-0}, }
[article] bibtex | Dokument aufrufen
M. Schwammberger, "Proving Properties of Autonomous Car Manoeuvres in Urban Traffic" it - Information Technology, vol. 63, iss. 5-6.
doi: doi:10.1515/itit-2021-0007
@Article{schwammberger:properties-of-manoeuvres:2021, author = {Maike Schwammberger}, title = {Proving Properties of Autonomous Car Manoeuvres in Urban Traffic}, journal = {it - Information Technology}, year = {2021}, volume = {63}, number = {5-6}, pages = {253--263}, doi = {doi:10.1515/itit-2021-0007}, url = {https://doi.org/10.1515/itit-2021-0007}, }
[article] bibtex | Dokument aufrufen
P. Kröger und M. Fränzle, "Bayesian Hybrid Automata: Reconciling Formal Methods with Metrology" it - Information Technology, vol. 63, iss. 5-6.
doi: doi:10.1515/itit-2021-0008
@Article{kroeger:bha:2021, author = {Paul Kr{\"o}ger and Martin Fr{\"a}nzle}, title = {Bayesian Hybrid Automata: Reconciling Formal Methods with Metrology}, journal = {it - Information Technology}, year = {2021}, volume = {63}, number = {5-6}, pages = {265--275}, doi = {doi:10.1515/itit-2021-0008}, url = {https://doi.org/10.1515/itit-2021-0008}, }
[article] bibtex | Dokument aufrufen
F. Moradkhani und M. Fränzle, "Functional Verification of Cyber-Physical Systems Containing Machine-learnt Components" it - Information Technology, vol. 63, iss. 5-6.
doi: doi:10.1515/itit-2021-0009
@Article{moradkhani:functional-verification:2021, author = {Farzaneh Moradkhani and Martin Fr{\"a}nzle}, title = {Functional Verification of Cyber-Physical Systems Containing Machine-learnt Components}, journal = {it - Information Technology}, year = {2021}, volume = {63}, number = {5-6}, pages = {277--287}, doi = {doi:10.1515/itit-2021-0009}, url = {https://doi.org/10.1515/itit-2021-0009}, }
[article] bibtex | Dokument aufrufen
E. B. Abdelwahab und M. Fränzle, "A Sampling-Based Approach for Handling Delays in Continuous and Hybrid Systems" it - Information Technology, vol. 63, iss. 5-6.
doi: doi:10.1515/itit-2021-0010
@Article{abdelwahab:delay-handling:2021, author = {Erzana Berani Abdelwahab and Martin Fr{\"a}nzle}, title = {A Sampling-Based Approach for Handling Delays in Continuous and Hybrid Systems}, journal = {it - Information Technology}, year = {2021}, volume = {63}, number = {5-6}, pages = {289--298}, doi = {doi:10.1515/itit-2021-0010}, url = {https://doi.org/10.1515/itit-2021-0010}, }
[article] bibtex | Dokument aufrufen
E. Olderog, M. Fränzle, O. Theel, und P. Kröger, "System Correctness under Adverse Conditions" it - Information Technology, vol. 63, iss. 5-6.
doi: doi:10.1515/itit-2021-0043
@Article{olderog:scare:2021, author = {Ernst-R{\"u}diger Olderog and Martin Fr{\"a}nzle and Oliver Theel and Paul Kr{\"o}ger}, title = {System Correctness under Adverse Conditions}, journal = {it - Information Technology}, year = {2021}, volume = {63}, number = {5-6}, pages = {249--251}, doi = {doi:10.1515/itit-2021-0043}, url = {https://doi.org/10.1515/itit-2021-0043}, }
[inbook] bibtex | Dokument aufrufen
I. Krefting, A. Trende, A. Unni, J. Rieger, A. Luedtke, und M. Fränzle, "Evaluation of Graphical Human-Machine Interfaces for Turning Manoeuvres in Automated Vehicles." New York, NY, USA: Association for Computing Machinery, p. 77.
@InBook{krefting:hmi-evaluation:2021, pages = {77–80}, title = {Evaluation of Graphical Human-Machine Interfaces for Turning Manoeuvres in Automated Vehicles}, publisher = {Association for Computing Machinery}, year = {2021}, author = {Krefting, Ina and Trende, Alexander and Unni, Anirudh and Rieger, Jochem and Luedtke, Andreas and Fr\"{a}nzle, Martin}, address = {New York, NY, USA}, isbn = {9781450386418}, booktitle = {13th International Conference on Automotive User Interfaces and Interactive Vehicular Applications}, url = {https://doi.org/10.1145/3473682.3480268}, }
[inproceedings] bibtex
M. Schwammberger, "A Quest of Self-Explainability: When Causal Diagrams meet Autonomous Urban Traffic Manoeuvres" in Proc. 2021 IEEE 29th International Requirements Engineering Conference Workshops (REW), 2021.
doi: 10.1109/REW53955.2021.00035
@InProceedings{schwammberger:causal-diagrams:2021, author = {Schwammberger, Maike}, title = {A Quest of Self-Explainability: When Causal Diagrams meet Autonomous Urban Traffic Manoeuvres}, booktitle = {2021 IEEE 29th International Requirements Engineering Conference Workshops (REW)}, year = {2021}, pages = {195-199}, doi = {10.1109/REW53955.2021.00035}, }
[inproceedings] bibtex
B. Xue, R. Li, N. Zhan, und M. Fränzle, "Reach-avoid Analysis for Stochastic Discrete-time Systems" in Proc. 2021 American Control Conference (ACC), 2021.
doi: 10.23919/ACC50511.2021.9483095
@InProceedings{xue:reach-avoid:2021, author = {Xue, Bai and Li, Renjue and Zhan, Naijun and Fr{\"a}nzle, Martin}, title = {Reach-avoid Analysis for Stochastic Discrete-time Systems}, booktitle = {2021 American Control Conference (ACC)}, year = {2021}, pages = {4879-4885}, doi = {10.23919/ACC50511.2021.9483095}, }
[inproceedings] bibtex
S. vom Dorff, M. Kneissl, und M. Fränzle, "Safe, Deterministic Trajectory Planning for Unstructured and Partially Occluded Environments" in Proc. 2021 IEEE International Intelligent Transportation Systems Conference (ITSC), 2021.
doi: 10.1109/ITSC48978.2021.9565022
@InProceedings{dorff:planning:2021, author = {Dorff, Sebastian vom and Kneissl, Maximilian and Fr{\"a}nzle, Martin}, title = {Safe, Deterministic Trajectory Planning for Unstructured and Partially Occluded Environments}, booktitle = {2021 IEEE International Intelligent Transportation Systems Conference (ITSC)}, year = {2021}, pages = {969-975}, doi = {10.1109/ITSC48978.2021.9565022}, }
[inproceedings] bibtex
H. Guissouma, J. Kröger, S. V. Maelen, und E. Sax, "Extension of Contracts for Variability Modeling and Incremental Update Checks of Cyber Physical Systems" in Proc. 2021 IEEE International Symposium on Systems Engineering (ISSE), 2021.
doi: 10.1109/ISSE51541.2021.9582468
@InProceedings{guissouma:contract-extension:2021, author = {Guissouma, Houssem and Kr{\"o}ger, Janis and Maelen, Sebastian Vander and Sax, Eric}, title = {Extension of Contracts for Variability Modeling and Incremental Update Checks of Cyber Physical Systems}, booktitle = {2021 IEEE International Symposium on Systems Engineering (ISSE)}, year = {2021}, pages = {1-8}, doi = {10.1109/ISSE51541.2021.9582468}, }
[inproceedings] bibtex
M. Schwammberger, "Beweisbare Eigenschaften autonomer Fahrmanöver im Stadtverkehr" in Proc. Ausgezeichnete Informatikdissertationen 2020, Bonn, 2021.
@InProceedings{schwammberger:manoever-eigenschaften:2021, author = {Schwammberger, Maike}, title = {Beweisbare Eigenschaften autonomer Fahrman{\"o}ver im Stadtverkehr}, booktitle = {Ausgezeichnete Informatikdissertationen 2020}, year = {2021}, editor = {Hölldobler, Steffen}, pages = {299-308}, address = {Bonn}, publisher = {Gesellschaft für Informatik e.V.}, }
[inproceedings] bibtex
M. Schwammberger und G. Vaz Alves, "Extending Urban Multi-Lane Spatial Logic to Formalise Road Junction Rules" in Proc. rm Proceedings Third Workshop on Formal Methods for Autonomous Systems, rm Virtual, 21st-22nd of October 2021, 2021.
doi: 10.4204/EPTCS.348.1
@InProceedings{schwammberger:mlsl:2021, author = {Schwammberger, Maike and Vaz Alves, Gleifer}, title = {Extending Urban Multi-Lane Spatial Logic to Formalise Road Junction Rules}, booktitle = {{\rm Proceedings Third Workshop on} Formal Methods for Autonomous Systems, {\rm Virtual, 21st-22nd of October 2021}}, year = {2021}, editor = {Farrell, Marie and Luckcuck, Matt}, volume = {348}, series = {Electronic Proceedings in Theoretical Computer Science}, pages = {1-19}, publisher = {Open Publishing Association}, doi = {10.4204/EPTCS.348.1}, }
[phdthesis] bibtex | Dokument aufrufen
M. Schwammberger, "Distributed Controllers for Provably Safe, Live and Fair Autonomous Car Manoeuvres in Urban Traffic" PhD Thesis , 2021.
@PhdThesis{schwammberger:phd:2021, author = {Maike Schwammberger}, title = {Distributed Controllers for Provably Safe, Live and Fair Autonomous Car Manoeuvres in Urban Traffic}, school = {Oldenburg University, Germany}, year = {2021}, url = {https://oops.uni-oldenburg.de/4961/}, urn = {urn:nbn:de:gbv:715-oops-50422}, }
[article] bibtex | Dokument aufrufen
D. J. Hess, D. Lee, B. Biebl, M. Fränzle, S. Lehnhoff, H. Neema, J. Niehaus, A. Pretschner, und J. Sztipanovits, "A Comparative, Sociotechnical Design Perspective on Responsible Innovation: Multidisciplinary Research and Education on Digitized Energy and Automated Vehicles" Journal of Responsible Innovation, vol. 8, iss. 3.
doi: 10.1080/23299460.2021.1975377
@Article{hess:design-perspective:2021, author = {David J. Hess and Dasom Lee and Bianca Biebl and Martin Fr{\"a}nzle and Sebastian Lehnhoff and Himanshu Neema and J{\"u}rgen Niehaus and Alexander Pretschner and Janos Sztipanovits}, title = {A Comparative, Sociotechnical Design Perspective on Responsible Innovation: Multidisciplinary Research and Education on Digitized Energy and Automated Vehicles}, journal = {Journal of Responsible Innovation}, year = {2021}, volume = {8}, number = {3}, pages = {421-444}, doi = {10.1080/23299460.2021.1975377}, eprint = {https://doi.org/10.1080/23299460.2021.1975377}, publisher = {Routledge}, url = {https://doi.org/10.1080/23299460.2021.1975377}, }
[article] bibtex | Dokument aufrufen
M. Chen, M. Fränzle, Y. Li, P. N. Mosaad, und N. Zhan, "Indecision and Delays are the Parents of Failure--Taming Them Algorithmically by Synthesizing Delay-Resilient Control" Acta Informatica, vol. 58, iss. 5.
@Article{chen:delay-resilient-control:2021, author = {Chen, Mingshuai and Fr{\"a}nzle, Martin and Li, Yangjia and Mosaad, Peter N. and Zhan, Naijun}, title = {Indecision and Delays are the Parents of Failure--Taming Them Algorithmically by Synthesizing Delay-Resilient Control}, journal = {Acta Informatica}, year = {2021}, volume = {58}, number = {5}, pages = {497--528}, month = oct, issn = {1432-0525}, url = {https://doi.org/10.1007/s00236-020-00374-7}, }
[article] bibtex | Dokument aufrufen
T. Kahlke, M. Fränzle, und A. K. Hartmann, "Phase Transition in the Bipartite z-Matching" The European Physical Journal B, vol. 94, iss. 12, p. 244.
@Article{kahlke:phase-transition:2021, author = {Kahlke, Till and Fr{\"a}nzle, Martin and Hartmann, Alexander K.}, title = {Phase Transition in the Bipartite z-Matching}, journal = {The European Physical Journal B}, year = {2021}, volume = {94}, number = {12}, pages = {244}, month = dec, issn = {1434-6036}, url = {https://doi.org/10.1140/epjb/s10051-021-00252-2},

2020

[article] bibtex | Dokument aufrufen
B. Xue, M. Fränzle, und N. Zhan, "Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties" IEEE Transactions on Automatic Control, vol. 65, iss. 4.
doi: 10.1109/tac.2019.2923049
@Article{xue:reachable-sets:2020, author = {Xue, Bai and Fränzle, Martin and Zhan, Naijun}, title = {Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties}, journal = {IEEE Transactions on Automatic Control}, year = {2020}, volume = {65}, number = {4}, pages = {1468-1483}, doi = {10.1109/tac.2019.2923049}, url = {https://doi.org/10.1109/TAC.2019.2923049}, }
[inproceedings] bibtex
B. Xue, N. Zhan, und M. Fränzle, "Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems" in Proc. Proceedings of the 59th IEEE Conference on Decision and Control (CDC2020), 2020.
doi: 10.1109/CDC42340.2020.9304212
@InProceedings{xue:reach-avaoid-sets:2020, author = {Xue, Bai and Zhan, Naijun and Fränzle, Martin}, title = {Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems}, booktitle = {Proceedings of the 59th IEEE Conference on Decision and Control (CDC2020)}, year = {2020}, month = dec, abstract = {In this paper we propose a computational method based on semi-definite programming for synthesizing infinite-time reach-avoid sets in discrete-time polynomial systems. An infinite-time reach-avoid set is a set of initial states making the system eventually, i.e., within finite time enter the target set while remaining inside another specified (safe) set during each time step preceding the target hit. The reach-avoid set is first characterized equivalently as a strictly positive sub-level of a bounded value function, which in turn is shown to be a solution to a system of derived equations. The derived equations are further relaxed into a system of inequalities, which is encoded into semi-definite constraints based on the sum-of-squares decomposition for multivariate polynomials, such that the problem of synthesizing inner-approximations of the reach-avoid set can be addressed via solving a semi-definite programming problem. Two examples demonstrate the proposed approach.}, doi = {10.1109/CDC42340.2020.9304212}, }
[article] bibtex
A. Trende, F. Hartwich, C. Schmidt, und M. Fränzle, "Improving the detection of user uncertainty in automated overtaking maneuvers by combining contextual, physiological and individualized user data" Constantine Stephanidis and Margherita Antona, editors, HCI International 2020 - Posters, Cham, 2020, vol. Springer International Publishing.
@Article{trende:user-uncertainty:2020, author = {Trende, Alexander and Hartwich, Franziska and Schmidt, Cornelia and Fränzle, Martin}, title = {Improving the detection of user uncertainty in automated overtaking maneuvers by combining contextual, physiological and individualized user data}, journal = {Constantine Stephanidis and Margherita Antona, editors, HCI International 2020 - Posters, Cham, 2020}, year = {2020}, volume = {Springer International Publishing}, pages = {390-397}, }
[article] bibtex | Dokument aufrufen
B. Xue, M. Fränzle, N. Zhan, S. Bogomolov, und B. Xia, "Safety Verification for Random Ordinary Differential Equations" IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE T COMPUT AID D).
doi: document/9211452
@Article{xue:random-ode:2020, author = {Xue, Bai and Fränzle, Martin and Zhan, Naijun and Bogomolov, Sergiy and Xia, Bican}, title = {Safety Verification for Random Ordinary Differential Equations}, journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE T COMPUT AID D)}, year = {2020}, abstract = {Random ordinary differential equations (RODEs) are ordinary differential equations (ODEs) that contain a stochastic process in their vector field functions. They have been used for many years in a wide range of applications, but have been a shadow existence to stochastic differential equations (SDEs) despite being able to model a wider and often physically more adequate range of disturbances. In this article, we study the safety verification problem over both finite time horizons and the infinite time horizon for RODEs incorporating Wiener processes. Concretely, we investigate the ${p}$ -safety problem, where we identify the set of initial states from which the probability to satisfy safety specifications is at least ${p}$ . Based on identifying a set of sample paths whose probability measure is larger than ${p}$ , we propose a method of reducing stochastic reachability to adversary reachability of ODEs for solving the ${p}$ -safety problem over finite time horizons. This method permits an efficient lifting of reach-set computation methods for perturbed ODEs to RODEs. In this method, the ${p}$ -safety problem over finite time horizons is reduced to the problem of inner-approximating robust backward reachable sets for ODEs with time-varying perturbation inputs. We then extend the method to the ${p}$ -safety problem over the infinite time horizon. Finally, we demonstrate our method on several examples.}, doi = {https://ieeexplore.ieee.org/document/9211452}, type = {article}, url = {https://www.researchgate.net/publication/343006187_Safety_Verification_for_Random_Ordinary_Differential_Equations}, }
[inproceedings] bibtex
Y. Bebawy, H. Guissouma, S. V. Maelen, J. Kröger, G. Hake, I. Stierand, M. Fränzle, E. Sax, und A. Hahn, "Incremental Contract-based Verification of Software Updates for Safety-Critical Cyber-Physical Systems." 2020.
@InProceedings{bebawy:contract-based-verification:2020, author = {Bebawy, Yosab and Guissouma, Houssem and Maelen, Sebastian Vander and Kröger, Janis and Hake, Georg and Stierand, Ingo and Fränzle, Martin and Sax, Eric and Hahn, Axel}, title = {Incremental Contract-based Verification of Software Updates for Safety-Critical Cyber-Physical Systems}, year = {2020}, month = dec, organization = {The 2020 International Conference on Computational Science and Computational Intelligence (CSCI)}, }
[inproceedings] bibtex
S. vom Dorff, B. Böddeker, M. Kneißl, und M. Fränzle, "A Fail-safe Architecture for Automated Driving" in Proc. 2020 Design, Automation & Test in Europe Conference & Exhibition, 2020.
doi: 10.23919/date48585.2020.9116283
@InProceedings{dorff:architecture:2020, author = {vom Dorff, Sebastian and Böddeker, Bert and Kneißl, Maximilian and Fränzle, Martin}, title = {A Fail-safe Architecture for Automated Driving}, booktitle = {2020 Design, Automation \& Test in Europe Conference \& Exhibition}, year = {2020}, pages = {828-833}, month = mar, organization = {DATE 2020}, publisher = {IEEE}, doi = {10.23919/date48585.2020.9116283}, location = {Grenoble, France}, type = {inproceedings}, }
[inproceedings] bibtex
M. Fränzle und P. Kröger, "Guess What I'm Doing! - Rendering Formal Verification Methods Ripe for the Era of Interacting Intelligent Systems" in Proc. Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III, 2020.
doi: 10.1007/978-3-030-61467-6
@InProceedings{fraenzle:guess-what:2020, author = {Fränzle, Martin and Kröger, Paul}, title = {Guess What {I}'m Doing! - Rendering Formal Verification Methods Ripe for the Era of Interacting Intelligent Systems}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III}, year = {2020}, series = {Lecture Notes in Computer Science}, pages = {255-272}, month = oct, publisher = {Springer}, doi = {10.1007/978-3-030-61467-6}, type = {inproceedings}, }
[article] bibtex
M. Fränzle, K. Quaas, M. Shirmohammadi, und J. Worrell, "Effective definability of the reachability relation in timed automata" Inf. Process. Lett..
doi: 10.1016/j.ipl.2019.105871
@Article{fraenzle:reachability-relation:2020, author = {Fränzle, Martin and Quaas, Karin and Shirmohammadi, Mahsa and Worrell, James}, title = {Effective definability of the reachability relation in timed automata}, journal = {Inf. Process. Lett.}, year = {2020}, doi = {10.1016/j.ipl.2019.105871}, type = {article}, }
[inproceedings] bibtex
B. Koopmann, S. Puch, G. Ehmen, und M. Fränzle, "Cooperative Maneuvers of Highly Automated Vehicles at Urban Intersections: A Game-theoretic Approach" in Proc. Karsten Berns, Markus Helfert and Oleg Gusikhin editors: Proceedings of the 6th International Conference on Vehicle Technology and Intelligent Transport Systems (VEHITS'20), 2020.
doi: 10.5220/0009351500150026
@InProceedings{koopmann:manoeuvres:2020, author = {Koopmann, Björn and Puch, Stefan and Ehmen, Günter and Fränzle, Martin}, title = {Cooperative Maneuvers of Highly Automated Vehicles at Urban Intersections: A Game-theoretic Approach}, booktitle = {Karsten Berns, Markus Helfert and Oleg Gusikhin editors: Proceedings of the 6th International Conference on Vehicle Technology and Intelligent Transport Systems (VEHITS'20)}, year = {2020}, pages = {15-26}, month = {05}, organization = {INSTICC}, publisher = {SciTePress}, abstract = {In this paper, we propose an approach how connected and highly automated vehicles can perform cooperative maneuvers such as lane changes and left-turns at urban intersections where they have to deal with human-operated vehicles and vulnerable road users such as cyclists and pedestrians in so-called mixed traffic. In order to support cooperative maneuvers the urban intersection is equipped with an intelligent controller which has access to different sensors along the intersection to detect and predict the behavior of the traffic participants involved. Since the intersection controller cannot directly control all road users and - not least due to the legal situation - driving decisions must always be made by the vehicle controller itself, we focus on a decentralized control paradigm. In this context, connected and highly automated vehicles use some carefully selected game theory concepts to make the best possible and clear decisions about cooperative maneuvers. The aim is to improve traffic efficiency while maintaining road safety at the same time. Our first results obtained with a prototypical implementation of the approach in a traffic simulation are promising.}, doi = {10.5220/0009351500150026}, type = {inproceedings}, }
[inproceedings] bibtex
B. Kramer, C. Neurohr, M. Büker, E. Böde, M. Fränzle, und W. Damm, "Identification and Quantification of Hazardous Scenarios for Automated Driving" in Proc. In Mark Zeller and Kai Höfig, editors, Model - Based Safety and Assessment - 7th International Symposium, IMBSA 2020, Lisbon, Portugal, September 14-16, 2020, Proceedings, volume 12297 of Lecture Notes in Computer Science, 2020.
@InProceedings{kramer:hazardous-scenarios:2020, author = {Kramer, Birte and Neurohr, Christian and Büker, Matthias and Böde, Eckard and Fränzle, Martin and Damm, Werner}, title = {Identification and Quantification of Hazardous Scenarios for Automated Driving}, booktitle = {In Mark Zeller and Kai Höfig, editors, Model - Based Safety and Assessment - 7th International Symposium, IMBSA 2020, Lisbon, Portugal, September 14-16, 2020, Proceedings, volume 12297 of Lecture Notes in Computer Science}, year = {2020}, editor = {Zeller, Marc and Höfig, Kai}, pages = {163-178}, month = sep, publisher = {Springer}, location = {Lisbon, Portugal}, }
[article] bibtex | Dokument aufrufen
M. Fränzle, M. Shirmohammadi, M. Swaminathan, und J. Worrell, "Costs and rewards in priced timed automata" Information and Computation.
@Article{fraenzle:pta:2020, author = {Fränzle, Martin and Shirmohammadi, Mahsa and Swaminathan, Mani and Worrell, James}, title = {Costs and rewards in priced timed automata}, journal = {Information and Computation}, year = {2020}, abstract = {We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an ε-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert’s 10 th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.}, type = {article}, url = {https://www.researchgate.net/publication/338954820_Costs_and_Rewards_in_Priced_Timed_Automata}, }
[article] bibtex | Dokument aufrufen
M. Chen, M. Fränzle, Y. Li, P. N. Mosaad, und N. Zhan, "Indecision and delays are the parents of failure—taming them algorithmically by synthesizing delay-resilient control" Acta Informatica.
doi: 10.1007/s00236-020-00374-7
@Article{chen:delays:2020, author = {Chen, Mingshuai and Fränzle, Martin and Li, Yangjia and Mosaad, Peter Nazier and Zhan, Naijun}, title = {Indecision and delays are the parents of failure—taming them algorithmically by synthesizing delay-resilient control}, journal = {Acta Informatica}, year = {2020}, pages = {1-32}, abstract = {The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and adding an appropriate winning condition permits to specify desirable behavior. The classical model here is the positional game, where both players can (fully or partially) observe the current position in the game graph, which in turn is indicative of their mutual current states. In practice, neither sensing and actuating the environment through physical devices nor data forwarding to and from the controller and signal processing in the controller are instantaneous. The resultant delays force the controller to draw decisions before being aware of the recent history of a play and to submit these decisions well before they can take effect asynchronously. It is known that existence of a winning strategy for the controller in games with such delays is decidable over finite game graphs and with respect to ω-regular objectives. The underlying reduction, however, is impractical for non-trivial delays as it incurs a blow-up of the game graph which is exponential in the magnitude of the delay. For safety objectives, we propose a more practical incremental algorithm successively synthesizing a series of controllers handling increasing delays and reducing the game-graph size in between. It is demonstrated using benchmark examples that even a simplistic explicit-state implementation of this algorithm outperforms state-of-the-art symbolic synthesis algorithms as soon as non-trivial delays have to be handled. We furthermore address the practically relevant cases of non-order-preserving delays and bounded message loss, as arising in actual networked control, thereby considerably extending the scope of regular game theory under delay.}, doi = {https://doi.org/10.1007/s00236-020-00374-7}, type = {article}, url = {https://link.springer.com/article/10.1007/s00236-020-00374-7}, }
[inproceedings] bibtex
S. K. Sowe, M. Fränzle, J. P. Osterloh, A. Trende, L. Weber, und A. Lüdtke, "Challenges for Integrating Humans into Vehicular Cyber-Physical Systems" in Proc. Lecture Notes in Computer Science - Software Engineering and Formal Methods - SEFM 2019 Collocated Workshops: CoSim-CPS, ASYDE, CIFMA, and FOCLASA, Oslo, Norway, September 16–20, 2019, Revised Selected Papers, 2020.
doi: 10.1007/978-3-030-57506-9_2
@InProceedings{sowe:integrating-humans:2020, author = {Sowe, Sulayman K. and Fränzle, Martin and Osterloh, Jan Patrick and Trende, Alexander and Weber, Lars and Lüdtke, Andreas}, title = {Challenges for Integrating Humans into Vehicular Cyber-Physical Systems}, booktitle = {Lecture Notes in Computer Science - Software Engineering and Formal Methods - SEFM 2019 Collocated Workshops: CoSim-CPS, ASYDE, CIFMA, and FOCLASA, Oslo, Norway, September 16–20, 2019, Revised Selected Papers}, year = {2020}, series = {12226 LNCS}, pages = {20-26}, publisher = {Springer Science and Business Media Deutschland GmbH}, abstract = {Advances in Vehicular Cyber-Physical Systems (VCPS) are the primary enablers of the shift from no automation to fully autonomous vehicles (AVs). One of the impacts of this shift is to develop safe AVs in which most or all of the functions of the human driver are replaced with an intelligent system. However, while some progress has been made in equipping AVs with advanced AI capabilities, VCPS designers are still faced with the challenge of designing trustworthy AVs that are in sync with the unpredictable behaviours of humans. In order to address this challenge, we present a model that describes how a Human Ambassador component can be integrated into the overall design of a new generation of VCPS. A scenario is presented to demonstrate how the model can work in practice. Formalisation and co-simulation challenges associated with integrating the Human Ambassador component and future work we are undertaking are also discussed.}, doi = {10.1007/978-3-030-57506-9_2}, isbn = {9783030575052}, type = {inproceedings},

2019

[inproceedings] bibtex | Dokument aufrufen
A. Abate, H. Blom, N. Cauchi, K. Degiorgio, M. Fränzle, E. M. Hahn, S. Haesaert, H. Ma, M. Oishi, C. Pilch, A. Remke, M. Salamati, S. Soudjani, B. van Huijgevoort, und A. P. Vinod, "ARCH-COMP19 Category Report: Stochastic Modelling" in Proc. ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, part of CPS-IoT Week 2019, Montreal, QC, Canada, April 15, 2019, 2019.
@InProceedings{abate:archcomp:2019, author = {Abate, Alessandro and Blom, Henk and Cauchi, Nathalie and Degiorgio, Kurt and Fränzle, Martin and Hahn, Ernst Moritz and Haesaert, Sofie and Ma, Hao and Oishi, Meeko and Pilch, Carina and Remke, Anne and Salamati, Mahmoud and Soudjani, Sadegh and van Huijgevoort, Birgit and Vinod, Abraham P.}, title = {{ARCH-COMP19} Category Report: Stochastic Modelling}, booktitle = {{ARCH19.} 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, part of CPS-IoT Week 2019, Montreal, QC, Canada, April 15, 2019}, year = {2019}, editor = {Frehse, Goran and Althoff, Matthias}, volume = {61}, series = {EPiC Series in Computing}, pages = {62--102}, publisher = {EasyChair}, url = {http://www.easychair.org/publications/paper/S95M}, }
[techreport] bibtex | Dokument aufrufen
E. Böde, M. Büker, W. Damm, M. Fränzle, B. Kramer, C. Neurohr, und S. V. Maelen, "Identifikation und Quantifizierung von Automationsrisiken für hochautomatisierte Fahrfunktionen" , techreport , 2019.
@TechReport{boede:automationsrisiken:2019, author = {B{\"o}de, Eckard and B{\"u}ker, Matthias and Damm, Werner and Fr{\"a}nzle, Martin and Kramer, Birte and Neurohr, Christian and Maelen, Sebastian Vander}, title = {Identifikation und Quantifizierung von Automationsrisiken f{\"u}r hochautomatisierte Fahrfunktionen}, year = {2019}, type = {techreport}, month = jul, url = {https://www.pegasusprojekt.de/files/tmpl/pdf/PEGASUS_TechnicalReport_Automationsrisiken_17.07.2019.pdf}, }
[inbook] bibtex
E. Böde, W. Damm, G. Ehmen, M. Fränzle, K. Grüttner, P. Ittershagen, B. Josko, B. Koopmann, F. Poppen, M. Siegel, und I. Stierand, "MULTIC-Tooling." FAT-Schriftenreihe 316.
@InBook{boede:multic:2019, title = {MULTIC-Tooling}, publisher = {FAT-Schriftenreihe 316}, year = {2019}, author = {B{\"o}de, Eckard and Damm, Werner and Ehmen, G{\"u}nter and Fr{\"a}nzle, Martin and Gr{\"u}ttner, Kim and Ittershagen, Philipp and Josko, Bernhard and Koopmann, Bj{\"o}rn and Poppen, Frank and Siegel, Michael and Stierand, Ingo}, month = jun, }
[inproceedings] bibtex
M. Büker, B. Kramer, E. Böde, S. V. Mealen, und M. Fränzle, "Identifikation von Automationsrisiken hochautomatischer Fahrfunktionen in PEGASUS" in Proc. AAET Automatisiertes und vernetztes Fahren, 2019.
@InProceedings{bueker:pegasus:2019, author = {Matthias B{\"u}ker and Birte Kramer and Eckard B{\"o}de and Sebastian Vander Mealen and Martin Fr{\"a}nzle}, title = {Identifikation von Automationsrisiken hochautomatischer Fahrfunktionen in PEGASUS}, booktitle = {AAET Automatisiertes und vernetztes Fahren}, year = {2019}, pages = {315- 329}, publisher = {ITS mobility e. V.}, abstract = {Die Identifikation von Automationsrisiken bedient sich einer iterativen erweiterten Sicherheitsanalyse. Sie dient dem Ziel, Ursachen f{\"u}r Risiken, die durch die Einf{\"u}hrung hochautomatisierter Fahrfunktionen (HAF-Funktionen) entstehen fr{\"u}hzeitig zu identifizieren. Im Rahmen der Analyse werden insbesondere die f{\"u}r eine Gef{\"a}hrdung urs{\"a}chlichen Umgebungsbedingungen identifiziert und in Form von Parameterbereichen logischer Szenarien (Bagschik, et al.\ 2017) beschrieben. Dies erm{\"o}glicht im sp{\"a}teren Testprozess ein zielgerichtetes Testen und belegt eine hinreichende Testfallabdeckung.}, type = {inproceedings}, }
[article] bibtex
W. Damm, M. Fränzle, W. Hagemann, P. Kröger, und A. Rakow, "Justification Based Reasoning in Dynamic Conflict Resolution" CoRR abs/1905.11764.
@Article{damm:dcr:2019, author = {Damm, Werner and Fr{\"a}nzle, Martin and Hagemann, Willem and Kr{\"o}ger, Paul and Rakow, Astrid}, title = {Justification Based Reasoning in Dynamic Conflict Resolution}, journal = {CoRR abs/1905.11764}, year = {2019}, }
[inproceedings] bibtex | Dokument aufrufen
W. Damm, M. Fränzle, W. Hagemann, P. Kröger, und A. Rakow, "Dynamic Conflict Resolution Using Justification Based Reasoning" in Proc. Proceedings of the 4th Workshop on Formal Reasoning about Causation, Responsibility, and Explanations in Science and Technology, CREST@ETAPS 2019, Prague, Czech Republic, 7th April 2019, 2019.
doi: 10.4204/eptcs.308.4
@InProceedings{damm:dcr-crest:2019, author = {Damm, Werner and Fr{\"a}nzle, Martin and Hagemann, Willem and Kr{\"o}ger, Paul and Rakow, Astrid}, title = {Dynamic Conflict Resolution Using Justification Based Reasoning}, booktitle = {Proceedings of the 4th Workshop on Formal Reasoning about Causation, Responsibility, and Explanations in Science and Technology, CREST@ETAPS 2019, Prague, Czech Republic, 7th April 2019}, year = {2019}, editor = {Caltais, Georgiana and Krivine, Jean}, volume = {308}, series = {{EPTCS}}, pages = {47--65}, month = apr, doi = {10.4204/eptcs.308.4}, url = {https://doi.org/10.4204/EPTCS.308.4}, }
[inproceedings] bibtex
W. Damm, M. Fränzle, A. Lüdtke, J. W. Rieger, A. Trende, und A. Unni, "Integrating Neurophysiological Sensors and Driver Models for Safe and Performant Automated Vehicle Control in Mixed Traffic" , Paris, 2019.
@InProceedings{damm:neurosensors:2019, author = {Damm, Werner and Fr{\"a}nzle, Martin and L{\"u}dtke, Andreas and Rieger, Jochem W. and Trende, Alexander and Unni, Anirudh}, title = {Integrating Neurophysiological Sensors and Driver Models for Safe and Performant Automated Vehicle Control in Mixed Traffic}, year = {2019}, pages = {82-89}, address = {Paris}, organization = {IEEE}, journal = {Intelligent Vehicles Symposium (IV 2019)}, }
[inproceedings] bibtex | Dokument aufrufen
S. Feng, M. Chen, N. Zhan, M. Fränzle, und B. Xue, "Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations" in Proc. Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, 2019.
doi: 10.1007/978-3-030-25540-4_37
@InProceedings{feng:delays:2019, author = {Feng, Shenghua and Chen, Mingshuai and Zhan, Naijun and Fr{\"a}nzle, Martin and Xue, Bai}, title = {Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations}, booktitle = {Computer Aided Verification - 31st International Conference, {CAV} 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part {I}}, year = {2019}, editor = {Dillig, Isil and Tasiran, Serdar}, volume = {11561}, series = {Lecture Notes in Computer Science}, pages = {650--669}, publisher = {Springer}, doi = {10.1007/978-3-030-25540-4\_37}, url = {https://doi.org/10.1007/978-3-030-25540-4\_37}, }
[article] bibtex | Dokument aufrufen
M. Fränzle, M. Chen, und P. Kröger, "In Memory of Oded Maler: Automatic Reachability Analysis of Hybrid-state Automata" ACM SIGLOG News, vol. 6, iss. 1.
doi: 10.1145/3313909.3313913
@Article{fraenzle:automatic-reachability:2019, author = {Fr\"{a}nzle, Martin and Chen, Mingshuai and Kr\"{o}ger, Paul}, title = {In Memory of Oded Maler: Automatic Reachability Analysis of Hybrid-state Automata}, journal = {ACM SIGLOG News}, year = {2019}, volume = {6}, number = {1}, pages = {19--39}, month = feb, issn = {2372-3491}, acmid = {3313913}, address = {New York, NY, USA}, doi = {10.1145/3313909.3313913}, file = {Read version:/home/pkroeger/syncdoc/docbook/bibtex/pdf/fraenzle_automatic-reachability_2019_read.pdf:PDF;Original version:/home/pkroeger/syncdoc/docbook/bibtex/pdf/fraenzle_automatic-reachability_2019.pdf:PDF}, issue_date = {January 2019}, numpages = {21}, publisher = {ACM}, url = {http://doi.acm.org/10.1145/3313909.3313913}, }
[article] bibtex | Dokument aufrufen
M. Fränzle, K. Quaas, M. Shirmohammadi, und J. Worrell, "Effective Definability of the Reachability Relation in Timed Automata" CoRR, vol. abs/1903.09773.
@Article{fraenzle:definability:2019, author = {Fr{\"a}nzle, Martin and Quaas, Karin and Shirmohammadi, Mahsa and Worrell, James}, title = {Effective Definability of the Reachability Relation in Timed Automata}, journal = {CoRR}, year = {2019}, volume = {abs/1903.09773}, archiveprefix = {arXiv}, eprint = {1903.09773}, url = {http://arxiv.org/abs/1903.09773}, }
[article] bibtex | Dokument aufrufen
E. Polgreen, M. Brain, M. Fränzle, und A. Abate, "Verifying Reachability Properties in Markov Chains via Incremental Induction" CoRR, vol. abs/1909.08017.
@Article{polgreen:reachability-mc:2019, author = {Polgreen, Elizabeth and Brain, Martin and Fr{\"a}nzle, Martin and Abate, Alessandro}, title = {Verifying Reachability Properties in Markov Chains via Incremental Induction}, journal = {CoRR}, year = {2019}, volume = {abs/1909.08017}, archiveprefix = {arXiv}, eprint = {1909.08017}, url = {http://arxiv.org/abs/1909.08017}, }
[phdthesis] bibtex | Dokument aufrufen
S. Puch, "Statistisches Model Checking mittels geführter Simulation im Kontext modellbasierter Entwicklung sicherheitskritischer Fahrerassistenzsysteme" PhD Thesis , 2019.
@PhdThesis{puch:smc:2019, author = {Stefan Puch}, title = {{Statistisches Model Checking mittels gef{\"u}hrter Simulation im Kontext modellbasierter Entwicklung sicherheitskritischer Fahrerassistenzsysteme}}, school = {Carl von Ossietzky Universit{\"a}t Oldenburg}, year = {2019}, abstract = {Die vorliegende Arbeit f{\"u}hrt eine Methodik ein, welche mit Statistischem Model Checking im Rahmen von gef{\"u}hrter Simulation seltene Ereignisse erfassen kann. Ein Kosimulationsframework auf Basis der High Level Architecture erm{\"o}glicht eine aus Fahrermodell, Fahrsimulationssoftware und Fahrerassistenzsystem bestehende Kosimulation, die von dem auf Adaptive Importance Sampling basierenden Threshold Uncertainty Tree Search (TUTS) Algorithmus mit Hilfe einer Kritikalit{\"a}tsfunktion zu seltenen Ereignissen gef{\"}hrt wird. Anhand eines Fahrer-Fahrzeug-Assistenzsystem-Szenarios k{\"o}nnen seltene Ereignisse mit einer Wahrscheinlichkeit deutlich kleiner als $10^{-9}$ erfasst werden. Nach einer mathematischen R{\"u}ckrechnung der gef{\"}hrten Simulationsergebnisse, erfolgt eine quantitative Absch{\"a}tzung mittels $99\%$igem Konfidenzniveaus mit welcher Sicherheit das vorliegende Ergebnis zutreffend ist. Eine {\"U}bertragbarkeit der Methodik auf weitere Dom{\"a}nen erfolgt anhand eines Benchmarks, bei dem die Wahrscheinlichkeit zu sch{\"a}tzen ist, mit der ein zuf{\"a}llig springender Ball ein winziges Loch trifft.}, file = {Read version:/home/pkroeger/syncdoc/docbook/bibtex/pdf/puch_smc_2019_read.pdf:PDF;Original version:/home/pkroeger/syncdoc/docbook/bibtex/pdf/puch_smc_2019.pdf:PDF}, url = {http://oops.uni-oldenburg.de/4213/1/pucsta19.pdf}, }
[inproceedings] bibtex
S. K. Sowe, M. Fränzle, J. Osterloh, A. Trende, L. Weber, und A. Lüdtke, "Challenges for Integrating Humans into Vehicular Cyber-Physical Systems." 2019.
@InProceedings{sowe:challenges:2019, author = {Sowe, Sulayman K. and Fr{\"a}nzle, Martin and Osterloh, Jan-Patrick and Trende, Alexander and Weber, Lars and L{\"u}dtke, Andreas}, title = {Challenges for Integrating Humans into Vehicular Cyber-Physical Systems}, year = {2019}, series = {The 17th edition of the International Conference on Software Engineering and Formal Methods}, month = {09}, location = {Oslo, Norway}, }
[inproceedings] bibtex | Dokument aufrufen
B. Xue, M. Fränzle, H. Zhao, N. Zhan, und A. Easwaran, "Probably Approximate Safety Verification of Hybrid Dynamical Systems" in Proc. Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, 2019.
doi: 10.1007/978-3-030-32409-4_15
@InProceedings{xue:pasv:2019, author = {Xue, Bai and Fr{\"a}nzle, Martin and Zhao, Hengjun and Zhan, Naijun and Easwaran, Arvind}, title = {Probably Approximate Safety Verification of Hybrid Dynamical Systems}, booktitle = {Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, {ICFEM} 2019, Shenzhen, China, November 5-9, 2019, Proceedings}, year = {2019}, editor = {Ameur, Yamine A{\"\i}t and Qin, Shengchao}, volume = {11852}, series = {Lecture Notes in Computer Science}, pages = {236--252}, publisher = {Springer}, doi = {10.1007/978-3-030-32409-4\_15}, url = {https://doi.org/10.1007/978-3-030-32409-4\_15}, }
[inproceedings] bibtex | Dokument aufrufen
B. Xue, Q. Wang, N. Zhan, und M. Fränzle, "Robust Invariant Sets Generation for State-constrained Perturbed Polynomial Systems" in Proc. Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, 2019.
doi: 10.1145/3302504.3311810
@InProceedings{xue:invariant-sets:2019, author = {Xue, Bai and Wang, Qiuye and Zhan, Naijun and Fr{\"a}nzle, Martin}, title = {Robust Invariant Sets Generation for State-constrained Perturbed Polynomial Systems}, booktitle = {Proceedings of the 22nd {ACM} International Conference on Hybrid Systems: Computation and Control, {HSCC} 2019, Montreal, QC, Canada, April 16-18, 2019}, year = {2019}, editor = {Ozay, Necmiye and Prabhakar, Pavithra}, pages = {128--137}, publisher = {{ACM}}, doi = {10.1145/3302504.3311810}, url = {https://doi.org/10.1145/3302504.3311810}, }
[article] bibtex | Dokument aufrufen
M. Fränzle, J. Tegtmeier, M. Käsberg, und M. Eicher, "Funktionale Sicherheit automatisierter, vernetzter Fahrzeuge" Karsten Lemmer editor: Neue autoMobilität II. Kooperativer Straßenverkehr und intelligente Verkehrssteuerung für die Mobilität der Zukunft (acatech Studie).
@Article{fraenzle:funktionale-sicherheit:2019, author = {Fränzle, Martin and Tegtmeier, Jörg and Käsberg, Mirco and Eicher, Matthis}, title = {Funktionale Sicherheit automatisierter, vernetzter Fahrzeuge}, journal = {Karsten Lemmer editor: Neue autoMobilität II. Kooperativer Straßenverkehr und intelligente Verkehrssteuerung für die Mobilität der Zukunft (acatech Studie)}, year = {2019}, pages = {52-56, chapter 5.2}, month = nov, publisher = {Utzverlag GmbH, München}, url = {https://www.acatech.de/publikation/neue-automobilitaet-ii/}, }
[article] bibtex
J. Sztipanovits, X. D. Koutsoukos, G. Karsai, S. Sastry, C. Tomlin, W. Damm, M. Fränzle, J. W. Rieger, A. Pretschner, und F. Köster, "Science of design for societal-scale cyber-physical systems: challenges and opportunities" Cyber-Physical Systems.
doi: 10.1080/23335777.2019.1624619
@Article{sztipanovits:societal-scale-cps:2019, author = {Sztipanovits, Janos and Koutsoukos, Xenofon D. and Karsai, Gabor and Sastry, Shankar and Tomlin, Claire and Damm, Werner and Fränzle, Martin and Rieger, Jochem W. and Pretschner, Alexander and Köster, Frank}, title = {Science of design for societal-scale cyber-physical systems: challenges and opportunities}, journal = {Cyber-Physical Systems}, year = {2019}, pages = {145-172}, month = jun, abstract = {Emerging industrial platforms such as the Internet of Things (IoT), Industrial Internet (II) in the US and Industrie 4.0 in Europe have tremendously accelerated the development of new generations of Cyber-Physical Systems (CPS) that integrate humans and human organizations (H-CPS) with physical and computation processes and extend to societal-scale systems such as traffic networks, electric grids, or networks of autonomous systems where control is dynamically shifted between humans and machines. Although such societal-scale CPS can potentially affect many aspect of our lives, significant societal strains have emerged about the new technology trends and their impact on how we live. Emerging tensions extend to regulations, certification, insurance, and other societal constructs that are necessary for the widespread adoption of new technologies. If these systems evolve independently in different parts of the world, they will ‘hard-wire’ the social context in which they are created, making interoperation hard or impossible, decreasing reusability, and narrowing markets for products and services. While impacts of new technology trends on social policies have received attention, the other side of the coin – to make systems adaptable to social policies – is nearly absent from engineering and computer science design practice. This paper focuses on technologies that can be adapted to varying public policies and presents (1) hard problems and technical challenges and (2) some recent research approaches and opportunities. The central goal of this paper is to discuss the challenges and opportunities for constructing H-CPS that can be parameterized by social context. The focus in on three major application domains: connected vehicles, transactive energy systems, and unmanned aerial vehicles. Abbreviations: CPS: Cyber-physical systems; H-CPS: Human-cyber-physical systems; CV: Connected vehicle; II: Industrial Internet; IoT: Internet of Things}, doi = {10.1080/23335777.2019.1624619},

2018

[article] bibtex | Dokument aufrufen
M. Abdelaal, M. Fränzle, und A. Hahn, "Nonlinear Model Predictive Control for trajectory tracking and collision avoidance of underactuated vessels with disturbances" Ocean Engineering, vol. 160.
doi: 10.1016/j.oceaneng.2018.04.026
@Article{abdelaal:mpc:2018, author = {Mohamed Abdelaal and Martin Fränzle and Axel Hahn}, title = {Nonlinear Model Predictive Control for trajectory tracking and collision avoidance of underactuated vessels with disturbances}, journal = {Ocean Engineering}, year = {2018}, volume = {160}, pages = {168 - 180}, issn = {0029-8018}, abstract = {This paper presents a combined Nonlinear Model Predictive Control (NMPC) for position and velocity tracking of underactuated surface vessels, and collision avoidance of static and dynamic objects into a single control scheme with sideslip angle compensation and environmental disturbances counteraction. A three-degree-of-freedom (3-DOF) dynamic model is used with only two control variables: namely, surge force and yaw moment. External environmental forces are considered as constant or slowly varying disturbances with respect to the inertial frame, and hence nonlinear for the body frame of the vessel. Nonlinear disturbance observer (NDO) is used to estimate these disturbances in order to be fed into the prediction model and enhance the robustness of the controller. A nonlinear optimization problem is formulated to minimize the deviation of the vessel states from a time varying reference generated over a finite horizon by a virtual vessel. Sideslip angle is considered in the cost function formulation to account for tracking error caused by the transverse external force in the absence of sway control force. Collision avoidance is embedded into the trajectory tracking control problem as a time-varying nonlinear constraint of position states to account for static and dynamic obstacles. MATLAB simulations are used to assess the validity of the proposed technique.}, doi = {https://doi.org/10.1016/j.oceaneng.2018.04.026}, keywords = {Nonlinear model predictive control (NMPC), Nonlinear disturbance obersver (NDO), Collision avoidance, Trajectory tracking, Underactuated vessel}, url = {http://www.sciencedirect.com/science/article/pii/S002980181830458X}, }
[inproceedings] bibtex | Dokument aufrufen
E. Böde, M. Büker, U. Eberle, M. Fränzle, S. Gerwinn, und B. Kramer, "Efficient Splitting of Test and Simulation Cases for the Verification of Highly Automated Driving Functions" in Proc. Computer Safety, Reliability, and Security, Cham, 2018.
doi: 10.1007/978-3-319-99130-6_10
@InProceedings{boede:splitting:2018, author = {B{\"o}de, Eckard and B{\"u}ker, Matthias and Eberle, Ulrich and Fr{\"a}nzle, Martin and Gerwinn, Sebastian and Kramer, Birte}, title = {Efficient Splitting of Test and Simulation Cases for the Verification of Highly Automated Driving Functions}, booktitle = {Computer Safety, Reliability, and Security}, year = {2018}, editor = {Gallina, Barbara and Skavhaug, Amund and Bitsch, Friedemann}, pages = {139--153}, address = {Cham}, publisher = {Springer International Publishing}, abstract = {We address the question of feasibility of tests to verify highly automated driving functions by optimizing the trade-off between virtual tests for verifying safety properties and physical tests for validating the models used for such verification. We follow a quantitative approach based on a probabilistic treatment of the different quantities in question. That is, we quantify the accuracy of a model in terms of its probabilistic prediction ability. Similarly, we quantify the compliance of a system with its requirements in terms of the probability of satisfying these requirements. Depending on the costs of an individual virtual and physical test we are then able to calculate an optimal trade-off between physical and virtual tests, yet guaranteeing a probability of satisfying all requirements.}, doi = {10.1007/978-3-319-99130-6_10}, isbn = {978-3-319-99130-6}, url = {https://doi.org/10.1007/978-3-319-99130-6_10}, }
[inproceedings] bibtex | Dokument aufrufen
M. Chen, M. Fränzle, Y. Li, P. N. Mosaad, und N. Zhan, "What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed Interaction" in Proc. Automated Technology for Verification and Analysis, Cham, 2018.
doi: 10.1007/978-3-030-01090-4_4
@InProceedings{chen:unsure:2018, author = {Chen, Mingshuai and Fr{\"a}nzle, Martin and Li, Yangjia and Mosaad, Peter N. and Zhan, Naijun}, title = {What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed Interaction}, booktitle = {Automated Technology for Verification and Analysis}, year = {2018}, editor = {Lahiri, Shuvendu K. and Wang, Chao}, pages = {56--74}, address = {Cham}, publisher = {Springer International Publishing}, abstract = {The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and adding an appropriate winning condition permits to specify desirable behavior. The classical model here is the positional game, where both players can (fully or partially) observe the current position in the game graph, which in turn is indicative of their mutual current states. In practice, neither sensing or actuating the environment through physical devices nor data forwarding to and signal processing in the controller are instantaneous. The resultant delays force the controller to draw decisions before being aware of the recent history of a play. It is known that existence of a winning strategy for the controller in games with such delays is decidable over finite game graphs and with respect to {\$}{\$}{\backslash}omega {\$}{\$}-regular objectives. The underlying reduction, however, is impractical for non-trivial delays as it incurs a blow-up of the game graph which is exponential in the magnitude of the delay. For safety objectives, we propose a more practical incremental algorithm synthesizing a series of controllers handling increasing delays and reducing game-graph size in between. It is demonstrated using benchmark examples that even a simplistic explicit-state implementation of this algorithm outperforms state-of-the-art symbolic synthesis algorithms as soon as non-trivial delays have to be handled. We furthermore shed some light on the practically relevant case of non-order-preserving delays, as arising in actual networked control, thereby considerably extending the scope of regular game theory under delay pioneered by Klein and Zimmermann.}, doi = {10.1007/978-3-030-01090-4_4}, isbn = {978-3-030-01090-4}, url = {https://doi.org/10.1007/978-3-030-01090-4_4}, }
[inproceedings] bibtex | Dokument aufrufen
W. Damm, M. Fränzle, S. Gerwinn, und P. Kröger, "Perspectives on the Validation and Verification of Machine Learning Systems in the Context of Highly Automated Vehicles" in Proc. 2018 AAAI Spring Symposia, Stanford University, Palo Alto, California, USA, March 26-28, 2018, 2018.
@InProceedings{damm:vv4ml:2018, author = {Werner Damm and Martin Fr{\"a}nzle and Sebastian Gerwinn and Paul Kr{\"o}ger}, title = {Perspectives on the Validation and Verification of Machine Learning Systems in the Context of Highly Automated Vehicles}, booktitle = {{2018 {AAAI} Spring Symposia, Stanford University, Palo Alto, California, USA, March 26-28, 2018}}, year = {2018}, series = {AAAI Spring Symposium Series}, pages = {512-515}, publisher = {{{AAAI} Press}}, abstract = {Algorithms incorporating learned functionality play an increasingly important role for highly automated vehicles. Their impressive performance within environmental perception and other tasks central to automated driving comes at the price of a hitherto unsolved functional verification problem within safety analysis. We propose to combine statistical guarantee statements about the generalisation ability of learning algorithms with the functional architecture as well as constraints about the dynamics and ontology of the physical world, yielding an integrated formulation of the safety verification problem of functional architectures comprising artificial intelligence components. Its formulation as a probabilistic constraint system enables calculation of low risk manoeuvres. We illustrate the proposed scheme on a simple automotive scenario featuring unreliable environmental perception.}, type = {techreport}, url = {https://aaai.org/ocs/index.php/SSS/SSS18/paper/view/17526}, }
[article] bibtex | Dokument aufrufen
M. Fränzle, A. Girard, J. Lygeros, und S. Sankaranarayanan, "Special issue on Hybrid Systems: Computation and Control" Nonlinear Analysis: Hybrid Systems, vol. 27.
doi: 10.1016/j.nahs.2017.07.001
@Article{fraenzle:special-issue:2018, author = {Martin Fränzle and Antoine Girard and John Lygeros and Sriram Sankaranarayanan}, title = {Special issue on Hybrid Systems: Computation and Control}, journal = {Nonlinear Analysis: Hybrid Systems}, year = {2018}, volume = {27}, pages = {174 - 176}, issn = {1751-570X}, doi = {https://doi.org/10.1016/j.nahs.2017.07.001}, url = {http://www.sciencedirect.com/science/article/pii/S1751570X17300547}, }
[inproceedings] bibtex | Dokument aufrufen
M. Fränzle und P. Kröger, "The Demon, the Gambler, and the Engineer - Reconciling Hybrid-System Theory with Metrology" in Proc. Symposium on Real-Time and Hybrid Systems, Cham, 2018.
doi: 10.1007/978-3-030-01461-2_9
@InProceedings{fraenzle:bha:2018, author = {Martin Fr{\"a}nzle and Paul Kr{\"o}ger}, title = {The Demon, the Gambler, and the Engineer - Reconciling Hybrid-System Theory with Metrology}, booktitle = {Symposium on Real-Time and Hybrid Systems}, year = {2018}, editor = {Cliff Jones and Ji Wang and Naijun Zhan}, volume = {11180}, series = {Theoretical Computer Science and General Issues}, pages = {165-185}, address = {Cham}, publisher = {Springer International Publishing}, doi = {10.1007/978-3-030-01461-2_9}, url = {https://doi.org/10.1007/978-3-030-01461-2_9}, }
[inproceedings] bibtex | Dokument aufrufen
M. Fränzle, M. Shirmohammadi, M. Swaminathan, und J. Worrell, "Costs and Rewards in Priced Timed Automata" in Proc. 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018), Dagstuhl, Germany, 2018.
doi: 10.4230/LIPIcs.ICALP.2018.125
@InProceedings{fraenzle:rewards-pta:2018, author = {Martin Fr{\"a}nzle and Mahsa Shirmohammadi and Mani Swaminathan and James Worrell}, title = {{Costs and Rewards in Priced Timed Automata}}, booktitle = {45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)}, year = {2018}, editor = {Ioannis Chatzigiannakis and Christos Kaklamanis and D{\'a}niel Marx and Donald Sannella}, volume = {107}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, pages = {125:1--125:14}, address = {Dagstuhl, Germany}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, annote = {Keywords: Priced Timed Automata, Pareto Domination, Diophantine Equations}, doi = {10.4230/LIPIcs.ICALP.2018.125}, isbn = {978-3-95977-076-7}, issn = {1868-8969}, url = {http://drops.dagstuhl.de/opus/volltexte/2018/9129}, urn = {urn:nbn:de:0030-drops-91297}, }
[article] bibtex | Dokument aufrufen
M. Fränzle, M. Shirmohammadi, M. Swaminathan, und J. Worrell, "Costs and Rewards in Priced Timed Automata" CoRR, vol. abs/1803.01914.
@Article{fraenzle:rewards-pta-corr:2018, author = {Martin Fr{\"{a}}nzle and Mahsa Shirmohammadi and Mani Swaminathan and James Worrell}, title = {Costs and Rewards in Priced Timed Automata}, journal = {CoRR}, year = {2018}, volume = {abs/1803.01914}, archiveprefix = {arXiv}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/bib/journals/corr/abs-1803-01914}, eprint = {1803.01914}, url = {http://arxiv.org/abs/1803.01914}, }
[article] bibtex | Dokument aufrufen
S. Khan, M. Alam, M. Fränzle, N. Müllner, und Y. Chen, "A Traffic Aware Segment-based Routing protocol for VANETs in urban scenarios" Computers & Electrical Engineering, vol. 68.
doi: 10.1016/j.compeleceng.2018.04.017
@Article{khan:traffic-aware:2018, author = {Saifullah Khan and Muhammad Alam and Martin Fränzle and Nils Müllner and Yuanfang Chen}, title = {A Traffic Aware Segment-based Routing protocol for VANETs in urban scenarios}, journal = {Computers \& Electrical Engineering}, year = {2018}, volume = {68}, pages = {447 - 462}, issn = {0045-7906}, abstract = {Vehicular ad-hoc networks (VANETs) offer a diverse set of applications and therefore gain more and more attention from both academic and industrial communities. However, the deployment of VANETs is not very straight-forward. One challenge is highlighted by an uphill task of establishing and subsequently sustaining a robust communication. The need to obviate extra relay infrastructure in dynamically fluctuating topologies plus concurring shielding obstacles only magnifies this arduous task. In this context, information about traffic-density and about its estimated progress are valuable assets to tackle this issue. This paper proposes a novel routing protocol called Traffic Aware Segment-based Routing (TASR) protocol. The proposed protocol comprises two major parts: 1) Real-time vehicular traffic information for route selection allows for calculating the Expected Connectivity Degree (ECD) on different segments, and 2) a new forwarding method based on geographical information transfers packets from source to destination node. The new metric ECD takes vehicle densities into account, estimating the connectivity on each segment and thus the connectivity of nodes and data delivery ratio for transmitting packets. Furthermore, extensive simulations help analyzing the efficiency of TASR, indicating that it outperforms competing routing protocols.}, doi = {https://doi.org/10.1016/j.compeleceng.2018.04.017}, keywords = {Routing protocol, Vehicular ad hoc networks, Medium access, Wireless communication}, url = {http://www.sciencedirect.com/science/article/pii/S0045790617337047}, }
[inproceedings] bibtex
M. Li, P. N. Mosaad, M. Fränzle, Z. She, und B. Xue, "Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems" in Proc. Formal Modeling and Analysis of Timed Systems, Cham, 2018.
@InProceedings{li:safe-approx:2018, author = {Li, Meilun and Mosaad, Peter N. and Fr{\"a}nzle, Martin and She, Zhikun and Xue, Bai}, title = {Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems}, booktitle = {Formal Modeling and Analysis of Timed Systems}, year = {2018}, editor = {Jansen, David N. and Prabhakar, Pavithra}, pages = {252--270}, address = {Cham}, publisher = {Springer International Publishing}, abstract = {We present a method based on the Hamilton-Jacobi framework that is able to compute over- and under-approximations of reachable sets for autonomous dynamical systems beyond polynomial dynamics. The method does not resort to user-supplied candidate polynomials, but rather relies on an expansion of the evolution function whose convergence in compact state space is guaranteed. Over- and under-approximations of the reachable state space up to any designated precision can consequently be obtained based on truncations of that expansion. As the truncations used in computing over- and under-approximations as well as their associated error bounds agree, double-sided enclosures of the true reach-set can be computed in a single sweep. We demonstrate the precision of the enclosures thus obtained by comparison of benchmark results to related simulations.}, isbn = {978-3-030-00151-3}, }
[inproceedings] bibtex | Dokument aufrufen
S. Puch, M. Fränzle, und S. Gerwinn, "Quantitative Risk Assessment of Safety-critical Systems via Guided Simulation for Rare Events" in Proc. Leveraging Applications of Formal Methods, Verification and Validation. Verification, Cham, 2018.
doi: 10.1007/978-3-030-03421-4_20
@InProceedings{fraenzle:guided-simulation:2018, author = {Stefan Puch and Martin Fr{\"a}nzle and Sebastian Gerwinn}, title = {Quantitative Risk Assessment of Safety-critical Systems via Guided Simulation for Rare Events}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Verification}, year = {2018}, editor = {Margaria, Tiziana and Steffen, Bernhard}, pages = {305--321}, address = {Cham}, publisher = {Springer International Publishing}, abstract = {For developers of assisted or automated driving systems, gaining specific feedback and quantitative figures on the safety impact of the systems under development is crucial. However, obtaining such data from simulation of their design models is a complex and often time-consuming process. Especially when data of interest hinge on extremely rare events, an estimation of potential risks is highly desirable but a non-trivial task lacking easily applicable methods. In this paper we describe how a quantitative statement for a risk estimation involving extremely rare events can be obtained by guiding simulation based on reinforcement learning. The method draws on variance reduction and importance sampling, yet applies different optimization principles than related methods, like the cross-entropy methods against which we compare. Our rationale for optimizing differently is that in quantitative system verification, a sharper upper bound of the confidence interval is of higher relevance than the total width of the confidence interval.}, doi = {10.1007/978-3-030-03421-4_20}, url = {https://doi.org/10.1007/978-3-030-03421-4_20}, }
[article] bibtex | Dokument aufrufen
B. Xue, M. Fränzle, und N. Zhan, "Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties" arXiv e-prints.
@Article{xue:inner-approx:2018, author = {{Xue}, Bai and {Fr{\"a}nzle}, Martin and {Zhan}, Naijun}, title = {{Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties}}, journal = {arXiv e-prints}, year = {2018}, month = Nov, adsnote = {Provided by the SAO/NASA Astrophysics Data System}, adsurl = {https://ui.adsabs.harvard.edu/\#abs/2018arXiv181101086X}, archiveprefix = {arXiv}, eid = {arXiv:1811.01086}, eprint = {1811.01086}, keywords = {Mathematics - Optimization and Control}, primaryclass = {math.OC}, url = {https://arxiv.org/abs/1811.01086} }
[inproceedings] bibtex | Dokument aufrufen
B. Xue, M. Fränzle, und N. Zhan, "Under-Approximating Reach Sets for Polynomial Continuous Systems" in Proc. Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week), New York, NY, USA, 2018.
doi: 10.1145/3178126.3178133
@InProceedings{xue:under-approx:2018, author = {Xue, Bai and Fr\"{a}nzle, Martin and Zhan, Naijun}, title = {Under-Approximating Reach Sets for Polynomial Continuous Systems}, booktitle = {Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week)}, year = {2018}, series = {HSCC '18}, pages = {51--60}, address = {New York, NY, USA}, publisher = {ACM}, acmid = {3178133}, doi = {10.1145/3178126.3178133}, isbn = {978-1-4503-5642-8}, location = {Porto, Portugal}, numpages = {10}, url = {http://doi.acm.org/10.1145/3178126.3178133}, }
[article] bibtex | Dokument aufrufen
B. Xue, Q. Wang, N. Zhan, und M. Fränzle, "Reach-Avoid Differential Games Based on Invariant Generation" arXiv e-prints.
@Article{xue:diff-games:2018, author = {{Xue}, Bai and {Wang}, Qiuye and {Zhan}, Naijun and {Fr{\"a}nzle}, Martin}, title = {{Reach-Avoid Differential Games Based on Invariant Generation}}, journal = {arXiv e-prints}, year = {2018}, month = Nov, adsnote = {Provided by the SAO/NASA Astrophysics Data System}, adsurl = {https://ui.adsabs.harvard.edu/\#abs/2018arXiv181103215X}, archiveprefix = {arXiv}, eid = {arXiv:1811.03215}, eprint = {1811.03215}, keywords = {Mathematics - Optimization and Control}, primaryclass = {math.OC}, url = {https://arxiv.org/abs/1811.03215},

2017

[inproceedings] bibtex | Dokument aufrufen
N. Müllner, S. Khan, M. H. Rahman, W. Afzal, und M. Saadatmand, "Simulation-Based Safety Testing Brake-By-Wire" in Proc. International Conference on Software Testing, Verification and Validation Workshops, ICST, 2017.
@INPROCEEDINGS{, author = {M{\"{u}}llner, Nils and Khan, Saifullah and Rahman, Md Habibur and Afzal, Wasif and Saadatmand, Mehrdad}, month = mar, title = {Simulation-Based Safety Testing Brake-By-Wire}, booktitle = {International Conference on Software Testing, Verification and Validation Workshops, {ICST}}, year = {2017}, pages = {61-64}, publisher = {Institute of Electrical and Electronics Engineers (IEEE)}, location = {Tokyo, Japan}, isbn = {9781509066766}, url = {https://doi.org/10.1109/ICSTW.2017.17}, abstract = {Mechanical systems in cars are replaced by electronic equivalents. To be authorized for the road, validation that the replacements are at least as good as the old systems is required. For electronic braking systems (brake-by-wire), this goodness translates to safety in terms of maintaining timing constraints. Yet, in the future, the safety of braking maneuvres will depend, not only, on electronic brakes, but also on cooperative driving maneuvres orchestrated among many cars. Connecting both brake-by-wire on the microscopic level with cooperative braking on the macroscopic level allows for determining safety on a broader scale, as both systems feed from the same resource: Time. This paper discusses work-in-progress, introducing and combining two threads: electronic brakes and cooperative braking. Discussing safety on two levels simultaneously motivates connecting a Simulink model of an electronic brake-by-wire system with the traffic simulator SUMO for conducting the required combined validation. How safe is a car in relation to a given maximal braking distance? What is the optimal distribution of reaction time between electronic brakes and cooperative braking? The validation focuses on non-functional safety limited by temporal constraints (translated to braking distance). It can be exploited in an early validation approach to help reduce costs of more expensive real world experimentation. It can also determine the boundaries at which sufficient safety can be guaranteed.} }
[inproceedings] bibtex | Dokument aufrufen
S. Khan, M. Alam, und M. Fränzle, "A hybrid MAC scheme for wireless vehicular communication" in Proc. IEEE-EUROCON, 2017 -17th International Conference on Smart Technologies, Ohrid, Macedonia, July 6-8, 2017, Ohrid, Macedonia, 2017.
doi: 10.1109/EUROCON.2017.8011239
@INPROCEEDINGS{, author = {Khan, Saifullah and Alam, Muhammad and Fr{\"{a}}nzle, Martin}, month = jul, title = {A hybrid MAC scheme for wireless vehicular communication}, booktitle = {IEEE-EUROCON, 2017 -17th International Conference on Smart Technologies, Ohrid, Macedonia, July 6-8, 2017}, year = {2017}, pages = {889-895}, organization = {IEEE}, address = {Ohrid, Macedonia}, url = {https://doi.org/10.1109/EUROCON.2017.8011239}, doi = {10.1109/EUROCON.2017.8011239} }
[inproceedings] bibtex
B. Xue, M. Fränzle, und P. N. Mosaad, "Just scratching the surface: Partial exploration of initial values in reach set computation" in Proc. 2017 IEEE 56th Conference on Decision and Control (CDC), 2017.
@INPROCEEDINGS{, author = {Xue, Bai and Fr{\"{a}}nzle, Martin and Mosaad, Peter Nazier}, month = dec, title = {Just scratching the surface: Partial exploration of initial values in reach set computation}, booktitle = {2017 IEEE 56th Conference on Decision and Control (CDC)}, year = {2017}, location = {Melbourne, Australien} }
[article] bibtex
B. Xue, A. Easwaran, N. Cho, und M. Fränzle, "Reach-avoid verification for nonlinear systems based on boundary analysis" IEEE Trans. Automat. Contr..
@ARTICLE{, author = {Xue, Bai and Easwaran, Arvind and Cho, Nam-Joon and Fr{\"{a}}nzle, Martin}, title = {Reach-avoid verification for nonlinear systems based on boundary analysis}, journal = {IEEE Trans. Automat. Contr.}, year = {2017}, pages = {62(7): 3518-3523} }
[book] bibtex
L. Cardelli, M. Ceska, M. Fränzle, M. Kwiatkowska, L. Laurenti, N. Paoletti, und M. Whitby, Syntax-Guided Optimal Synthesis for Chemical Reaction Networks, Springer International Publishing.
doi: 10.1007/978-3-319-63390-9_20
@BOOK{, author = {Cardelli, Luca and Ceska, Milan and Fr{\"{a}}nzle, Martin and Kwiatkowska, Marta and Laurenti, Luca and Paoletti, Nicola and Whitby, Max}, month = jul, title = {Syntax-Guided Optimal Synthesis for Chemical Reaction Networks}, journal = {Lecture Notes in Computer Science}, booktitle = {Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany}, number = {Proceedings, Part II}, year = {2017}, pages = {375-395}, publisher = {Springer International Publishing}, isbn = {978-3-319-63390-9}, doi = {10.1007/978-3-319-63390-9_20}, abstract = {We study the problem of optimal syntax-guided synthesis of stochastic Chemical Reaction Networks (CRNs) that plays a fundamental role in design automation of molecular devices and in the construction of predictive biochemical models. We propose a sketching language for CRNs that concisely captures syntactic constraints on the network topology and allows its under-specification. Given a sketch, a correctness specification, and a cost function defined over the CRN syntax, our goal is to find a CRN that simultaneously meets the constraints, satisfies the specification and minimizes the cost function. To ensure computational feasibility of the synthesis process, we employ the Linear Noise Approximation allowing us to encode the synthesis problem as a satisfiability modulo theories problem over a set of parametric Ordinary Differential Equations (ODEs). We design and implement a novel algorithm for the optimal synthesis of CRNs that employs almost complete refutation procedure for SMT over reals and ODEs, and exploits a meta-sketching abstraction controlling the search strategy. Through relevant case studies we demonstrate that our approach significantly improves the capability of existing methods for synthesis of biochemical systems and paves the way towards their automated and provably-correct design.} }
[inproceedings] bibtex
S. Parisi und M. Fränzle, "Navigating with safety in confined waterways: an explorative case study" in Proc. SEC-HCI Workshop, MUC 2017, 2017.
@INPROCEEDINGS{, author = {Parisi, Stella and Fr{\"{a}}nzle, Martin}, title = {Navigating with safety in confined waterways: an explorative case study}, type = {inproceedings}, booktitle = {SEC-HCI Workshop, MUC 2017}, year = {2017}, publisher = {Gesellschaft f{\"{u}}r Informatik e.V.}, abstract = {his study explores how safe navigation is performed in restricted waterways in the North Sea from the point of view of maritime pilots. The purpose is to obtain and assess domain expert knowledge as part of an ongoing research project related to the analysis of critical factors that affect the bridge team build situation awareness while performing navigational tasks in such fairways. The study is based on the adaption of the knowledge elicitation technique of Applied Cognitive Task Analysis and ethnographic observations that were made during two sea voyages. The results indicate that the applied technique is promising for the intended analysis and can be used as input for the design of the next research phase. The findings have implications for studying safety critical tasks in the maritime domain.} }
[article] bibtex
P. N. Mosaad, M. Fränzle, und B. Xue, "Model Checking Delay Differential Equations Against Metric Interval Temporal Logic" Scientific Annals of Computer Science.
@ARTICLE{, author = {Mosaad, Peter Nazier and Fr{\"{a}}nzle, Martin and Xue, Bai}, title = {Model Checking Delay Differential Equations Against Metric Interval Temporal Logic}, journal = {Scientific Annals of Computer Science}, year = {2017}, pages = {77-109} }
[inproceedings] bibtex | Dokument aufrufen
B. Xue, P. N. Mosaad, M. Fränzle, M. Chen, Y. Li, und N. Zhan, "Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations" in Proc. Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, 2017.
doi: 10.1007/978-3-319-65765-3_16
@INPROCEEDINGS{DBLP:conf/formats/XueMFCLZ17, author = {Xue, Bai and Mosaad, Peter Nazier and Fr{\"{a}}nzle, Martin and Chen, Mingshuai and Li, Yangjia and Zhan, Naijun}, editor = {Abate, Alessandro and Geeraerts, Gilles}, title = {Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations}, booktitle = {Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017}, series = {Lecture Notes in Computer Science}, volume = {10419}, year = {2017}, pages = {281--299}, publisher = {Springer}, location = {Berlin}, isbn = {978-3-319-65764-6}, url = {https://doi.org/10.1007/978-3-319-65765-3{\_}16}, doi = {10.1007/978-3-319-65765-3_16} }
[inproceedings] bibtex
E. Böde, M. Büker, W. Damm, G. Ehmen, M. Fränzle, S. Gerwinn, T. Goodfellow, K. Grüttner, B. Josko, B. Koopmann, T. Peikenkamp, F. Poppen, P. Reinkemeier, M. Siegel, und I. Stierand, "Design Paradigms for Multi-Layer Time Coherency in ADAS and Automated Driving (MULTIC)" in Proc. FAT Series, 2017.
@INPROCEEDINGS{multic_final_report, author = {B{\"{o}}de, E. and B{\"{u}}ker, M. and Damm, W. and Ehmen, G. and Fr{\"{a}}nzle, Martin and Gerwinn, S. and Goodfellow, T. and Gr{\"{u}}ttner, K. and Josko, B. and Koopmann, B. and Peikenkamp, T. and Poppen, F. and Reinkemeier, P. and Siegel, M. and Stierand, I.}, month = {October}, title = {{Design Paradigms for Multi-Layer Time Coherency in ADAS and Automated Driving (MULTIC)}}, booktitle = {FAT Series}, number = {302}, year = {2017}, note = {Available online at \url{https://www.vda.de/en/services/Publications/fat-schriftenreihe-302.html} [Accessed on October 16, 2017]}, issn = {2192-7863} }
[incollection] bibtex
M. Fränzle, S. Gerwinn, und Y. Gao, Constraint-Solving Techniques for the Analysis of Stochastic Hybrid Systemsspringer.
@INCOLLECTION{ProCoS25, author = {Fr{\"{a}}nzle, Martin and Gerwinn, Sebastian and Gao, Yang}, editor = {Hinchey, Mike and Bowen, Jonathan P. and Olderog, Ernst-R{\"{u}}diger}, title = {Constraint-Solving Techniques for the Analysis of Stochastic Hybrid Systems}, booktitle = {Provably Correct Systems}, series = {NASA Monographs in Systems and Software Engineering}, year = {2017}, publisher = {springer}, note = {To appear}, optvolume={""}, optpages={""},

2016

[article] bibtex
M. Abdelaal, O. E. Theel, C. Kuka, P. Zhang, Y. Gao, V. Bashlovkina, D. Nicklas, und M. Fränzle, "Improving Energy Efficiency in QoS-Constrained Wireless Sensor Networks" IJDSN, vol. 2016.
doi: 10.1155/2016/1576038
@ARTICLE{Abdelaal:Journal16, author = {Abdelaal, Mohamed and Theel, Oliver E. and Kuka, Christian and Zhang, Peilin and Gao, Yang and Bashlovkina, Vasilisa and Nicklas, Daniela and Fr{\"{a}}nzle, Martin}, title = {Improving Energy Efficiency in {QoS}-Constrained Wireless Sensor Networks}, journal = {{IJDSN}}, volume = {2016}, year = {2016}, pages = {1576038:1--1576038:28}, doi = {10.1155/2016/1576038}, timestamp={Wed, 08 Jun 2016 17:51:00 +0200}, biburl={http://dblp.uni-trier.de/rec/bib/journals/ijdsn/AbdelaalTKZGBNF16}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[techreport] bibtex
K. Scheibler, F. Neubauer, A. Mahdi, M. Fränzle, T. Teige, T. Bienmüller, D. Fehrer, und B. Becker, "Extending iSAT3 with ICP-Contractors for Bitwise Integer Operations" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 116, 2016.
@TECHREPORT{ATR116, author = {Scheibler, Karsten and Neubauer, Felix and Mahdi, Ahmed and Fr{\"{a}}nzle, Martin and Teige, Tino and Bienm{\"{u}}ller, Tom and Fehrer, Detlef and Becker, Bernd}, editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fr{\"{a}}nzle, Martin and Olderog, Ernst-R{\"{u}}diger and Podelski, Andreas}, title = {Extending {iSAT3} with {ICP}-Contractors for Bitwise Integer Operations}, type = {Reports of SFB/TR 14 AVACS}, series = {ATR}, number = {116}, year = {2016}, institution = {SFB/TR 14 AVACS} }
[inproceedings] bibtex
H. Ody, M. Fränzle, und M. R. Hansen, "Discounted Duration Calculus" in Proc. FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, 2016.
@INPROCEEDINGS{FM16-DDC, author = {Ody, Heinrich and Fr{\"{a}}nzle, Martin and Hansen, Michael R.}, editor = {Fitzgerald, John S. and Heitmeyer, Constance L. and Gnesi, Stefania and Philippou, Anna}, title = {Discounted Duration Calculus}, booktitle = {{FM} 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9995}, year = {2016}, pages = {577--592} }
[inproceedings] bibtex
M. Chen, M. Fränzle, Y. Li, P. N. Mosaad, und N. Zhan, "Validated Simulation-Based Verification of Delayed Differential Dynamics" in Proc. FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, 2016.
@INPROCEEDINGS{FM16-DDE, author = {Chen, Mingshuai and Fr{\"{a}}nzle, Martin and Li, Yangjia and Mosaad, Peter Nazier and Zhan, Naijun}, editor = {Fitzgerald, John S. and Heitmeyer, Constance L. and Gnesi, Stefania and Philippou, Anna}, title = {Validated Simulation-Based Verification of Delayed Differential Dynamics}, booktitle = {{FM} 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9995}, year = {2016}, pages = {137--154} }
[inproceedings] bibtex
K. Scheibler, F. Neubauer, A. Mahdi, M. Fränzle, T. Teige, T. Bienmüller, D. Fehrer, und B. Becker, "Accurate ICP-based Floating-Point Reasoning" in Proc. Formal Methods in Computer-Aided Design (FMCAD 2016), 2016.
@INPROCEEDINGS{FMCAD16, author = {Scheibler, Karsten and Neubauer, Felix and Mahdi, Ahmed and Fr{\"{a}}nzle, Martin and Teige, Tino and Bienm{\"{u}}ller, Tom and Fehrer, Detlef and Becker, Bernd}, title = {Accurate {ICP}-based Floating-Point Reasoning}, booktitle = {Formal Methods in Computer-Aided Design (FMCAD 2016)}, year = {2016}, organization = {FMCAD Inc.}, opteditor={""}, optvolume={""}, optnumber={""}, optseries={""}, optpages={""}, optpublisher={""}, }
[proceedings] bibtex
Fränzle, Martin and Markey, Nicolas, Formal Modeling and Analysis of Timed SystemsFORMATS 2016 : 14th International Conference, Québec City (Canada): springer.
@PROCEEDINGS{, author = {Fr{\"{a}}nzle, Martin and Markey, Nicolas}, month = aug, title = {Formal Modeling and Analysis of Timed Systems}, series = {lncs}, volume = {9884}, year = {2016}, publisher = {springer}, address = {FORMATS 2016 : 14th International Conference, Qu{\'{e}}bec City (Canada)} }
[inproceedings] bibtex
A. Mahdi, K. Scheibler, F. Neubauer, M. Fränzle, und B. Becker, "Advancing Software Model Checking Beyond Linear Arithmetic Theories" in Proc. Hardware and Software: Verification and Testing - 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016, Proceedings, 2016.
doi: 10.1007/978-3-319-49052-6_12
@INPROCEEDINGS{HVC16, author = {Mahdi, Ahmed and Scheibler, Karsten and Neubauer, Felix and Fr{\"{a}}nzle, Martin and Becker, Bernd}, title = {Advancing Software Model Checking Beyond Linear Arithmetic Theories}, booktitle = {Hardware and Software: Verification and Testing - 12th International Haifa Verification Conference, {HVC} 2016, Haifa, Israel, November 14-17, 2016, Proceedings}, year = {2016}, pages = {186--201}, doi = {10.1007/978-3-319-49052-6_12}, crossref = {DBLP:conf/hvc/2016}, timestamp={Wed, 02 Nov 2016 13:49:10 +0100}, biburl={http://dblp.uni-trier.de/rec/bib/conf/hvc/MahdiSNFB16}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[inproceedings] bibtex
P. Mosaad, M. Fränzle, und B. Xue, "Temporal Logic Verification for Delay Differential Equations" in Proc. 13th International Colloquium on Theoretical Aspects of Computing, ICTAC 2016, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings, 2016.
@INPROCEEDINGS{ICTAC16, author = {Mosaad, Peter and Fr{\"{a}}nzle, Martin and Xue, Bai}, editor = {Sampaio, Augusto and Wang, Farn}, title = {Temporal Logic Verification for Delay Differential Equations}, booktitle = {13th International Colloquium on Theoretical Aspects of Computing, {ICTAC} 2016, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings}, series = {Lecture Notes in Computer Science}, year = {2016}, publisher = {Springer}, crossref = {DBLP:conf/ictac/2016} }
[inproceedings] bibtex
S. Khan und M. Fränzle, "Multi-channel mode for emergency system in urban connected vehicles" in Proc. 24th IEEE/ACM International Symposium on Quality of Service, IWQoS 2016, Beijing, China, June 20-21, 2016, 2016.
doi: 10.1109/iwqos.2016.7590415
@INPROCEEDINGS{iwqos16, author = {Khan, Saifullah and Fr{\"{a}}nzle, Martin}, title = {Multi-channel mode for emergency system in urban connected vehicles}, booktitle = {24th {IEEE/ACM} International Symposium on Quality of Service, IWQoS 2016, Beijing, China, June 20-21, 2016}, year = {2016}, pages = {1--2}, doi = {10.1109/iwqos.2016.7590415}, crossref = {DBLP:conf/iwqos/2016}, timestamp={Wed, 19 Oct 2016 16:43:13 +0200}, biburl={http://dblp.uni-trier.de/rec/bib/conf/iwqos/KhanF16}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[inproceedings] bibtex
S. Parisi und A. Lüdtke, "Evaluation of Distributed Situation Awareness on a Ship Bridge" in Proc. Proceedings of the European Conference on Cognitive Ergonomics, New York, NY, USA, 2016.
doi: 10.1145/2970930.2970965
@INPROCEEDINGS{Parisi:2016:EDS:2970930.2970965, author = {Parisi, Stella and L{\"{u}}dtke, Andreas}, keywords = {Distributed Situation Awareness, Fuzzy Cognitive Maps, Human Factors, Situation Awareness, User Interfaces}, title = {Evaluation of Distributed Situation Awareness on a Ship Bridge}, booktitle = {Proceedings of the European Conference on Cognitive Ergonomics}, series = {ECCE '16}, year = {2016}, pages = {34:1--34:2}, publisher = {ACM}, location = {Nottingham, United Kingdom}, address = {New York, NY, USA}, isbn = {978-1-4503-4244-5}, doi = {10.1145/2970930.2970965}, articleno={34}, numpages={2}, acmid={2970965}, }
[proceedings] bibtex
Fränzle, Martin and Kapur, Deepak and Zhan, Naijun, Dependable Software Engineering: Theories, Tools, and ApplicationsSecond International Symposium, SETTA 2016, November 9-11, 2016, Beijing, China:
doi: 10.1007/978-3-319-47677-3
@PROCEEDINGS{SETTA16, author = {Fr{\"{a}}nzle, Martin and Kapur, Deepak and Zhan, Naijun}, month = nov, title = {Dependable Software Engineering: Theories, Tools, and Applications}, series = {Lecture Notes in Computer Science}, volume = {9984}, year = {2016}, address = {Second International Symposium, {SETTA} 2016, November 9-11, 2016, Beijing, China}, isbn = {978-3-319-47676-6}, doi = {10.1007/978-3-319-47677-3}, timestamp={Thu, 20 Oct 2016 14:55:50 +0200}, biburl={http://dblp.uni-trier.de/rec/bib/conf/setta/2016}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[inproceedings] bibtex
Y. Gao und M. Fränzle, "CSiSAT: A Satisfiability Solver for SMT Formulas with Continuous Probability Distributions" in Proc. SNR 2016: 2nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, 2016.
@INPROCEEDINGS{SNR16, author = {Gao, Yang and Fr{\"{a}}nzle, Martin}, editor = {{\'{A}}brah{\'{a}}m, Erika and Bogomolov, Sergiy}, title = {{CSiSAT}: A Satisfiability Solver for {SMT} Formulas with Continuous Probability Distributions}, booktitle = {SNR 2016: 2nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis}, year = {2016}, organization = {IEEE}, optvolume={""}, optnumber={""}, optseries={""}, optpages={""}, optpublisher={""},

2015

[article] bibtex
Y. Gao und M. Fränzle, "Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain" Symbolic and Numerical Methods for Reachability Analysis, 1st International Workshop, SNR 2015, vol. 37.
@ARTICLE{, author = {Gao, Yang and Fr{\"{a}}nzle, Martin}, editor = {Bogomolov, Sergiy and Tiwari, Ashish}, title = {Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain}, journal = {Symbolic and Numerical Methods for Reachability Analysis, 1st International Workshop, SNR 2015}, volume = {37}, year = {2015}, pages = {2-10}, issn = {2040-557X}, abstract = {Stochastic Satisfiability Modulo Theories (SSMT) is a quantitative exten- sion of classical Satisfiability Modulo Theories (SMT) inspired by stochastic logics. It extends SMT by the usual as well as randomized quantifiers, fa- cilitating capture of stochastic game properties in the logic, like reachability analysis of hybrid-state Markov decision processes. Solving for SSMT for- mulae with quantification over finite and thus discrete domain has been ad- dressed by Tino Teige et al. In our work, we extend their work to SSMT over continuous quantifier domains (CSSMT) in order to enable capture of, e.g., continuous disturbances and uncertainty in hybrid systems. We extend the semantics of SSMT and introduce a corresponding solving procedure. A discussion regarding to reachability analysis is given to demonstrate applica- bility of our framework to reachability problems in hybrid systems.} }
[inproceedings] bibtex
M. Amri, Y. Becis, D. Aubry, N. Ramdani, und M. Fränzle, "Robust indoor location tracking of multiple inhabitants using only binary sensors" in Proc. IEEE International Conference on Automation Science and Engineering, CASE 2015, Gothenburg, Sweden, August 24-28, 2015, 2015.
doi: 10.1109/coase.2015.7294061
@INPROCEEDINGS{Amri-etal:CASE15, author = {Amri, Mohamed{-}Hedi and Becis, Yasmina and Aubry, Didier and Ramdani, Nacim and Fr{\"{a}}nzle, Martin}, title = {Robust indoor location tracking of multiple inhabitants using only binary sensors}, booktitle = {{IEEE} International Conference on Automation Science and Engineering, {CASE} 2015, Gothenburg, Sweden, August 24-28, 2015}, year = {2015}, pages = {194--199}, publisher = {{IEEE}}, doi = {10.1109/coase.2015.7294061}, timestamp={Tue, 13 Oct 2015 09:07:07 +0200}, biburl={http://dblp.uni-trier.de/rec/bib/conf/case/AmriBARF15}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[article] bibtex
A. Eggers, N. Ramdani, N. S. Nedialkov, und M. Fränzle, "Improving the SAT Modulo ODE Approach to Hybrid Systems Analysis by Combining Different Enclosure Methods" Softw. Syst. Model. vol. 14, iss. 1.
doi: 10.1007/s10270-012-0295-3
@ARTICLE{Eggers:2015:ISM:2733585.2733610, author = {Eggers, Andreas and Ramdani, Nacim and Nedialkov, Nedialko S. and Fr{\"{a}}nzle, Martin}, keywords = {Analysis of hybrid discrete-continuous systems, bracketing systems, Enclosure methods for ODEs, satisfiability modulo theories}, month = feb, title = {Improving the SAT Modulo ODE Approach to Hybrid Systems Analysis by Combining Different Enclosure Methods}, journal = {Softw. Syst. Model.}, volume = {14}, number = {1}, year = {2015}, pages = {121--148}, publisher = {Springer-Verlag New York, Inc.}, address = {Secaucus, NJ, USA}, issn = {1619-1366}, doi = {10.1007/s10270-012-0295-3}, issue_date={February 2015}, numpages={28}, acmid={2733610}, }
[inproceedings] bibtex
Y. Page, F. Fahrenkrog, A. Fiorentino, M. Fränzle, J. Gwehenberger, T. Helmer, M. Lindman, O. op den Camp, S. Puch, L. van Rooi, U. Sander, und P. Wimmer, "A Comprehensive and Harmonized Method for Assessing the Effectiveness of Advanced Driver Assistance Systems by Virtual Simulation: The P.E.A.R.S. Initiative" in Proc. The 24th International Technical Conference on the Enhanced Safety of Vehicles (ESV), Gothenburg, Sweden, 2015.
@INPROCEEDINGS{esv2015, author = {Page, Yves and Fahrenkrog, Felix and Fiorentino, Anita and Fr{\"{a}}nzle, Martin and Gwehenberger, Johann and Helmer, Thomas and Lindman, Magdalena and op den Camp, Olaf and Puch, Stefan and van Rooi, Lex and Sander, Ulrich and Wimmer, Peter}, month = {June}, title = {{A Comprehensive and Harmonized Method for Assessing the Effectiveness of Advanced Driver Assistance Systems by Virtual Simulation: The P.E.A.R.S. Initiative}}, booktitle = {The 24th International Technical Conference on the Enhanced Safety of Vehicles (ESV)}, year = {2015}, organization = {National Highway Traffic Safety Administration}, address = {Gothenburg, Sweden}, note = {PAPERNO.15-0370} }
[article] bibtex
M. Fakih, K. Grüttner, M. Fränzle, und A. Rettberg, "State-based real-time analysis of SDF applications on MPSoCs with shared communication resources" Journal of Systems Architecture - Embedded Systems Design, vol. 61, iss. 9.
doi: 10.1016/j.sysarc.2015.04.005
@ARTICLE{Fakih:JSA15, author = {Fakih, Maher and Gr{\"{u}}ttner, Kim and Fr{\"{a}}nzle, Martin and Rettberg, Achim}, title = {State-based real-time analysis of {SDF} applications on MPSoCs with shared communication resources}, journal = {Journal of Systems Architecture - Embedded Systems Design}, volume = {61}, number = {9}, year = {2015}, pages = {486--509}, doi = {10.1016/j.sysarc.2015.04.005}, timestamp={Thu, 26 Nov 2015 09:26:36 +0100}, biburl={http://dblp.uni-trier.de/rec/bib/journals/jsa/FakihGFR15}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[incollection] bibtex
M. Fränzle, S. Gerwinn, P. Kröger, A. Abate, und J. Katoen, Multi-objective Parameter Synthesis in Probabilistic Hybrid SystemsSpringer International Publishing.
doi: 10.1007/978-3-319-22975-1_7
@INCOLLECTION{FraenzleEtAL2015, author = {Fr{\"{a}}nzle, Martin and Gerwinn, Sebastian and Kr{\"{o}}ger, Paul and Abate, Alessandro and Katoen, Joost-Pieter}, editor = {Sankaranarayanan, Sriram and Vicario, Enrico}, title = {Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems}, booktitle = {Formal Modeling and Analysis of Timed Systems}, series = {Lecture Notes in Computer Science}, volume = {9268}, year = {2015}, pages = {93-107}, publisher = {Springer International Publishing}, isbn = {978-3-319-22974-4}, doi = {10.1007/978-3-319-22975-1_7}, language={English}, }
[article] bibtex
Y. Gao und M. Fränzle, "A Solving Procedure for Stochastic Satisfiability Modulo Theories with Continuous Domain" Quantitative Evaluation of Systems, vol. 9259.
@ARTICLE{gao2015solving, author = {Gao, Yang and Fr{\"{a}}nzle, Martin}, title = {A Solving Procedure for Stochastic Satisfiability Modulo Theories with Continuous Domain}, journal = {Quantitative Evaluation of Systems}, volume = {9259}, year = {2015}, pages = {295--311} }
[inproceedings] bibtex
L. Zou, N. Zhan, S. Wang, und M. Fränzle, "Formal Verification of Simulink/Stateflow Diagrams" in Proc. Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings, 2015.
doi: 10.1007/978-3-319-24953-7_33
@INPROCEEDINGS{Liang:ATVA15, author = {Zou, Liang and Zhan, Naijun and Wang, Shuling and Fr{\"{a}}nzle, Martin}, editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun}, title = {Formal Verification of Simulink/Stateflow Diagrams}, booktitle = {Automated Technology for Verification and Analysis - 13th International Symposium, {ATVA} 2015, Shanghai, China, October 12-15, 2015, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9364}, year = {2015}, pages = {464--481}, publisher = {Springer}, doi = {10.1007/978-3-319-24953-7_33}, timestamp={Thu, 08 Oct 2015 12:37:28 +0200}, biburl={http://dblp.uni-trier.de/rec/bib/conf/atva/ZouZWF15}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[inproceedings] bibtex
L. Zou, M. Fränzle, N. Zhan, und P. N. Mosaad, "Automatic Verification of Stability and Safety for Delay Differential Equations" in Proc. Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, 2015.
doi: 10.1007/978-3-319-21668-3_20
@INPROCEEDINGS{MF:CAV15-DDE, author = {Zou, Liang and Fr{\"{a}}nzle, Martin and Zhan, Naijun and Mosaad, Peter Nazier}, title = {Automatic Verification of Stability and Safety for Delay Differential Equations}, booktitle = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {II}}, year = {2015}, pages = {338--355}, doi = {10.1007/978-3-319-21668-3_20}, crossref = {DBLP:conf/cav/2015}, timestamp={Mon, 20 Jul 2015 11:19:16 +0200}, biburl={http://dblp.uni-trier.de/rec/bib/conf/cav/ZouFZM15}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[inproceedings] bibtex
M. Fränzle, M. R. Hansen, und H. Ody, "No Need Knowing Numerous Neighbours - Towards a Realizable Interpretation of MLSL" in Proc. Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings, 2015.
doi: 10.1007/978-3-319-23506-6_11
@INPROCEEDINGS{MFetal:ERO60, author = {Fr{\"{a}}nzle, Martin and Hansen, Michael R. and Ody, Heinrich}, editor = {Meyer, Roland and Platzer, Andr{\'{e}} and Wehrheim, Heike}, title = {No Need Knowing Numerous Neighbours - Towards a Realizable Interpretation of {MLSL}}, booktitle = {Correct System Design - Symposium in Honor of Ernst-R{\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9360}, year = {2015}, pages = {152--171}, publisher = {Springer}, doi = {10.1007/978-3-319-23506-6_11}, timestamp={Fri, 04 Sep 2015 13:09:10 +0200}, biburl={http://dblp.uni-trier.de/rec/bib/conf/birthday/FranzleHO15}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[inproceedings] bibtex
N. Müllner, M. Fränzle, und S. Fröschle, "Estimating the Probability of a Timely Traffic-Hazard Warning via Simulation" in Proc. Proceedings of the 48th Annual Symposium on Simulation (AnSS2015), Washington DC, USA, 2015.
@INPROCEEDINGS{Muellner:SpringSim2015, author = {M{\"{u}}llner, Nils and Fr{\"{a}}nzle, Martin and Fr{\"{o}}schle, Sibylle}, month = {April}, title = {Estimating the Probability of a Timely Traffic-Hazard Warning via Simulation}, booktitle = {Proceedings of the 48th Annual Symposium on Simulation (AnSS2015)}, year = {2015}, publisher = {IEEE Computer Society Press}, address = {Washington DC, USA}, abstract = {Traffic flow simulation is exploited for estimating the probability that a message ---\, a hazard warning in this case \,--- is correctly transmitted to an approaching car in time, that is, before overstepping a safety threshold. The results derived by simulation provide valuable insights in the functional relation between the numerous authoritative parameters and the reliability of timely message reception.}, access={restricted}, bibtex={muellner.anss.2015.bib}, category={Automatic Verification}, conference-long={Symposium on Simulation}, conference-short={ANSS}, cross-site={""}, pdf={muellner.anss.2015.pdf}, subproject={H1/2}, }
[article] bibtex | Dokument aufrufen
E. Olderog und M. Swaminathan, "Structural Transformations for Data-Enriched Real-Time Systems" Formal Aspects of Computing, vol. 27, iss. 4.
doi: 10.1007/s00165-014-0306-y
@ARTICLE{OlderogSwami2015, author = {Olderog, Ernst-R{\"{u}}diger and Swaminathan, Mani}, keywords = {Communication Closedness, Extended Timed Automata, Flattening, Layered Composition, Layered reachability, Non-interference and Precedence, Real-time Mutual Exclusion, Separation, Structural transformations}, month = aug, title = {Structural Transformations for Data-Enriched Real-Time Systems}, journal = {Formal Aspects of Computing}, volume = {27}, number = {4}, year = {2015}, pages = {727-750}, url = {http://dx.doi.org/10.1007/s00165-014-0306-y}, doi = {10.1007/s00165-014-0306-y}, abstract = {We investigate design-level structural transformations that aim at easier subsequent verification of real-time systems with shared data variables, modelled as networks of extended timed automata (ETA). Our contributions to this end are the following: (1) We first equip ETA with an operator for layered composition, intermediate between parallel and sequential composition. Under certain non-interference and / or precedence conditions imposed on the structure of the ETA networks, the Communication Closed Layer (CCL) laws and associated partial-order (po-) and (layered) reachability equivalences are shown to hold. (2) Next, we investigate (under certain cycle conditions on the ETA) the (reachability preserving) transformations of separation and flattening aimed at reducing the number of cycles of the ETA. (3) We then show that our separation and flattening in (2) may be applied together with the CCL laws in (1), in order to restructure ETA networks such that the verification of layered reachability properties is rendered easier. This interplay of the three structural transformations (separation, flattening, and layering) is demonstrated on an enhanced version of Fischer’s real-time mutual exclusion protocol for access to multiple critical sections.} }
[inproceedings] bibtex | Dokument aufrufen
S. Khan und M. Fränzle, "Robust mid-range communication in urban VANETs." 2015.
doi: 10.1109/ICACT.2015.7224769
@INPROCEEDINGS{SKhanEtAL2015-1, author = {Khan, S. and Fr{\"{a}}nzle, Martin}, keywords = {Robust communication, routing protocols, Trafﬁc awareness, Vehicular ad-hoc networks (VANETs)}, month = jul, title = {Robust mid-range communication in urban VANETs}, year = {2015}, pages = {115-120}, publisher = {IEEE}, location = {South Korea}, organization = {ICACT}, isbn = {978-8-9968-6504-9}, url = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?reload=true&arnumber=7224769&punumber%3D7166144%26filter%3DAND%28p_IS_Number%3A7224736%29%26pageNumber%3D2}, doi = {10.1109/ICACT.2015.7224769}, abstract = {Cooperative driving and the associated need for vehicular communication motivate vehicular ad-hoc networks (VANETs). One major challenge is to provide for robust communication - in spite of highly dynamic topologies and the presence of shielding obstacles - without installing extra relay infrastructure. Traffic-density information and density estimation schemes are a valuable asset to approach this challenge. In this light we propose a novel routing protocol. Furthermore, extensive simulations are provided to support our case.} }
[inproceedings] bibtex
S. Khan, M. Alam, N. Mullner, und M. Franzle, "Cooperation and network coding based MAC protocol for VANETs" in Proc. Vehicular Networking Conference (VNC), 2015 IEEE, 2015.
doi: 10.1109/vnc.2015.7385548
@INPROCEEDINGS{SKhanEtAL2015-2, author = {Khan, S. and Alam, M. and Mullner, N. and Franzle, M.}, keywords = {access protocols, ARQ-MAC, automatic repeat request, CNC-MAC protocol, cooperative ARQ-MAC, cooperative automatic repeat request, cooperative communication, cooperative communications, Media Access Protocol, network coding, network coding based MAC protocol, network coding techniques, relay nodes, Relays, Signal to noise ratio, Throughput, VANET, vehicular ad hoc networks, Vehicular Ad-hoc Networks}, month = {Dec}, title = {Cooperation and network coding based MAC protocol for VANETs}, booktitle = {Vehicular Networking Conference (VNC), 2015 IEEE}, year = {2015}, pages = {64-67}, doi = {10.1109/vnc.2015.7385548}

2014

[inproceedings] bibtex
N. Müllner, O. Theel, und M. Fränzle, "Composing Thermostatically Controlled Loads to Determine the Reliability against Blackouts" in Proc. Proceedings of the 10th International Symposium on Frontiers of Information Systems and Network Applications (FINA2014), 2014.
@INPROCEEDINGS{, author = {M{\"{u}}llner, Nils and Theel, Oliver and Fr{\"{a}}nzle, Martin}, month = may, title = {Composing Thermostatically Controlled Loads to Determine the Reliability against Blackouts}, booktitle = {Proceedings of the 10th International Symposium on Frontiers of Information Systems and Network Applications (FINA2014)}, year = {2014}, pages = {334--341}, location = {Victoria, BC, Canada} }
[inproceedings] bibtex
N. Müllner, O. Theel, und M. Fränzle, "Combining Decomposition and Lumping to Evaluate Semi-hierarchical Systems" in Proc. Proceedings of the 28th IEEE International Conference on Advanced Information Networking and Applications (AINA2014), 2014.
@INPROCEEDINGS{, author = {M{\"{u}}llner, Nils and Theel, Oliver and Fr{\"{a}}nzle, Martin}, month = may, title = {Combining Decomposition and Lumping to Evaluate Semi-hierarchical Systems}, booktitle = {Proceedings of the 28th IEEE International Conference on Advanced Information Networking and Applications (AINA2014)}, year = {2014}, pages = {1049--1056}, location = {Victoria, BC, Canada} }
[phdthesis] bibtex | Dokument aufrufen
N. Müllner, "Unmasking fault tolerance: Quantifying deterministic recovery dynamics in probabilistic environments" PhD Thesis , 2014.
@PHDTHESIS{, author = {M{\"{u}}llner, Nils}, month = feb, title = {Unmasking fault tolerance: Quantifying deterministic recovery dynamics in probabilistic environments}, year = {2014}, school = {Carl von Ossietzky Universit{\"{a}}t Oldenburg}, note = {175 pages of contents and appendix of 188 overall pages}, url = {http://www.uni-oldenburg.de/fileadmin/user_upload/informatik/Mue14.pdf} }
[inproceedings] bibtex
A. Mahdi und M. Fränzle, "Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems" in Proc. Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, 2014.
doi: 10.1007/978-3-319-11439-2_16
@INPROCEEDINGS{DBLP:conf/rp/MahdiF14, author = {Mahdi, Ahmed and Fr{\"{a}}nzle, Martin}, title = {Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems}, booktitle = {Reachability Problems - 8th International Workshop, {RP} 2014, Oxford, UK, September 22-24, 2014. Proceedings}, year = {2014}, pages = {203--215}, doi = {10.1007/978-3-319-11439-2_16}, crossref = {DBLP:conf/rp/2014}, timestamp={Wed, 08 Oct 2014 12:10:38 +0200}, biburl={http://dblp.uni-trier.de/rec/bib/conf/rp/MahdiF14}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[inproceedings] bibtex
A. Mahdi, B. Westphal, und M. Fränzle, "Transformations for Compositional Verification of Assumption-Commitment Properties" in Proc. Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, 2014.
doi: 10.1007/978-3-319-11439-2_17
@INPROCEEDINGS{DBLP:conf/rp/MahdiWF14, author = {Mahdi, Ahmed and Westphal, Bernd and Fr{\"{a}}nzle, Martin}, title = {Transformations for Compositional Verification of Assumption-Commitment Properties}, booktitle = {Reachability Problems - 8th International Workshop, {RP} 2014, Oxford, UK, September 22-24, 2014. Proceedings}, year = {2014}, pages = {216--229}, doi = {10.1007/978-3-319-11439-2_17}, crossref = {DBLP:conf/rp/2014}, timestamp={Wed, 08 Oct 2014 12:13:48 +0200}, biburl={http://dblp.uni-trier.de/rec/bib/conf/rp/MahdiWF14}, bibsource={dblp computer science bibliography, http://dblp.org}, }
[phdthesis] bibtex | Dokument aufrufen
A. Eggers, "Direct Handling of Ordinary Differential Equations in Constraint-Solving-Based Analysis of Hybrid Systems" PhD Thesis , Germany, 2014.
@PHDTHESIS{eggers:phd:2014, author = {Eggers, Andreas}, title = {Direct Handling of Ordinary Differential Equations in Constraint-Solving-Based Analysis of Hybrid Systems}, type = {Doctoral Dissertation}, year = {2014}, school = {Carl von Ossietzky Universit{\"{a}}t Oldenburg, Fakult{\"{a}}t II, Department of Computing Science}, address = {Germany}, note = {Referees: Martin Fr{\"{a}}nzle and Nacim Ramdani, open access: \url{http://oops.uni-oldenburg.de/id/eprint/1911}}, url = {http://oops.uni-oldenburg.de/id/eprint/1911}, abstract = {In this thesis, the behavior of hybrid discrete-continuous systems is analyzed using a Bounded Model Checking (BMC) approach, i.e. by finitely unwinding the systems' transition relations as formulae. Contrary to earlier BMC approaches for hybrid systems, we allow Ordinary Differential Equations (ODEs) directly in the formula, introducing the problem class of Satisfiability (SAT) modulo ODE. The main contribution of the thesis and its underlying publications is the direct handling of SAT modulo ODE formulae by combining the iSAT solver for boolean combinations of non-linear arithmetic constraints with the VNODE-LP library for computing validated numerical enclosures for ODE solutions. This iSAT-ODE solver comprises several algorithmic enhancements, like caching of intermediate results and previous queries, bracketing systems, and the deduction of trajectory directions, all of which are subjected to evaluation on academic case studies and compared with results from the literature.}, access={open}, subproject={h12}, bibtex={eggers.phd.2014.bib}, pdf={eggers.phd.2014.pdf}, }
[article] bibtex
C. Ellen, S. Gerwinn, und M. Fränzle, "Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains" International Journal on Software Tools for Technology Transfer.
doi: 10.1007/s10009-014-0329-y
@ARTICLE{Ellen2014statistical, author = {Ellen, Christian and Gerwinn, Sebastian and Fr{\"{a}}nzle, Martin}, keywords = {Non-determinism, SSMT, Statistical model checking, Stochastic hybrid systems}, title = {Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2014}, pages = {1-20}, publisher = {Springer Berlin Heidelberg}, issn = {1433-2779}, doi = {10.1007/s10009-014-0329-y}, abstract = {Behavioral veriﬁcation of technical systems involving both discrete and continuous components is a common and demanding task. The behavior of such systems can often be characterized using stochastic hybrid automata, leading to veriﬁcation problems which can be formalized and solved using stochastic logic calculi like Stochastic Satisﬁability Modulo Theory (SSMT). While algorithms for discharging proof obligations in SSMT form exist, their applicability is limited due to the computational complexity, which often increases exponentially with the number of quantiﬁed variables. Recently, statistical model checking has been successfully applied to stochastic hybrid systems, thereby increasing the size of the system for which veriﬁcation problems is tractable. However, being based on randomized simulation, these methods usually cannot handle non-determinism. In previous work, we have deviated from the usual approach of simulating the model and rather proposed a statistical method for SSMT solving which, being based on statistical AI planning algorithms, can also treat non-determinism over a ﬁnite domain. Here, we extend this previous work to the case of continuous domains. In particular, using ideas from noisy optimization, we adaptively build up a decision tree recording the ﬁndings and guiding further exploration, thereby favoring the currently most promising sub-domain. The non-determinism is resolved by translating the satisfaction problem into an optimization problem, thereby computing both optimistic and pessimistic bounds on the probability of satisfaction. At each stage of the evaluation process, we show how to obtain conﬁdence statements about the probability of satisfaction for the overall SSMT formula, including reliable estimates on the optimal resolution of any non-deterministic choice involved.}, language={English}, owner={cellen}, timestamp={2014.08.06}, }
[inproceedings] bibtex
M. Fakih, K. Grüttner, M. Fränzle, und A. Rettberg, "Mulitcore Performance Analysis of a Multi-Phase Electrical Motor Controller" in Proc. Proceedings of the Embedded Real Time Software and Systems Congress (ERTS$^2$), 2014.
@INPROCEEDINGS{ERTSS14, author = {Fakih, Maher and Gr{\"{u}}ttner, Kim and Fr{\"{a}}nzle, Martin and Rettberg, Achim}, month = feb, title = {Mulitcore Performance Analysis of a Multi-Phase Electrical Motor Controller}, booktitle = {Proceedings of the Embedded Real Time Software and Systems Congress (ERTS$^2$)}, year = {2014}, note = {With 10 pages}, abstract = {The timing predictability of embedded systems with hard real--time requirements is fundamental for guaranteeing their safe usage. With the emergence of multicore platforms this task becomes even more challenging, because of shared processing, communication and memory resources. In this paper, a combination of simulative method with a performance analysis based on model--checking is proposed. The simulative approach is used for functional validation of the Synchronous Data Flow Application (SDFA) implementation and its mapping on the targeted hardware platform. In our proposed methodology, we are using a binary--compatible and cycle--accurate virtual platform representation to simulate and map all relevant architectural properties to our analytical performance model. In combination, the model--checking based method allows to guarantee timing bounds of multiple Synchronous Data Flow Application (SDFA) implementations. This approach utilizes Timed Automata (TA) as a common semantic model to represent WCET of software components (SDF actors) and access protocols including timing of shared buses, shared DMAs, private local and shared memories of the multicore platform. The resulting network of TA is analyzed using the UPPAAL model--checker for providing safe timing bounds of the implementation. We demonstrate our approach using a multi--phase electric motor control algorithm (modeled as SDFA) mapped to Infineon's TriCore--based Aurix multicore hardware platform.} }
[proceedings] bibtex
HSCC '14: Proceedings of the 17th International Conference on Hybrid Systems: Computation and ControlNew York, NY, USA: ACM.
@PROCEEDINGS{Fraanzle:2014:2562059, editor = {Fr{\"{a}}nzle, Martin and Lygeros, John}, month = apr, title = {HSCC '14: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control}, year = {2014}, publisher = {ACM}, location = {Berlin, Germany}, address = {New York, NY, USA}, note = {100141}, isbn = {978-1-4503-2732-9} }
[inproceedings] bibtex
M. Abdelaal, Y. Gao, M. Fränzle, und O. Theel, "EAVS: Energy Aware Virtual Sensing for Wireless Sensor Networks" in Proc. ISSNIP 2014 - Symposium on Sensor Networks, 2014.
@INPROCEEDINGS{ISSNIP14, author = {Abdelaal, Mohamed and Gao, Yang and Fr{\"{a}}nzle, Martin and Theel, Oliver}, title = {EAVS: Energy Aware Virtual Sensing for Wireless Sensor Networks}, booktitle = {ISSNIP 2014 - Symposium on Sensor Networks}, year = {2014}, pages = {1--6}, organization = {IEEE} }
[book] bibtex
N. Müllner, Unmasking fault tolerance: Quantifying deterministic recovery dynamics in probabilistic environments, Ammerländer Heerstr. 114-118, 26111 Oldenburg: BIS-Verlag der Carl von Ossietzky Universität Oldenburg.
@BOOK{Muellner2014c, author = {M{\"{u}}llner, Nils}, month = {February}, title = {Unmasking fault tolerance: Quantifying deterministic recovery dynamics in probabilistic environments}, year = {2014}, pages = {i -- xiv, 1--166}, publisher = {BIS-Verlag der Carl von Ossietzky Universit{\"{a}}t Oldenburg}, school = {Carl von Ossietzky Universit{\"{a}}t Oldenburg}, address = {Ammerl\"ander Heerstr. 114-118, 26111 Oldenburg}, note = {The book is the revised version of a PhD thesis with the same title.}, isbn = {978-3-8142-2319-3}, abstract = {The present book focuses on distributed systems operating under probabilistic influences like faults. How well can such systems provide their service under the effects of faults? How well can they recover from faults? Along with a thorough introduction into the area of fault tolerance, this book introduces a measure called \emph{limiting window availability} to answer such questions. Furthermore, a method for computing the limiting window availability based on constructing the transition models from the system and environment models is developed. The method yet hinges on the transition model being exponential in the size of the constituting system models. This effect is commonly known as \emph{state space explosion}. Combining \emph{decomposition} and \emph{lumping} ---\, methods for reducing the state space from the domain of model checking \,--- yet allows to dampen the state space explosion, thus enhancing the spectrum of systems that are tractable for an analysis significantly.}, numpages={180}, }
[inproceedings] bibtex
M. Oertel, A. Mahdi, E. Böde, und A. Rettberg, "Contract--based Safety: Specification and Application Guidelines" in Proc. Proceedings of the 1st International Workshop on Emerging Ideas and Trends in Engineering of Cyber--Physical Systems (EITEC 2014), 2014.
@INPROCEEDINGS{oertel2014, author = {Oertel, Markus and Mahdi, Ahmed and B{\"{o}}de, Eckard and Rettberg, Achim}, title = {Contract--based Safety: Specification and Application Guidelines}, booktitle = {Proceedings of the 1st International Workshop on Emerging Ideas and Trends in Engineering of Cyber--Physical Systems (EITEC 2014)}, year = {2014}, publisher = {Springer}, note = {Research related to qualification and certification of safety properties is mainly driven by two objectives, that are currently being addressed independently: the creation of reusable and modular safety cases as well as the direct integration of safety properties in the model based development artifacts abandoning separate analysis models. In this paper, we present a contract based specification approach allowing to reason about fault containment properties of components in a modular, reusable way. We link formalized safety requirements to typical development models like EAST--ADL, Simulink and AUTOSAR to state the needed properties and relations enabling analyzability of systems without any changes in industrial format, tool--chains and processes. The identification of the necessary safety artifacts to express safety concepts has been performed based on the ISO 26262, but can be applied also to other safety standards. Furthermore, we provide step--by--step application guidelines for the specification of safety concepts that can also be applied by engineers without a background in formal methods. The specification covers all typical areas of safety concepts like definitions of faults/failures, fault containment, expression of safety mechanisms or handling of degradation modes and safe states at multiple abstraction levels. Although the main focus is on the specification, we shortly introduce the possible analysis targets and clarify the interface between the safety view and the functional design. Finally, the approach is applied to a case study.}

2013

[article] bibtex | Dokument aufrufen
N. Müllner, O. Theel, und M. Fränzle, "Combining Decomposition and Reduction for the State Space Analysis of Self-Stabilizing Systems" Journal of Computer and System Sciences (JCSS), vol. 79, iss. 7.
doi: 10.1016/j.jcss.2013.01.022
@ARTICLE{Muellner2013, author = {M{\"{u}}llner, Nils and Theel, Oliver and Fr{\"{a}}nzle, Martin}, keywords = {fault tolerance, Limiting window availability, Markov chains, Probabilistic bisimilarity, Probabilistic model checking, Self stabilization}, key = {Muellner2013}, month = nov, title = {Combining Decomposition and Reduction for the State Space Analysis of Self-Stabilizing Systems}, journal = {Journal of Computer and System Sciences (JCSS)}, volume = {79}, number = {7}, year = {2013}, pages = {1113--1125}, issn = {0022-0000}, url = {http://www.sciencedirect.com/science/article/pii/S0022000013000329}, doi = {10.1016/j.jcss.2013.01.022}, abstract = {Fault tolerance measures of distributed systems can be calculated precisely by state space analysis of the Markov chain corresponding to the product of the system components. The power of such an approach is inherently confined by the state space explosion, i.e. the exponential growth of the Markov chain in the size of the underlying system. We propose a decompositional method to alleviate this limitation. Lumping is a well-known reduction technique facilitating computation of the relevant measures on the quotient of the Markov chain under lumping equivalence. In order to avoid computation of lumping equivalences on intractably large Markov chains, we propose a system decomposition supporting local lumping on the considerably smaller Markov chains of the subsystems. Recomposing the lumped Markov chains of the subsystems constructs a lumped transition model of the whole system, thus avoiding the construction of the full product chain. An example demonstrates how the limiting window availability (i.e. a particular fault tolerance measure) can be computed for a self-stabilizing system exploiting lumping and decomposition.} }
[incollection] bibtex | Dokument aufrufen
S. Puch, B. Wortelen, M. Fränzle, und T. Peikenkamp, Evaluation of Drivers Interaction with Assistant Systems using Criticality Driven Guided SimulationSpringer Berlin Heidelberg.
doi: 10.1007/978-3-642-39173-6_13
@INCOLLECTION{PWF13, author = {Puch, Stefan and Wortelen, Bertram and Fr{\"{a}}nzle, Martin and Peikenkamp, Thomas}, editor = {Duffy, Vincent G.}, keywords = {Driver Model, Guided Co-Simulation, Hybrid Simulation, Monte Carlo, Risk Analysis}, month = jun, title = {Evaluation of Drivers Interaction with Assistant Systems using Criticality Driven Guided Simulation}, booktitle = {Digital Human Modeling and Applications in Health, Safety, Ergonomics, and Risk Management. Healthcare and Safety of the Environment and Transport}, series = {Lecture Notes in Computer Science}, volume = {8025}, number = {LNCS 8025-8026}, year = {2013}, pages = {108-117}, publisher = {Springer Berlin Heidelberg}, isbn = {978-3-642-39172-9}, url = {http://dx.doi.org/10.1007/978-3-642-39173-6_13}, doi = {10.1007/978-3-642-39173-6_13}, abstract = {Advanced Driver Assistance Systems (ADAS) operate more and more autonomously and take over essential parts of the driving task e.g. keeping safe distance or detecting hazards. Thereby they change the structure of the driver�s task and thus induce a change in driver�s behavior. Nevertheless it is still the driver who is ultimately responsible for the safe operation of the vehicle. Therefore it is necessary to ensure that the behavioral changes neither reduce the controllability of the vehicle nor the controllability of the hazardous events. We introduce the Threshold Uncertainty Tree Search (TUTS) algorithm as a simulation based approach to explore rare but critical driver behavior in interaction with an assistance system. We present first results obtained with a validated driver model in a simple driving scenario.} }
[inproceedings] bibtex
M. Fakih, K. Grüttner, M. Fränzle, und A. Rettberg, "Exploiting Segregation in Bus--Based MPSoCs to Improve Scalability of Model--Checking--Based Performance Analysis for SDFAs" in Proc. International Embedded Systems Symposium (IESS), 2013.
@INPROCEEDINGS{FakihEA:IESS13, author = {Fakih, Maher and Gr{\"{u}}ttner, Kim and Fr{\"{a}}nzle, Martin and Rettberg, Achim}, title = {Exploiting Segregation in Bus--Based {MPSoCs} to Improve Scalability of Model--Checking--Based Performance Analysis for {SDFAs}}, booktitle = {International Embedded Systems Symposium (IESS)}, year = {2013}, pages = {205--217}, abstract = {The timing predictability of embedded systems with hard real--time requirements is fundamental for guaranteeing their safe usage. With the emergence of multicore platforms this task becomes even more challenging, because of shared processing, communication and memory resources. Model--checking techniques are capable of verifying the performance properties of applications running on these platforms. Unfortunately, these techniques are not scalable when analyzing systems with large number of tasks and processing units. In this paper, a model--checking based approach that allows to guarantee timing bounds of multiple Synchronous Data Flow Applications (SDFA) running on shared-- bus multicore architectures will be extended for a TDMA hypervisor architecture. We will improve the scalability of our model--checking approach by exploiting the temporal and spatial segregation properties of the TDMA architecture and demonstrate how this method can be applied.} }
[inproceedings] bibtex
M. Fakih, K. Grüttner, M. Fränzle, und A. Rettberg, "Towards Performance Analysis of SDFGs Mapped to Shared--Bus Architectures Using Model--Checking" in Proc. Proceedings of the Conference on Design, Automation and Test in Europe (DATE) 2013, 3001 Leuven, Belgium, 2013.
@INPROCEEDINGS{FakihEA:DATE2013, author = {Fakih, Maher and Gr{\"{u}}ttner, Kim and Fr{\"{a}}nzle, Martin and Rettberg, Achim}, title = {Towards Performance Analysis of SDFGs Mapped to Shared--Bus Architectures Using Model--Checking}, booktitle = {Proceedings of the Conference on Design, Automation and Test in Europe (DATE) 2013}, series = {DATE '13}, year = {2013}, pages = {1167--1172}, publisher = {European Design and Automation Association}, address = {3001 Leuven, Belgium}, abstract = {The timing predictability of embedded systems with hard real--time requirements is fundamental for guaranteeing their safe usage. With the emergence of multicore platforms this task became very challenging. In this paper, a model-- checking based approach will be described which allows us to guarantee timing bounds of multiple Synchronous Data Flow Graphs (SDFG) running on shared--bus multicore architectures. Our approach utilizes Timed Automata (TA) as a common semantic model to represent software components (SDF actors) and hardware components of the multicore platform. These TA are explored using the UPPAAL model--checker for providing the timing guarantees. Our approach shows a significant precision improvement compared with the worst--case bounds estimated based on maximal delay for every bus access. Furthermore, scalability is examined to demonstrate analysis feasibility for small parallel systems.} }
[inproceedings] bibtex | Dokument aufrufen
S. Eilers, J. Boger, und M. Fränzle, "A Path Planning Framework for Autonomous Vehicles" in Proc. 9th International Workshop on Robot Motion and Control, 2013.
doi: 10.1109/RoMoCo.2013.6614609
@INPROCEEDINGS{Eilers2013_1, author = {Eilers, S{\"{o}}nke and Boger, J{\"{u}}rgen and Fr{\"{a}}nzle, Martin}, month = jul, title = {A Path Planning Framework for Autonomous Vehicles}, booktitle = {9th International Workshop on Robot Motion and Control}, year = {2013}, pages = {203--208}, publisher = {IEEE Explore}, url = {http://dx.doi.org/10.1109/RoMoCo.2013.6614609}, doi = {10.1109/RoMoCo.2013.6614609}, abstract = {In this paper we present a framework for path planning of autonomous vehicles in static environments which allows for rapid prototyping and evaluation. We achieve this by decoupling search based path planning into search on the one hand and expansion strategies on the other hand. Thus we are able to combine arbitrary sampling methods to discretize the search space with arbitrary heuristic search algorithms. Sampling methods and searches can be connected at design--time without the need to recompile the code. Other search algorithms and sampling methods that are programmed against our interfaces can be easily added and combined with existing search algorithms and sampling methods. Furthermore, the framework is capable of creating more complex planners, by adding further sampling/search combinations to planning pipelines. We show the strength of our approach by applying our framework to one particular path planning problem and evaluating three different planning pipelines.}, timestamp={2013.02.07}, }
[inproceedings] bibtex
M. Fränzle und A. Tsourdos, "Preface.".
@INPROCEEDINGS{IntroHAS2011, author = {Fr{\"{a}}nzle, Martin and Tsourdos, Antonios}, title = {Preface}, pages = {1--2}, crossref = {HAS2011} }
[proceedings] bibtex
Fränzle, Martin and Tsourdos, Antonios, Proceedings of the first workshop on Hybrid Autonomous SystemsElsevier.
@PROCEEDINGS{HAS2011, author = {Fr{\"{a}}nzle, Martin and Tsourdos, Antonios}, editor = {Fr{\"{a}}nzle, Martin and Tsourdos, Antonios}, title = {Proceedings of the first workshop on Hybrid Autonomous Systems}, series = {Electronic Notes in Theoretical Computer Science}, volume = {297}, year = {2013}, publisher = {Elsevier} }
[inproceedings] bibtex
M. Kamgarpour, C. Ellen, S. Esmaeil Zadeh Soudjani, S. Gerwinn, J. L. Mathieu, N. Müllner, A. Abate, D. S. Callaway, M. Fränzle, und J. Lygeros, "Modeling Options for Demand Side Participation of Thermostatically Controlled Loads" in Proc. Bulk Power System Dynamics and Control -- IX Optimization, Security and Control of the Emerging Power Grid (IREP), 2013 IREP Symposium, 2013.
doi: 10.1109/irep.2013.6629396
@INPROCEEDINGS{irep2013, author = {Kamgarpour, Maryam and Ellen, Christian and Esmaeil Zadeh Soudjani, Sadegh and Gerwinn, Sebastian and Mathieu, Johanna L. and M{\"{u}}llner, Nils and Abate, Alessandro and Callaway, Duncan S. and Fr{\"{a}}nzle, Martin and Lygeros, John}, month = {8}, title = {Modeling Options for Demand Side Participation of Thermostatically Controlled Loads}, booktitle = {Bulk Power System Dynamics and Control -- IX Optimization, Security and Control of the Emerging Power Grid (IREP), 2013 IREP Symposium}, year = {2013}, pages = {1--15}, publisher = {IEEE Xplore}, doi = {10.1109/irep.2013.6629396} }
[inproceedings] bibtex
L. Zou, N. Zhan, S. Wang, M. Fränzle, und S. Qin, "Verifying Simulink Diagrams Via A Hybrid Hoare Logic Prover" in Proc. Proccedings of the 13th International Conference on Embedded Software (EMSOFT), 2013.
doi: 10.1109/EMSOFT.2013.6658587
@INPROCEEDINGS{Liang:EMSOFT13, author = {Zou, Liang and Zhan, Naijun and Wang, Shuling and Fr{\"{a}}nzle, Martin and Qin, Shengchao}, editor = {Ernst, Rolf and Sokolsky, Oleg}, title = {Verifying {Simulink} Diagrams Via A Hybrid {Hoare} Logic Prover}, booktitle = {Proccedings of the 13th International Conference on Embedded Software (EMSOFT)}, year = {2013}, pages = {9:1--9:10}, organization = {ACM}, doi = {10.1109/EMSOFT.2013.6658587}, abstract = {Simulink is an industrial de-facto standard for building executable models of embedded systems and their environments, facilitating validation by simulation. Due to the inherent incompleteness of this form of system validation, complementing simulation by formal verification would be desirable. A prerequisite for such an approach is a formal semantics of Simulink's graphical models. In this paper, we show how to encode Simulink diagrams into Hybrid CSP (HCSP), a formal modelling language encoding hybrid system dynamics by means of an extension of CSP. The translation from Simulink to HCSP is fully automatic. We furthermore discuss how to utilize a Hybrid Hoare Logic Prover to verify the translated HCSP models. We demonstrate our approach on a combined scenario originating from the Chinese High-speed Train Control System at Level 3 (CTCS-3).} }
[inproceedings] bibtex
E. Olderog und M. Swaminathan, "Structural Transformations for Data-Enriched Real-Time Systems" in Proc. integrated Formal Methods (iFM), 2013.
doi: 10.1007/978-3-642-38613-8_26
@INPROCEEDINGS{, author = {Olderog, Ernst-R{\"{u}}diger and Swaminathan, Mani}, keywords = {Communication Closedness, Extended Timed Automata, Flattening, Layered Composition, layred reachability, Non-interference and Precedence, Real-time Mutual Exclusion, Separation}, month = jun, title = {Structural Transformations for Data-Enriched Real-Time Systems}, booktitle = {integrated Formal Methods (iFM)}, series = {Lecture Notes in Computer Science}, volume = {7940}, year = {2013}, pages = {378-393}, publisher = {Springer}, location = {Turku, Finland}, isbn = {978-3-642-38612-1,978-3-642-3861}, doi = {http://dx.doi.org/10.1007/978-3-642-38613-8_26}, abstract = {We investigate structural transformations for easier verification of real-time systems with shared data variables, modelled as networks of extended timed automata (ETA). Our contributions to this end are: (1) An operator for layered composition of ETA that yields communication closed equivalences under certain independence and / or precedence conditions. (2) Two reachability preserving transformations of separation and flattening for reducing (under certain cycle conditions) the number cycles of the ETA. (3) The interplay of the three structural transformations (separation, flattening, and layering), illustrated on an enhanced version of Fischer�s real-time mutual exclusion protocol.}

2012

[article] bibtex | Dokument aufrufen
T. Teige und M. Fränzle, "Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability" Logical Methods in Computer Science, vol. 8, iss. 2.
doi: 10.2168/LMCS-8(2:16)2012
@Article{ teigefraenzle:lmcs, author = {Tino Teige and Martin Fr{\"a}nzle}, title = {Generalized {C}raig Interpolation for Stochastic {B}oolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability}, journal = {Logical Methods in Computer Science}, volume = {8}, number = {2}, year = {2012}, pages = {1--32}, subproject = {H1/2,H4}, url = {http://www.lmcs-online.org/ojs/viewarticle.php?id=1022\&layout=abstract}, doi = {10.2168/LMCS-8(2:16)2012}, abstract = {The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them probabilistic bounded model checking (PBMC) of symbolically represented Markov decision processes. This article identifies a notion of \emph{Craig interpolant} for the SSAT framework and develops an algorithm for computing such interpolants based on a resolution calculus for SSAT. As a potential application area of this novel concept of Craig interpolation, we address the symbolic analysis of probabilistic systems. We first investigate the use of interpolation in probabilistic state reachability analysis, turning the falsification procedure employing PBMC into a verification technique for probabilistic safety properties. We furthermore propose an interpolation-based approach to probabilistic region stability, being able to verify that the probability of stabilizing within some region is sufficiently large.} }
[inproceedings] bibtex | Dokument aufrufen
A. Eggers, N. Ramdani, N. S. Nedialkov, und M. Fränzle, "Set-Membership Estimation of Hybrid Systems via SAT Modulo ODE" in Proc. Proceedings of the 16th IFAC Symposium on System Identification, 2012.
doi: 10.3182/20120711-3-BE-2027.00292
@inproceedings{EggRamNedFra:SYSID:2012, author = {Andreas Eggers and Nacim Ramdani and Nedialko S. Nedialkov and Martin Fr{\"{a}}nzle}, title = {Set-Membership Estimation of Hybrid Systems via {SAT} Modulo {ODE}}, pages = {440--445}, booktitle = {Proceedings of the 16th IFAC Symposium on System Identification}, editor = {Michel Kinnaert}, doi = {10.3182/20120711-3-BE-2027.00292}, url = {http://dx.doi.org/10.3182/20120711-3-BE-2027.00292}, publisher = {The International Federation of Automatic Control (IFAC)}, year = {2012}, abstract = { Set membership estimation (SME) of nonlinear hybrid systems is still a challenging issue. Although SME of nonlinear continuous systems has made significant progress recently, the direct extension of these methods to the hybrid case is not easy. Meanwhile, satisfiability (SAT) checkers for Boolean combinations of arithmetic constraints over real- and integer-valued variables have made significant progress, as they can effectively deal with algebraic constraints between variables and non-linear ODEs, what is denoted as SAT Modulo ODE. Finally, the corresponding solvers solve in a natural way the hybrid differential and algebraic constraints satisfaction problems that underlie SME of hybrid systems. This paper presents the application of such a SAT Modulo ODE solver to SME of hybrid dynamical systems.} }
[inproceedings] bibtex
S. Puch, M. Fränzle, J. Osterloh, und C. Läsche, "Rapid Virtual-Human-in-the-Loop Simulation with the High Level Architecture" in Proc. Proceedings of Summer Computer Simulation Conference 2012 (SCSC 2012), Genua, 2012.
@INPROCEEDINGS{scsc12, author = {Puch, Stefan and Fr{\"{a}}nzle, Martin and Osterloh, Jan-Patrick and L{\"{a}}sche, Christoph}, editor = {Bruzzone, A.}, keywords = {Driver Model, Guided Simulation, High Level Architecture (HLA)}, month = {07}, title = {Rapid Virtual-Human-in-the-Loop Simulation with the High Level Architecture}, booktitle = {Proceedings of Summer Computer Simulation Conference 2012 (SCSC 2012)}, volume = {44}, number = {10}, year = {2012}, pages = {44--50}, publisher = {Curran Associates, Inc.}, organization = {The Society for Modeling \& Simulation International (SCS)}, address = {Genua}, abstract = {Connecting different simulators, and setting up a distributed simulation is a complex and expensive task. Especially in research projects, where rapid results are desired, this is a task that is often too time consuming. Therefore the use of standards and existing frameworks can be helpful. The IEEE 1516 High Level Architecture (HLA) is a well--established concept for distributed simulation, whereas HLA is not well suited for rapid prototyping. In this paper, we describe how we use HLA in a virtual--human--in--the--loop simulation, as well as the framework we developed in order to allow to rapidly connect new simulators. Finally, we present an evaluation of our framework, which shows that an open source RTI in our context of research may compete well with a commercial RTI implementation.} }
[inproceedings] bibtex
C. Ellen, S. Gerwinn, und M. Fränzle, "Confidence Bounds for Statistical Model Checking of Probabilistic Hybrid Systems" in Proc. Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2012.
@INPROCEEDINGS{Ellen2012, author = {Ellen, Christian and Gerwinn, Sebastian and Fr{\"a}nzle, Martin}, title = {Confidence Bounds for Statistical Model Checking of Probabilistic Hybrid Systems}, booktitle = {Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)}, year = {2012}, editor = {Jurdzi{\'n}ski, Marcin and Nickovic, Dejan}, volume = {7595}, series = {LNCS}, pages = {123-138}, publisher = {Springer}, owner = {cellen}, timestamp = {2012.07.20} }
[inproceedings] bibtex
S. Eilers, S. Gerwinn, M. Fränzle, C. Kuka, S. Schweiger, und T. Toben, "An Autonomous Vehicle Design for Safe Operation in Heterogeneous Environments" in Proc. Proceedings of The CONCUR '12 Workshop on Trustworthy Cyber--Physical Systems, 2012.
@INPROCEEDINGS{Eilers2012, author = {Eilers, S{\"o}nke and Gerwinn, Sebastian and Fr{\"a}nzle, Martin and Kuka, Christian and Schweiger, S{\"o}ren and Toben, Tobe}, Title = {An Autonomous Vehicle Design for Safe Operation in Heterogeneous Environments}, Year = {2012}, Pages = {31 -- 37}, Month = {08}, Editor = {Fitzgerald, John and Mak, Terrence and Romanovsky, Alexander and Yakovlev, Alex}, Series = {Technical Report Series}, Booktitle = {Proceedings of The CONCUR '12 Workshop on Trustworthy Cyber--Physical Systems}, Institution = {Newcastle University, UK} }
[article] bibtex
M. Swaminathan, J. Katoen, und E. Olderog, "Layered Reasoning for Randomized Distributed Algorithms" Formal Aspects of Computing, vol. 24, iss. 4-6.
doi: 10.1007/s00165-012-0231-x
@ARTICLE{swakatold:2012, author = {Swaminathan, Mani and Katoen, Joost-Pieter and Olderog, Ernst-R{\"{u}}diger}, keywords = {Probabilistic automata – Layered composition and separation – Communication closedness – Partial order equivalence – Randomizedmutual exclusion}, month = jul, title = {Layered Reasoning for Randomized Distributed Algorithms}, journal = {Formal Aspects of Computing}, volume = {24}, number = {4-6}, year = {2012}, pages = {477-496}, doi = {http://dx.doi.org/10.1007/s00165-012-0231-x}, abstract = {This paper adopts the communication closed layer (CCL) concept of Elrad and Francez to the formal reasoning of randomized distributed algorithms. We do so by enriching probabilistic automata (PA) with a layered composition operator, an intermediate between parallel and sequential composition. Layered composition is used to establish probabilistic counterparts of the CCL laws that exploit independence and/or precedence conditions between the constituent PA. The probabilistic CCL laws enable partial order (po-) equivalence when layered composition is replaced by sequential composition. Such po-equivalence induces a purely syntactic partial-order state space reduction via layered separation in compositions of PA while preserving probabilistic next-free linear-time properties. The feasibility of such layered separation is demonstrated on a randomized mutual exclusion algorithm by Kushilevitz and Rabin, complementing an algebraic approach (for analyzing this algorithm) by McIver, Gonzalia, Cohen, and Morgan.} }
[inproceedings] bibtex
S. Puch, B. Wortelen, M. Fränzle, und T. Peikenkamp, "Using Guided Simulation to Improve a Model-Based Design Process of Complex Human Machine Systems" in Proc. ESM'2012 - The 2012 European Simulation And Modelling Conference, Essen, 2012.
@INPROCEEDINGS{esm2012, author = {Stefan Puch and Bertram Wortelen and Martin Fr{\"{a}}nzle and Thomas Peikenkamp}, title = {Using Guided Simulation to Improve a Model-Based Design Process of Complex Human Machine Systems}, booktitle = {ESM'2012 - The 2012 European Simulation And Modelling Conference}, year = {2012}, editor = {M. Klumpp}, pages = {159--164}, address = {Essen}, month = {10}, isbn = {978-90-77381-71-1}, publisher = {EUROSIS-ETI}, abstract = {Model-based risk assessment of human machine systems in safety critical environments is a difficult task. The complexity of the system and the inherent probabilistic nature of the human operators make an exhaustive formal analysis infeasible. In this paper a concept for an efficient exploration of critical situations is presented. Two algorithms for identification of critical situations and estimation of their probabilities are introduced. Complexity is handled by an intelligent guidance strategy and an adjustable concept of abstraction. We discuss advantages and shortcomings of our approach on a theoretical level. Finally, an evaluation plan of the presented concept is outlined. It will investigate the effects of a driver assistance system in a system incorporating a driver, a car and its environment. This study utilizes a detailed cognitive driver model for the driver component of the system.} }
[article] bibtex | Dokument aufrufen
A. Eggers, N. Ramdani, N. S. Nedialkov, und M. Fränzle, "Improving the SAT Modulo ODE Approach to Hybrid Systems Analysis by Combining Different Enclosure Methods" Software and Systems Modeling.
doi: 10.1007/s10270-012-0295-3
@article{eggramnedfra:sosym:2012, author = {Andreas Eggers and Nacim Ramdani and Nedialko S. Nedialkov and Martin Fr{\"{a}}nzle}, title = {Improving the {SAT} Modulo {ODE} Approach to Hybrid Systems Analysis by Combining Different Enclosure Methods}, journal = {Software and Systems Modeling}, doi = {10.1007/s10270-012-0295-3}, publisher = {Springer}, year = {2012 to appear. Copyright: Springer-Verlag Berlin Heidelberg, 2012. The final publication is available at www.springerlink.com.}, note = {accepted for publication, to appear. Copyright: Springer-Verlag Berlin Heidelberg, 2012. The final publication is available at www.springerlink.com.}, abstract = {Aiming at automatic verification and analysis techniques for hybrid discrete-continuous systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art interval solver for ODEs, and with bracketing systems, which exploit monotonicity properties allowing to find enclosures for problems that VNODE-LP alone cannot enclose tightly. We apply the combined iSAT-ODE solver to the analysis of a variety of non-linear hybrid systems by solving predicative encodings of reachability properties and of an inductive stability argument, and evaluate the impact of the different enclosure methods, decision heuristics, and their combination. Our experiments include classic benchmarks from the literature, as well as a newly-designed conveyor belt system that combines hybrid behavior of parallel components, a slip-stick friction model with non-linear dynamics and flow invariants, and several dimensions of parameterization. In the paper, we also present and evaluate an extension of VNODE-LP tailored to its use as a deduction mechanism within iSAT-ODE, to allow fast re-evaluations of enclosures over arbitrary subranges of the analyzed time span.}, url = {http://hs.informatik.uni-oldenburg.de/download/eggramnedfra_sosys_2012_authors_copy.pdf} }
[phdthesis] bibtex | Dokument aufrufen
T. Teige, "Stochastic Satisfiability Modulo Theories: A Symbolic Technique for the Analysis of Probabilistic Hybrid Systems" PhD Thesis , Germany, 2012.
@PhdThesis{Teige12:PhDThesis, author = {Tino Teige}, title = {Stochastic Satisfiability Modulo Theories: A Symbolic Technique for the Analysis of Probabilistic Hybrid Systems}, school = {Carl von Ossietz\-ky Universit{\"a}t Oldenburg, Department of Computing Science}, year = {2012}, type = {Doctoral Dissertation}, address = {Germany}, note = {Supervisors: Prof.~Dr.~Martin Fr{\"a}nzle and Prof.~Dr.-Ing.~Holger Hermanns}, url = {http://oops.uni-oldenburg.de/1389/} }
[inproceedings] bibtex
N. Müllner, O. Theel, und M. Fränzle, "Combining Decomposition and Reduction for State Space Analysis of a Self-Stabilizing System" in Proc. Proceedings of the 2012 IEEE 26th International Conference on Advanced Information Networking and Applications, 2012.
doi: 10.1109/AINA.2012.127
@INPROCEEDINGS{Muellner2012, author = {M{\"{u}}llner, Nils and Theel, Oliver and Fr{\"{a}}nzle, Martin}, keywords = {chain state space, Detectors, distributed processing , distributed system, exponential growth, fault tolerance, fault tolerance property verification, fault tolerant computing, Fault tolerant systems, formal verification, lumped Markov chain, lumping, lumping piecewise, Markov chains, Markov processes, probabilistic logic, reduction technique, redundant information, Registers, self-stabilization, self-stabilizing system, state space analysis, state space reduction, state-space methods, system decomposition, Transient analysis}, month = mar, title = {Combining Decomposition and Reduction for State Space Analysis of a Self-Stabilizing System}, booktitle = {Proceedings of the 2012 IEEE 26th International Conference on Advanced Information Networking and Applications}, year = {2012}, pages = {936 -- 943}, publisher = {IEEE Computer Society}, location = {Fukuoka-shi, Fukuoka, Japan}, organization = {IEEE}, note = {Best Paper Award}, issn = {1550-445X}, doi = {10.1109/AINA.2012.127}, abstract = {Verifying fault tolerance properties of a distributed system can be achieved by state space analysis via Markov chains. Yet, the power of such exact analytic methods is very limited as the state space is exponentially proportional to the system size. We propose a method that alleviates this limit. Lumping is a well known reduction technique that can be applied to a Markov chain to prune redundant information. We propose a system decomposition to employ lumping piecewise on the considerably smaller Markov chains of the subsystems which are much more likely to be tractable. Recomposing the lumped Markov chains of the subsystems results in a configuration space that is likely to be considerably smaller. An example demonstrates how the limiting window availability (i.e. a fault tolerance property) can be computed for a system while exploiting the combination of lumping and decomposition.} }
[incollection] bibtex
M. Fränzle, An Introduction to Interval MethodsOldenburger Universitätsverlag.
@INCOLLECTION{MCS12:IntervalMethods, author = {Fr{\"{a}}nzle, Martin}, editor = {Leidl, Reinhard and Hartmann, Alexander}, title = {An Introduction to Interval Methods}, booktitle = {Modern Computational Science}, year = {2012}, pages = {207--222}, publisher = {Oldenburger Universit{\"{a}}tsverlag} }
[inproceedings] bibtex
C. Ellen, E. Christoph, und M. Oertel, "Automatic Transition Between Structural System Views in a Safety Relevant Embedded Systems Development Process" in Proc. Proceedings of the Conference on Design, Automation and Test in Europe, 3001 Leuven, Belgium, 2012.
@INPROCEEDINGS{Ellen2012b, author = {Ellen, Christian and Christoph, Etzien and Oertel, Markus}, month = {03}, title = {Automatic Transition Between Structural System Views in a Safety Relevant Embedded Systems Development Process}, booktitle = {Proceedings of the Conference on Design, Automation and Test in Europe}, series = {DATE '12}, year = {2012}, pages = {820--824}, publisher = {European Design and Automation Association}, address = {3001 Leuven, Belgium}, isbn = {978--3--9810801--8--6}, abstract = {It is mandatory to design safety relevant embedded systems in multiple structural system views. A typical example is the usage of a functional and technical system representation. A transition between these system views not only comprises the allocation of components but also copes with multiple design aspects and constraints that need to be transferred to the target perspective. Optimization goals regarding arbitrary design artifacts complicate this problem. In this paper we present a novel comprehensive approach integrating common allocation techniques together with a partial design generation in a system wide process to optimize complex system view transitions. We demonstrate our approach using the CESAR design methodology. The original system models and requirements are used as input for our procedure and the results are directly applied to the same models.}

2011

[techreport] bibtex
T. Teige und M. Fränzle, "Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 67, 2011.
@techreport{TeigeFraenzle:ATR67, author = {Tino Teige and Martin Fr{\"a}nzle}, title = {Generalized {C}raig Interpolation for Stochastic {B}oolean Satisfiability Problems}, editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski}, institution = {SFB/TR 14 AVACS}, month = {March}, year = {2011}, type = {Reports of SFB/TR 14 AVACS}, series = {ATR}, number = {67}, note = {ISSN: 1860-9821, http://www.avacs.org.}, }
[inproceedings] bibtex
T. Teige, "Stochastic Satisfiability Modulo Theories: A Technique for the Analysis of Probabilistic Hybrid Systems" in Proc. Joint Workshop of the German Research Training Groups in Computer Science, 2011, p. 47.
@InProceedings{TeigeDagstuhl11:SSMT, author = {Tino Teige}, title = {Stochastic Satisfiability Modulo Theories: A Technique for the Analysis of Probabilistic Hybrid Systems}, booktitle = {Joint Workshop of the German Research Training Groups in Computer Science}, editor = {Johannes H\"olzl and Liz Ribe-Baumann and Markus Br\"uckner}, year = {2011}, pages = {47}, publisher = {Gito Verlag}, note = {ISBN: 978-3-942183-36-9} }
[inproceedings] bibtex
S. Kupferschmid, B. Becker, T. Teige, und M. Fränzle, "Proof Certificates and Non-linear Arithmetic Constraints" in Proc. Proceedings of the 14th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2011), 2011.
@InProceedings{KupferschmidEtAl:DDECS11, author = {Stefan Kupferschmid and Bernd Becker and Tino Teige and Martin Fr{\"a}nzle}, title = {Proof Certificates and Non-linear Arithmetic Constraints}, booktitle = {Proceedings of the 14th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2011)}, year = {2011}, publisher = {IEEE}, }
[inproceedings] bibtex
T. Teige und M. Fränzle, "Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems" in Proc. Proceedings of the Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2011.
@InProceedings{TeigeFraenzle:TACAS11, author = {Tino Teige and Martin Fr{\"a}nzle}, title = {Generalized {C}raig Interpolation for Stochastic {B}oolean Satisfiability Problems}, editor = {Parosh Aziz Abdulla and K. Rustan M. Leino}, booktitle = {Proceedings of the Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, year = {2011}, pages = {158--172}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6605}, }
[article] bibtex
T. Teige, A. Eggers, und M. Fränzle, "Constraint-Based Analysis of Concurrent Probabilistic Hybrid Systems: An Application to Networked Automation Systems" Nonlinear Analysis: Hybrid Systems, vol. 5, iss. 2.
doi: 10.1016/j.nahs.2010.04.009
@ARTICLE{TeiEggFra:NAHS, author = {Teige, Tino and Eggers, Andreas and Fr{\"{a}}nzle, Martin}, editor = {Giu, Allessandro and Silva, Manuel and Zaytoon, Janan}, keywords = {automatic verification, concurrent probabilistic hybrid systems, constraint satisfaction problems, probabilistic logic, problem solvers}, month = may, title = {Constraint-Based Analysis of Concurrent Probabilistic Hybrid Systems: An Application to Networked Automation Systems}, journal = {Nonlinear Analysis: Hybrid Systems}, volume = {5}, number = {2}, year = {2011}, pages = {343-366}, publisher = {Elsevier}, issn = {1751-570x}, doi = {10.1016/j.nahs.2010.04.009}, abstract = {In previous publications, the authors have introduced the notion of stochastic satisfiability modulo theories (SSMT) and the corresponding SiSAT solving algorithm, which provide a symbolic method for the reachability analysis of probabilistic hybrid systems. SSMT extends satisfiability modulo theories (SMT) with randomized (or stochastic), existential, and universal quantification, as known from stochastic propositional satisfiability. In this paper, we extend the SSMT-based procedures to the symbolic analysis of concurrent probabilistic hybrid systems. After formally introducing the computational model, we provide a mechanized translation scheme to encode probabilistic bounded reachability problems of concurrent probabilistic hybrid automata as linearly sized SSMT formulae, which in turn can be solved by the SiSAT tool. We furthermore propose an algorithmic enhancement which tailors SiSAT to probabilistic bounded reachability problems by caching and reusing solutions obtained on bounded reachability problems of smaller depth. An essential part of this article is devoted to a case study from the networked automation systems domain. We explain in detail the formal model in terms of concurrent probabilistic automata, its encoding into the SiSAT modeling language, and finally the automated quantitative analysis.}, access={restricted}, subproject={H1/2,H4} }
[inproceedings] bibtex
M. Fränzle, T. Gezgin, H. Hungar, S. Puch, und G. Sauter, "Predicting the Effect of Driver Assistance via Simulation" in Proc. Human Modelling in Assisted Transportation, 2011.
@INPROCEEDINGS{FGH10, author = {Martin Fr{\"a}nzle and Tayfun Gezgin and Hardi Hungar and Stefan Puch and Gerald Sauter}, title = {Predicting the Effect of Driver Assistance via Simulation}, booktitle = {Human Modelling in Assisted Transportation}, year = {2011}, pages = {299-306}, editor = {P.C. Cacciabue and M. Hj{\"a}lmdahl and A. L{\"u}dtke and C. Riccioli}, publisher = {Springer}, abstract = {Developing assistance systems in the automotive domain involves several exploration and evaluation activities with potential users of the system. To replace the amount of human test subject involvement, executable models reproducing human behaviour are introduced. Together with models of the car, road, surrounding traffic and of course the assistance system, a complete representation of the assistance system in its application environment can then be constructed which may be used to predict effects of introducing the assistance without having to resort to experiments with humans. In this paper we present techniques concerned with the exploration of the behaviour spectrum of the combined models. We show how functionality and safety aspects of assisted driving can be evaluated in computer simulations already during early phases of the development process.} }
[techreport] bibtex
N. T. Dinh, M. Fränzle, und A. Eggers, "AVACS H1/2 8-year Benchmark: Analyzing Traffic Models With iSAT" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 81, 2011.
@TECHREPORT{atr081, author = {Dinh, Nam Thang and Fr{\"{a}}nzle, Martin and Eggers, Andreas}, editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fr{\"{a}}nzle, Martin and Olderog, Ernst-R{\"{u}}diger and Podelski, Andreas}, keywords = {benchmark, HySAT, iSAT, traffic modelling}, month = {July}, title = {{AVACS H1/2} 8-year Benchmark: Analyzing Traffic Models With {iSAT}}, type = {Reports of SFB/TR 14 AVACS}, series = {ATR}, number = {81}, year = {2011}, institution = {SFB/TR 14 AVACS}, note = {ISSN: 1860-9821, http://www.avacs.org}, abstract = {In this technical report, we present an application of the iSAT constraint solver to instances of traffic flow networks.We give an account of the underlying model and provide details of different instances of the model and a variety of verification and falsification tasks handled by our solver.} }
[inproceedings] bibtex
A. Eggers, E. Kruglov, S. Kupferschmid, K. Scheibler, T. Teige, und C. Weidenbach, "Superposition Modulo Non-Linear Arithmetic" in Proc. 8th international Symposium on Frontiers of Combining Systems (FroCos 2011), 2011.
doi: 10.1007/978-3-642-24364-6_9
@INPROCEEDINGS{eggersetalfrocos2011, author = {Eggers, Andreas and Kruglov, Evgeny and Kupferschmid, Stefan and Scheibler, Karsten and Teige, Tino and Weidenbach, Christoph}, keywords = {iSAT, SPASS, SPASS(iSAT), SUP(T)}, title = {Superposition Modulo Non-Linear Arithmetic}, booktitle = {8th international Symposium on Frontiers of Combining Systems (FroCos 2011)}, series = {Lecture Notes in Computer Science}, year = {2011}, publisher = {Springer}, pages = {119--134}, doi = {10.1007/978-3-642-24364-6_9}, volume = {6989}, abstract = {The first-order theory over non-linear arithmetic including transcendental functions (NLA) is undecidable. Nevertheless, in this paper we show that a particular combination with superposition leads to a sound and complete calculus that is useful in practice. We follow basically the ideas of the SUP(LA) combination, but have to take care of undecidability, i.e., ``unknown'' answers by the NLA reasoning procedure. A pipeline of NLA constraint simplification techniques related to the SUP(NLA) framework significantly decreases the number of ``unknown'' answers. The resulting approach is implemented as SUP(NLA) by a system combination of Spass and iSAT. Applied to various scenarios of traffic collision avoidance protocols, we show by experiments that Spass(iSAT) can fully automatically proof and disproof safety properties of such protocols using the very same formalization.} }
[inproceedings] bibtex
A. Eggers, N. Ramdani, N. S. Nedialkov, und M. Fränzle, "Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods" in Proc. Proceedings of the Ninth International Conference on Software Engineering and Formal Methods (SEFM), 2011.
doi: 10.1007/978-3-642-24690-6_13
@INPROCEEDINGS{eggramnedfra:sefm:2011, author = {Eggers, Andreas and Ramdani, Nacim and Nedialkov, Nedialko S. and Fr{\"{a}}nzle, Martin}, keywords = {bounded model checking, bracketing systems, direction deduction, hybrid systems, integration of ordinary differential equations, iSAT(ODE), Sat Modulo Theories, two-tank system, VNODE-LP. iSAT}, title = {Improving {SAT} Modulo {ODE} for Hybrid Systems Analysis by Combining Different Enclosure Methods}, booktitle = {Proceedings of the Ninth International Conference on Software Engineering and Formal Methods (SEFM)}, series = {Lecture Notes in Computer Science}, year = {2011}, pages = {172--187}, doi = {10.1007/978-3-642-24690-6_13}, volume = {7041}, publisher = {Springer}, abstract = {Aiming at automatic verification and analysis techniques for hybrid systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art enclosure method for ODEs, and with bracketing systems which---by exploiting monotonicity properties of the system---allow finding enclosures for problems that VNODE-LP alone cannot enclose tightly. We apply our method to the analysis of a non-linear hybrid system by solving predicative encodings of an inductive stability argument and evaluate the impact of different methods and their interplay in combination.} }
[inproceedings] bibtex
W. Damm, M. Fränzle, und J. Quesel, "Crossing the Bridge between Similar Games" in Proc. Formal Modeling and Analysis of Timed Systems - 9th International Conference (FORMATS), Aalborg, Denmark, 21-23 September, 2011. Proceedings, 2011.
doi: 10.1007/978-3-642-24310-3_12
@INPROCEEDINGS{avacs-h3-brg-11, author = {Damm, W. and Fr{\"{a}}nzle, Martin and Quesel, Jan-David}, editor = {Tripakis, Stavros and Fahrenberg, Uli}, keywords = {formal verification of hybrid systems, hybrid games, logics for hybrid systems, robust simulation}, month = sep, title = {Crossing the Bridge between Similar Games}, booktitle = {Formal Modeling and Analysis of Timed Systems - 9th International Conference (FORMATS), Aalborg, Denmark, 21-23 September, 2011. Proceedings}, series = {Lecture Notes in Computer Science (LNCS)}, volume = {6919}, year = {2011}, pages = {160--176}, publisher = {Springer-Verlag}, issn = {978-3-642-24309-7}, doi = {10.1007/978-3-642-24310-3_12}, abstract = {Specifications and implementations of complex physical systems tend to differ as low level effects such as sampling are often ignored when high level models are created. Thus, the low level models are often not exact refinements of the high level specification. However, they are similar to those. To bridge the gap between those models, we study robust simulation relations for hybrid systems. In this paper, we identify a family of robust simulation relations that allow for certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of simulation a broad class of logical properties is preserved. The question whether two systems are in simulation relation can be reduced to a reach avoid problem for hybrid games. We provide a sufficient condition under which a winning strategy for these games exists.} }
[incollection] bibtex
M. Fränzle und C. Lengauer, Semantic IndependenceSpringer-Verlag.
@incollection{FraLen11svSemInd, author = {Martin Fr{\"a}nzle and Christian Lengauer}, title = {Semantic Independence}, booktitle = {Encyclopedia of Parallel Computing}, publisher = {Springer-Verlag}, year = {2011}, editor = {David Padua and others}, month = {sep}, pages = {1803--1810} }
[book] bibtex
C. Herde, Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure -- Proof Engines for the Analysis of Hybrid Discrete-Continuous Systems, 1st ed., Vieweg+Teubner Research.
@BOOK{herde:2011:phd, author = {Herde, Christian}, title = {Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure -- Proof Engines for the Analysis of Hybrid Discrete-Continuous Systems}, edition = {1st}, year = {2011}, publisher = {Vieweg+Teubner Research}, school = {Carl von Ossietzky Universit{\"{a}}t Oldenburg}, isbn = {978-3-8348-1494-4} }
[inproceedings] bibtex | Dokument aufrufen
M. Fränzle, E. M. Hahn, H. Hermanns, N. Wolovick, und L. Zhang, "Measurability and safety verification for stochastic hybrid systems" in Proc. Proceedings of the 14th international conference on Hybrid systems: computation and control, New York, NY, USA, 2011.
doi: 10.1145/1967701.1967710
@inproceedings{Franzle:2011:MSV:1967701.1967710, author = {Fr\"{a}nzle, Martin and Hahn, Ernst Moritz and Hermanns, Holger and Wolovick, Nicol\'{a}s and Zhang, Lijun}, title = {Measurability and safety verification for stochastic hybrid systems}, booktitle = {Proceedings of the 14th international conference on Hybrid systems: computation and control}, series = {HSCC '11}, year = {2011}, isbn = {978-1-4503-0629-4}, location = {Chicago, IL, USA}, pages = {43--52}, numpages = {10}, url = {http://doi.acm.org/10.1145/1967701.1967710}, doi = {http://doi.acm.org/10.1145/1967701.1967710}, acmid = {1967710}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {measurability, nondeterministic markov process, probabilistic hybrid automaton, reachability, stochastic hybrid automaton}, }
[article] bibtex
E. Ábrahám, T. Schubert, B. Becker, M. Fränzle, und C. Herde, "Parallel SAT Solving in Bounded Model Checking" Journal of Logic and Computation, vol. 21, iss. 1.
doi: 10.1093/logcom/exp002
@ARTICLE{AbrahamEA11, author = {{\'{A}}brah{\'{a}}m, Erika and Schubert, Tobias and Becker, Bernd and Fr{\"{a}}nzle, Martin and Herde, Christian}, keywords = {bounded model checking, hybrid systems, linear programming, parallel programs, SAT solving}, title = {Parallel {SAT} Solving in Bounded Model Checking}, journal = {Journal of Logic and Computation}, volume = {21}, number = {1}, year = {2011}, pages = {5--21}, publisher = {Oxford University Press}, doi = {10.1093/logcom/exp002}, abstract = {Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.}, subproject={H1/2}, access={restricted},

2010

[inproceedings] bibtex | Dokument aufrufen
T. Teige und M. Fränzle, "Resolution for Stochastic Boolean Satisfiability" in Proc. Logic for Programming, Artificial Intelligence, and Reasoning, 17th International Conference (LPAR-17), 2010.
doi: 10.1007/978-3-642-16242-8_44
@InProceedings{TeiFrae:LPAR17, author = {Tino Teige and Martin Fr{\"a}nzle}, title = {Resolution for Stochastic {B}oolean Satisfiability}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 17th International Conference (LPAR-17)}, editor = {Christian Ferm{\"u}ller and Andrei Voronkov}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6397}, pages = {625--639}, year = {2010}, doi = {10.1007/978-3-642-16242-8_44}, url = {http://dx.doi.org/10.1007/978-3-642-16242-8_44} }
[inproceedings] bibtex | Dokument aufrufen
M. Fränzle, T. Teige, und A. Eggers, "Satisfaction Meets Expectations: Computing Expected Values of Probabilistic Hybrid Systems with SMT" in Proc. Integrated Formal Methods 2010, 2010.
doi: 10.1007/978-3-642-16265-7
@InProceedings{FraTeiEgg:iFM10, author = {Martin Fr{\"a}nzle and Tino Teige and Andreas Eggers}, title = {Satisfaction Meets Expectations: Computing Expected Values of Probabilistic Hybrid Systems with SMT}, booktitle = {Integrated Formal Methods 2010}, editor = {Dominique M{\'e}ry and Stephan Merz}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6396}, pages = {168--182}, year = {2010}, subproject = {H1/2,H4}, doi = {10.1007/978-3-642-16265-7}, url = {http://dx.doi.org/10.1007/978-3-642-16265-7}, abstract = {Stochastic satisfiability modulo theories (SSMT), which is an extension of satisfiability modulo theories with randomized quantification, has successfully been used as a symbolic technique for computing reachability probabilities in probabilistic hybrid systems. Motivated by the fact that several industrial applications call for quantitative measures that go beyond mere reachability probabilities, this paper extends SSMT to compute expected values of probabilistic hybrid systems like, e.g., mean-times to failure. Practical applicability of the proposed approach is demonstrated by a case study from networked automation systems.}, }
[article] bibtex | Dokument aufrufen
M. Fränzle, T. Teige, und A. Eggers, "Engineering Constraint Solvers for Automatic Analysis of Probabilistic Hybrid Automata" Journal of Logic and Algebraic Programming, vol. 79.
doi: 10.1016/j.jlap.2010.07.003
@Article{FraTeiEgg:JLAP, author = {Martin Fr{\"a}nzle and Tino Teige and Andreas Eggers}, title = {Engineering Constraint Solvers for Automatic Analysis of Probabilistic Hybrid Automata}, journal = {Journal of Logic and Algebraic Programming}, editor = {Tarmo Uustalu and J{\"u}ri Vain}, volume = {79}, pages = {436--466}, publisher = {Elsevier}, year = {2010}, keywords = {Probabilistic hybrid automata, bounded model checking, arithmetic constraint solving, stochastic satisfiability}, subproject = {H1/2,H4}, doi = {10.1016/j.jlap.2010.07.003}, url = {http://dx.doi.org/10.1016/j.jlap.2010.07.003}, abstract = {In this article, we recall different approaches to the constraint-based, symbolic analysis of hybrid discrete-continuous systems and combine them to a technology able to address hybrid systems exhibiting both non-deterministic and probabilistic behavior akin to infinite-state Markov decision processes. To enable mechanized analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theories (SMT) solving by, first, reasoning over ordinary differential equations (ODEs) and, second, a comprehensive treatment of randomized (also known as stochastic) quantification over discrete variables as well as existential quantification over both discrete and continuous variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a constraint-based analysis of dense-time probabilistic hybrid automata, extending previous results addressing discrete-time automata (1). Generalizing SMT-based bounded model-checking of hybrid automata (2; 3), stochastic SMT including ODEs permits the direct analysis of probabilistic bounded reachability problems of dense-time probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.} }
[techreport] bibtex | Dokument aufrufen
S. Puch, G. Sauter, und M. Fränzle, "HLA-basierte Kosimulation domänentypischer Simulatoren" Carl von Ossietzky Universität Oldenburg2010.
@TECHREPORT{PuchEA:TechReport, author = {Stefan Puch and Gerald Sauter and Martin Fr{\"a}nzle}, title = {{HLA-basierte Kosimulation dom{\"a}nentypischer Simulatoren}}, institution = {Carl von Ossietzky Universit{\"a}t Oldenburg}, url = {http://imost.informatik.uni-oldenburg.de/download/TecReport_IMoST_002.pdf}, year = {2010}, }
[inproceedings] bibtex
J. Gacnik, H. Jost, F. Köster, und M. Fränzle, "The DeSCAS Methodology and Lessons Learned on Applying Formal Reasoning to Safety Domain Knowledge" in Proc. Proceedings of the 8th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010), 2010.
@INPROCEEDINGS{GaJoKoFr:FORMS10, author = {Jan Gacnik and Henning Jost and Frank K{\"o}ster and Martin Fr{\"a}nzle}, title = {{The DeSCAS Methodology and Lessons Learned on Applying Formal Reasoning to Safety Domain Knowledge}}, booktitle = {{Proceedings of the 8th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010)}}, year = {2010}, editor = {Eckehard Schnieder and G\'{e}za Tarnai}, abstract = {Functional safety has become an important aspect for engineering activities in the automotive domain due to the upcoming introduction of the safety standard ISO 26262. This paper proposes a methodology to guide the safety related requirements engineering process by means of OWL (Web Ontology Language) ontologies. These ontologies formalize necessary domain knowledge and serve as reference models to support semi-automated requirements discovery and to ease the certification process. Using OWL's logical base, knowledge inference is applied to reason about safety measures for ensuring compliance with the reference process (guidance). The proposed methodology has been implemented in a prototype toolchain and applied to a simple lane departure warning system as an example assistance and automation system. Lessons learned refer to conceptual (expressiveness) and technical (tooling efficiency) issues.} }
[inproceedings] bibtex | Dokument aufrufen
M. Fränzle, T. Gezgin, H. Hungar, S. Puch, und G. Sauter, "Using Guided Simulation to Assess Driver Assistance Systems" in Proc. Proc. FORMS/FORMAT 2010, 2010.
@INPROCEEDINGS{FGH10b, author = {Martin Fr{\"a}nzle and Tayfun Gezgin and Hardi Hungar and Stefan Puch and Gerald Sauter}, title = {Using Guided Simulation to Assess Driver Assistance Systems}, booktitle = {Proc. FORMS/FORMAT 2010}, year = {2010}, editor = {E. Schnieder and G. Tarnai}, abstract = {The goal of our approach is the model-based prediction of the effects of driver assistance systems. Starting with the integration of a computer model of the driver of a car into a simulation environment, we face the problem of analysing the emergent effects of a complex system with discrete, numeric and probabilistic components. In particular, it is difficult to assess the probability of rare events, though we are specifically interested in critical situations which will be infrequent for any reasonable system. For that purpose, we use a quantitative logic which enables us to specify criticality and other properties of simulation runs. An online evaluation of the logic permits us to define a procedure which guides the simulation towards critical situations and allows to estimate the risk of connected with the introduction of the assistance system.}, url = {http://hs.informatik.uni-oldenburg.de/download/HungarEtAl-FORMS2010-pub.pdf} }
[inproceedings] bibtex | Dokument aufrufen
A. Eggers, "SAT Modulo ODE: A Direct SAT approach to Hybrid Systems" in Proc. 10271 Abstracts Collection -- Verification over discrete-continuous boundaries, Dagstuhl, Germany, 2010.
@inproceedings{eggers:satmoduloode:dagstuhl:10271:2010, author = {Andreas Eggers}, title = {{SAT} Modulo {ODE}: A Direct {SAT} approach to Hybrid Systems}, booktitle = {10271 Abstracts Collection -- Verification over discrete-continuous boundaries}, editor = {Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar}, series = {Dagstuhl Seminar Proceeding}, number = {10271}, year = {2010}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany}, address = {Dagstuhl, Germany}, pages = {7--8}, ISSN = {1862-4405}, subproject= {H1/2}, bibtex = {eggers.dagstuhl10.bib}, url = {http://drops.dagstuhl.de/opus/volltexte/2010/2792}, abstract = {In this talk, we present our approach to perform bounded model checking (BMC) of hybrid discrete continuous systems using constraint solving techniques. The BMC problem can be expressed by a Boolean combination of arithmetic constraints and ordinary differential equations (ODEs). While the Boolean, integer, and real-valued variables represent the state of the hybrid system, the constraint system describes traces characterized by their initial states, a transition relation connecting subsequent states by continuous flows or discrete jumps, and a target state whose reachability is to be analyzed. The reachability problem of the hybrid system therefore becomes a satisfiability problem of this type of formula. We extend our constraint solving algorithm iSAT to also handle the ODEs occuring in these formulae by using safe enclosures of the ODEs solution trajectories thereby coupling the structure of the DPLL procedure, which is used successfully in propositional satisfiability solving, with interval methods for arithmetic constraints and safe enclosure methods for the solutions of initial value problems. Our current work is focused (1) on exchanging our prototypical enclosure mechanism with Ned Nedialkov's VNODE-LP in order to obtain such enclosures more efficiently and (2) on storing once-deduced knowledge and potentially further information available on the solution trajectories persistently in the constraint system to avoid costly enclosures in the first place. Keywords: Hybrid discrete continuous systems, automatic verification, satisfiability modulo theories, ordinary differential equations Joint work of: Eggers, Andreas; Fraenzle, Martin; Herde, Christian} }
[phdthesis] bibtex
C. Herde, "Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure: Proof Engines for the Analysis of Hybrid Discrete--Continuous Systems" PhD Thesis , 2010.
@PhdThesis{Herde:Thesis, author = "Christian Herde", title = "Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure: Proof Engines for the Analysis of Hybrid Discrete--Continuous Systems", school = "Carl von Ossietzky Universi{\"a}t Oldenburg", year = "2010", type = "Doctoral Dissertation", subproject = {H1/2}, access = {restricted}, bibtex = {herde.phd.2010.bib}, abstract = "Due to the increasing use of more and more complex computerized systems in safety-critical applications, formal verification of such systems is of growing importance. Among the most successful methods in formal verification of finite-state systems is bounded model checking (BMC), a technique for checking whether an unsafe system state is reachable within a fixed number of steps. BMC belongs to a class of verification algorithms having in common that the verification task is reduced to the problem of checking the satisfiability of a propositional formula or a series thereof. Though originally formulated for discrete transition systems only, BMC is in principle also applicable to hybrid discrete-continuous systems, which naturally arise e.g. in the field of embedded systems where digital (discrete) controllers are coupled with analog (continuous) physical plants. The BMC formulae arising from such systems are, however, no longer purely propositional, but usually comprise complex Boolean combinations of arithmetic constraints over real-valued variables, thus entailing the need for new decision procedures to solve them. This thesis deals with the development of such procedures. A key component of the algorithms we present is the DPLL procedure for solving Boolean formulae which are in conjunctive normal form (CNF). As a first contribution, we demonstrate that the acceleration techniques, which enabled the enormous performance gains of Boolean SAT solvers in the recent past, generalize smoothly to DPLL-based procedures for solving systems of pseudo-Boolean constraints, a much more concise representation of Boolean functions than CNFs. Second, we investigate how to efficiently couple a linear programming routine with a DPLL-based SAT solver in order to obtain a solver which is tailored for BMC of hybrid systems with linear dynamics. In particular, we examine how to exploit the unique characteristics of BMC formulae and the incremental nature of BMC for various optimizations inside the solver. Finally, we present our main contribution, a tight integration of the DPLL procedure with interval constraint solving, resulting in an algorithm, called iSAT, which generalizes the DPLL procedure and is capable of solving arbitrary Boolean combinations of nonlinear arithmetic constraints over the reals, even such involving transcendental functions. We demonstrate the applicability of our methods using benchmarks from the envisaged application domain.", }
[inproceedings] bibtex
E. Olderog und M. Swaminathan, "Layered Composition for Timed Automata" in Proc. 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2010), 2010.
doi: 10.1007/978-3-642-15297-9_18
@INPROCEEDINGS{, author = {Olderog, Ernst-R{\"{u}}diger and Swaminathan, Mani}, month = sep, title = {Layered Composition for Timed Automata}, booktitle = {8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2010)}, series = {Lecture Notes in Computer Science}, volume = {6246}, year = {2010}, pages = {228-242}, publisher = {Springer}, location = {Klosterneuburg, Austria}, isbn = {978-3-642-15296-2}, doi = {http://dx.doi.org/10.1007/978-3-642-15297-9_18}, abstract = {We investigate layered composition for real-time systems modelled as (networks of) timed automata (TA). We first formulate the principles of layering and transition independence for TA, and demonstrate the validity of the communication closed layer (CCL) laws in such a setting, by means of an operator for layered composition that is intermediate between parallel and sequential composition. Next, we introduce the principles of input/output (i/o) and partial-order (po) equivalences, and show that such equivalences are preserved when the layered composition operator is replaced by sequential composition within the expressions appearing in the CCL laws. Finally, we proceed to show that such layering (together with equivalences obtained through the CCL laws) can be useful in the design and verification of dense real-time systems that consist of a network of interacting components, by bringing about a reduction of the state-space through the exploitation of transition independence. This is illustrated by considering a collision avoidance protocol developed for an audio/video system of Bang and Olufsen.}

2009

[inproceedings] bibtex
T. Teige, "Stochastic Satisfiability Modulo Theories: A Technique for the Analysis of Probabilistic Hybrid Systems" in Proc. Dagstuhl 2009 - Proceedings des gemeinsamen Workshops der Informatik-Graduiertenkollegs und Forschungskollegs, 2009.
@InProceedings{TeigeDagstuhl09:SSMT, author = {Tino Teige}, title = {{Stochastic Satisfiability Modulo Theories: A Technique for the Analysis of Probabilistic Hybrid Systems}}, booktitle = {Dagstuhl 2009 - Proceedings des gemeinsamen Workshops der Informatik-Graduiertenkollegs und Forschungskollegs}, editor = {Artin Avanes and Dirk Fahland and Joanna Geibig and Siamak Haschemi and Sebastian Heglmeier and Daniel A. Sadile and Falko Theisselmann and Guido Wachsmuth and Stephan Wei{\ss}leder}, year = {2009}, pages = {52--53}, publisher = {Gito Verlag}, note = {ISBN: 978-3940019738} }
[inproceedings] bibtex
T. Teige und M. Fränzle, "Constraint-Based Analysis of Probabilistic Hybrid Systems" in Proc. Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2009), 2009.
@InProceedings{TeigeFraenzle09:ADHS, author = {Tino Teige and Martin Fr{\"a}nzle}, title = {{Constraint-Based Analysis of Probabilistic Hybrid Systems}}, booktitle = {Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2009)}, publisher = {IFAC}, editor = {A. Giua and C. Mahulea and M. Silva and J. Zaytoon}, pages = {162--167}, year = {2009} }
[inproceedings] bibtex
S. Kupferschmid, T. Teige, B. Becker, und M. Fränzle, "Proofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae" in Proc. Proceedings of the 12th Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'' (MBMV 2009), 2009.
@InProceedings{KupferschmidEtAl09:MBMV, author = {Stefan Kupferschmid and Tino Teige and Bernd Becker and Martin Fr{\"a}nzle}, title = {{Proofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae}}, booktitle = {Proceedings of the 12th Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'' (MBMV 2009)}, editor = {Carsten Gremzow and Nico Moser}, pages = {27--36}, year = {2009}, publisher = {Universit{\"a}tsverlag TU Berlin}, isbn = {978-3-7983-2118-2} }
[inproceedings] bibtex | Dokument aufrufen
A. Eggers, N. Kalinnik, S. Kupferschmid, und T. Teige, "Challenges in Constraint-Based Analysis of Hybrid Systems" in Proc. Recent Advances in Constraints -- 13th Annual ERCIM International Workshop on Constraint Solving and Constraint Logic Programming, CSCLP 2008, Rome, Italy, June 18-20, 2008, Revised Selected Papers, Berlin, Heidelberg, 2009.
doi: 10.1007/978-3-642-03251-6_4
@InProceedings{EggKalKupTei:RAC08:Challenges, author = "Andreas Eggers and Natalia Kalinnik and Stefan Kupferschmid and Tino Teige", title = "Challenges in Constraint-Based Analysis of Hybrid Systems", booktitle = "Recent Advances in Constraints -- 13th Annual ERCIM International Workshop on Constraint Solving and Constraint Logic Programming, CSCLP 2008, Rome, Italy, June 18-20, 2008, Revised Selected Papers", editor = "Angelo Oddi and Fran\c{c}ois Fages and Francesca Rossi", publisher = "Springer", address = "Berlin, Heidelberg", series = "Lecture Notes in Artificial Intelligence", volume = "5655", pages = "51--65", year = "2009", doi = "10.1007/978-3-642-03251-6_4", url = "http://dx.doi.org/10.1007/978-3-642-03251-6_4", note = "Springerlink: \url{http://www.springerlink.com/content/hx755817464v6746}", subproject= {H1/2}, abstract = "In the analysis of hybrid discrete-continuous systems, rich arithmetic constraint formulae with complex Boolean structure arise naturally. The iSAT algorithm, a solver for such formulae, is aimed at bounded model checking of hybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhance the iSAT algorithm. First, we propose an extension of iSAT to directly handle ordinary differential equations as constraints. Second, we outline the recently introduced generalization of the iSAT algorithm to deal with probabilistic hybrid systems and some open research issues in that context. Third, we present ideas on how to move from bounded to unbounded model checking by using the concept of interpolation. Finally, we discuss the adaption of some parallelization techniques to the iSAT case, which will hopefully lead to performance gains in the future. By presenting these open research questions, this paper aims at fostering discussions on these extensions of constraint solving.", keywords = "mixed Boolean and arithmetic constraints - differential equations - stochastic SMT - Craig interpolation - parallel solver " }
[inproceedings] bibtex | Dokument aufrufen
A. Eggers, M. Fränzle, und C. Herde, "Application of Constraint Solving and ODE-Enclosure Methods to the Analysis of Hybrid Systems" in Proc. NUMERICAL ANALYSIS AND APPLIED MATHEMATICS: International Conference on Numerical Analysis and Applied Mathematics 2009, Melville, New York, 2009.
doi: 10.1063/1.3241327
@InProceedings{EggFraHer:ICNAAM09:ApplicationConstraintSolvingODEHybridSystems, author = "Andreas Eggers and Martin Fr{\"a}nzle and Christian Herde", title = "Application of Constraint Solving and ODE-Enclosure Methods to the Analysis of Hybrid Systems", booktitle = "NUMERICAL ANALYSIS AND APPLIED MATHEMATICS: International Conference on Numerical Analysis and Applied Mathematics 2009", editor = "Theodore E. Simos and George Psihoyios and Ch. Tsitouras", publisher = "American Institute of Physics", address = "Melville, New York", series = "AIP Conference Proceedings", volume = "1168", pages = "1326--1330", year = "2009", url = "http://link.aip.org/link/?APC/1168/1326/1", doi = "10.1063/1.3241327", subproject= "H1/2", abstract = "In this short paper, we summarize our approach to analyzing hybrid discrete-continuous systems by reduction to constraint solving paired with enclosure methods for sets of initial value problems of ordinary differential equations.", keywords = "hybrid discrete-continuous systems, verification, ordinary differential equations, constraint solving, PACS: 02.60.Lj, 02.70.-c, 89.75.-k" }
[inproceedings] bibtex | Dokument aufrufen
G. Sauter, H. Dierks, M. Fränzle, und M. R. Hansen, "Light-weight hybrid model checking facilitating online prediction of temporal properties" in Proc. Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09, Kgs. Lyngby, Denmark, 2009.
@INPROCEEDINGS{SauterEA:NWPT09, author = {Gerald Sauter and Henning Dierks and Martin Fr{\"a}nzle and Michael R. Hansen}, title = {Light-weight hybrid model checking facilitating online prediction of temporal properties}, booktitle = {Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09}, year = {2009}, pages = {20-22}, address = {Kgs. Lyngby, Denmark}, note = {\url{http://imost.informatik.uni-oldenburg.de}}, url = {http://imost.informatik.uni-oldenburg.de/download/RobustMonitoring-NWPT09.pdf}, publisher = {Danmarks Tekniske Universitet} }
[techreport] bibtex | Dokument aufrufen
G. Sauter, H. Dierks, M. Fränzle, und M. R. Hansen, "Light-weight hybrid model checking facilitating online prediction of temporal properties" Carl von Ossietzky Universität Oldenburg2009.
@TECHREPORT{SauterEA:TechReport, author = {Gerald Sauter and Henning Dierks and Martin Fr{\"a}nzle and Michael R. Hansen}, title = {Light-weight hybrid model checking facilitating online prediction of temporal properties}, institution = {Carl von Ossietzky Universit{\"a}t Oldenburg}, year = {2009}, note = {\url{http://imost.informatik.uni-oldenburg.de}}, url = {http://imost.informatik.uni-oldenburg.de/download/TecReport_IMoST_001.pdf}, abstract = {We address the problem of online prediction of future temporal properties of open continuous systems based on time series obtained from online measurements. The objective is, given a partial time series stating (possibly inexact) measurements of observable variables of the system, to safely predict the truth value of a linear-time temporal-logic formula including future modalities, and to do so in real-time while the system is evolving. While this can in principle be done using techniques from hybrid-system model checking, these algorithms are computationally by far too expensive to support online prediction in real-time. As a computationally tractable alternative, we suggest an approach decomposing hybrid model-checking into an offline and an online phase, where the offline phase precomputes all computationally expensive entities, in particular those involving forms of branching, while the online part exploits these precomputed properties in a branching-free analysis based on computationally inexpensive interval constraint propagation. The procedure is designed for system-in-the-loop testing or similar use cases requiring real-time monitoring of dynamic processes with respect to temporal properties at moderately high sampling frequencies.} }
[inproceedings] bibtex | Dokument aufrufen
M. Fränzle und M. Swaminathan, "Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata" in Proc. The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2009), 2009.
@InProceedings{SwaminathanFraenzleFORMATS09, author = {Martin Fr{\"a}nzle and Mani Swaminathan}, title = {Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata}, booktitle = {The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2009)}, editor = {J. Ouaknine and F. Vaandrager}, pages = {149--163}, year = {2009}, month = {September}, publisher = {Springer Verlag}, url = {http://dx.doi.org/10.1007/978-3-642-04368-0_13} }
[inproceedings] bibtex
M. Fränzle, "Engineering constraint solvers for the analysis of hybrid systems" in Proc. 20th Nordic Workshop on Programming Theory, NWPT '08, 2008, p. 9.
@INPROCEEDINGS{Fraenzle:NWPT08, author = "Martin Fr{\"a}nzle", title = "Engineering constraint solvers for the analysis of hybrid systems", booktitle = "20th Nordic Workshop on Programming Theory, NWPT '08", editors = "Tarmo Uustalu and J{\"u}ri Vain and Juhan Ernits", pages = "9", publisher = "Institute of Cybernetics, Tallinn Technical University", year = "2008"}
[inproceedings] bibtex
M. Fränzle, A. Eggers, C. Herde, und T. Teige, "Hybrid Discrete-Continuous Systems" in Proc. Modern Computational Science 09, 2009.
@InProceedings{FraenzleEA:MCS, author = "Martin Fr{\"a}nzle and Andreas Eggers and Christian Herde and Tino Teige", title = "Hybrid Discrete-Continuous Systems", booktitle = "Modern Computational Science 09", editors = "Reinhard Leidl and Hartmann, Alexander K.", publisher = "BIS-Verlag der Carl von Ossietzky Universit{\"a}t Oldenburg", year = "2009", pages = "363--378"}
[inproceedings] bibtex
W. P. Heise, M. R. Hansen, und M. Fränzle, "A prototype of a model checker for Duration Calculus" in Proc. Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09, Kgs. Lyngby, Denmark, 2009.
@INPROCEEDINGS{WilliamEA:BranchingDCNWPT, author = {Heise, William Pihl and Hansen, Michael R. and Martin Fr{\"a}nzle}, title = {A prototype of a model checker for Duration Calculus}, booktitle = {Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09}, year = {2009}, address = {Kgs. Lyngby, Denmark}, publisher = {DTU Informatics, Danmarks Tekniske Universitet}, pages = {26--28} }
[article] bibtex
M. Fränzle und M. R. Hansen, "Efficient Model Checking for Duration Calculus" International Journal of Software and Informatics, vol. 3, iss. 2--3.
@Article{FraenzleHansen:BranchingTimeDCJournal, author = {Martin Fr{\"a}nzle and Hansen, Michael R.}, title = {Efficient Model Checking for Duration Calculus}, journal = {International Journal of Software and Informatics}, volume = "3", number = "2--3", pages = "171--196", year = {2009} }
[inproceedings] bibtex
J. Gacnic, H. Jost, F. Köster, J. Rataj, K. Lemmer, W. Damm, M. Fränzle, und E. Schnieder, "DeSCAS -- Formale Ontologien zur Verwebung von interdisziplinären Entwicklungsprozessen" in Proc. AUTOMATION 2009 -- Der Automatisierungskongress in Deutschland, Düsseldorf, 2009.
@inproceedings{GacnicEtAl, author = {Jan Gacnic and Henning Jost and Frank K{\"o}ster and J{\"u}rgen Rataj and Karsten Lemmer and Werner Damm and Martin Fr{\"a}nzle and Eckehard Schnieder}, title = {{DeSCAS} -- Formale Ontologien zur Verwebung von interdisziplin{\"a}ren Entwicklungsprozessen}, year = 2009, month = 6, publisher = {VDI Verlag}, address = {D{\"u}sseldorf}, booktitle = {{AUTOMATION} 2009 -- Der Automatisierungskongress in Deutschland}, series = {VDI-Berichte/VDI-Tagungsb{\"a}nde}, number = {2067}, issn = {0083-5560}, isbn = {978-3-18-092067-2}, pages = {449--453}, note = {Umfang der beigef. CD-ROM Version: 12 Seiten}

2008

[techreport] bibtex
T. Teige, C. Herde, M. Fränzle, und E. Ábrahám, "Conflict Analysis and Restarts in a mixed Boolean and Non-linear Arithmetic Constraint Solver" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 34, with 12 pages, 2008.
@techreport{atr34, author = {Tino Teige and Christian Herde and Martin Fr{\"a}nzle and Erika \'Abrah\'am}, title = {{Conflict Analysis and Restarts in a mixed Boolean and Non-linear Arithmetic Constraint Solver}}, editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, institution = {SFB/TR 14 AVACS}, subproject = {H1/2}, year = {2008}, month = {January}, type = {Reports of SFB/TR 14 AVACS}, series = {ATR}, number = {34, with 12 pages}, note = {ISSN: 1860-9821, http://www.avacs.org.}, access = {open}, abstract = { The recently presented constraint solver HySAT tackles the in general undecidable problem of solving mixed Boolean and non-linear arithmetic constraint formulae over the reals involving transcendental functions. The algorithmic core of HySAT is the iSAT algorithm, a tight integration of the Davis-Putnam-Logemann-Loveland algorithm with interval constraint propagation enriched by enhancements like conflict-driven clause learning and non-chronological backtracking. However, it was an open question whether HySAT's conflict analysis scheme, an adapted first unique implication point technique as applied in most modern SAT solvers, performs favorably compared to other schemes. In this paper, we compare several conflict analysis heuristics to answer this question. Furthermore, we consider the integration of restarts into the iSAT algorithm and investigate their impact. For our empirical results we use benchmarks from the hybrid systems domain.}, bibtex = {atr034.bib}, pdf = {avacs_technical_report_034.pdf} }
[techreport] bibtex
S. Kupferschmid, T. Teige, B. Becker, und M. Fränzle, "Proofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 40, with 13 pages, 2008.
@techreport{atr40, author = {Stefan Kupferschmid and Tino Teige and Bernd Becker and Martin Fr{\"a}nzle}, title = {{Proofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae}}, editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, institution = {SFB/TR 14 AVACS}, subproject = {H1/2}, year = {2008}, month = {June}, type = {Reports of SFB/TR 14 AVACS}, series = {ATR}, number = {40, with 13 pages}, note = {ISSN: 1860-9821, http://www.avacs.org.}, access = {open}, abstract = { In recent years, the use of constraint solvers for analysis and verification of industrial systems has become increasingly popular. The correctness and reliability of the results returned by the employed solvers are a vital requirement, in particular for safety-critical systems. If a solver proves the satisfiability of a constraint system and returns a solution then the answer of the solver can be validated by means of the solution. However, in case the solver claims that the constraint system is unsatisfiable without any certificate then the validation of this answer is not that simple. In this paper, we establish the theoretical basis of generating proofs of unsatisfiability in the mixed Boolean and non-linear arithmetic constraint framework over the reals and integers. To do so, we propose a simple rule-based calculus for unsatisfiable mixed Boolean-arithmetic constraints to produce and check unsatisfiability proofs. Furthermore, we enhance the iSAT constraint solver to generate unsatisfiability proofs, we implement a tool validating such proofs, and give some experimental results.}, bibtex = {atr040.bib}, pdf = {avacs_technical_report_040.pdf} }
[inproceedings] bibtex
A. Eggers, N. Kalinnik, S. Kupferschmid, und T. Teige, "Challenges in Constraint-based Analysis of Hybrid Systems" in Proc. Preproceedings of the Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming (CSCLP 2008), 2008.
@InProceedings{EggersEtAl08:Challenges, author = {A. Eggers and N. Kalinnik and S. Kupferschmid and T. Teige}, title = {{Challenges in Constraint-based Analysis of Hybrid Systems}}, booktitle = {Preproceedings of the Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming (CSCLP 2008)}, pages = {1-15}, year = {2008}, month = {June}, location = {Rome, Italy}, subproject = {H1/2}, access = {open}, note = {http://pst.istc.cnr.it/CSCLP08/program/papers/EggersEtalCSCLP2008.pdf}, bibtex = {eggers.csclp08.bib}, pdf = {eggers.csclp08.pdf}, abstract = { In the analysis of hybrid discrete-continuous systems, rich arithmetic constraint formulae with complex Boolean structure arise naturally. The iSAT algorithm, a solver for such formulae, is aimed at bounded model checking of hybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhance the iSAT algorithm: First, we propose an extension of iSAT to directly handle ordinary differential equations as constraints. Second, we outline the recently introduced generalization of the iSAT algorithm to deal with probabilistic hybrid systems and some open research issues in that context. Third, we present ideas on how to move from bounded to unbounded model checking by using the concept of interpolation. Finally, we discuss the adaption of some parallelization techniques to the iSAT case, which will hopefully lead to performance gains in the future. By presenting these open research questions, this paper aims at fostering discussions on these extensions of constraint solving.} }
[inproceedings] bibtex
M. Fränzle, H. Hermanns, und T. Teige, "Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems" in Proc. Pre-Proceedings of the ETAPS 2008 Sixth Workshop on Quantitative Aspects of Programming Languages (QAPL 2008), 2008.
@InProceedings{FraHerTei08:QAPL:SSMT, author = {M. Fr{\"a}nzle and H. Hermanns and T. Teige}, title = {{Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems}}, booktitle = {Pre-Proceedings of the ETAPS 2008 Sixth Workshop on Quantitative Aspects of Programming Languages (QAPL 2008)}, pages = {1-4}, year = {2008}, editor = {Alessandro Aldini and Christel Baier}, keywords = {Stochastic satisfiability, infinite domains, probabilistic hybrid automata, probabilistic bounded reachability.}, subproject = {H1/2,H4}, access = {open}, note = {http://www.avacs.org}, bibtex = {fraenzle.qapl08.bib}, pdf = {fraenzle.qapl08.pdf}, abstract = {The analysis of hybrid systems exhibiting probabilistic behaviour is notoriously difficult. To enable mechanised analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theory solving (SMT) by a comprehensive treatment of randomized (a.k.a. stochastic) quantification over discrete variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a fully symbolic analysis of probabilistic hybrid automata. Generalizing SMT-based bounded model-checking of hybrid automata [2,9], stochastic SMT permits the direct and fully symbolic analysis of probabilistic bounded reachability problems of probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.} }
[inproceedings] bibtex
M. Fränzle, H. Hermanns, und T. Teige, "Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems" in Proc. Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC'08), 2008.
@InProceedings{FraHerTei08:SSMT, author = {M. Fr{\"a}nzle and H. Hermanns and T. Teige}, title = {{Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems}}, booktitle = {Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC'08)}, pages = {172-186}, editor = {Magnus Egerstedt and Bud Mishra}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4981}, year = {2008}, note = {ISBN:978-3-540-78928-4}, subproject = {H1/2,H4}, bibtex = {fraenzle.hscc08.bib}, pdf = {fraenzle.hscc08.pdf}, access = {restricted}, abstract = {The analysis of hybrid systems exhibiting probabilistic behaviour is notoriously difficult. To enable mechanised analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulotheory solving (SMT) by a comprehensive treatment of randomized (a.k.a. stochastic) quantification over discrete variables within the mixed Booleanarithmetic constraint system. This provides the technological basis for a fully symbolic analysis of probabilistic hybrid automata. Generalizing SMT-based bounded model-checking of hybrid automata [2, 11], stochastic SMT permits the direct and fully symbolic analysis of probabilistic bounded reachability problems of probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.} }
[inproceedings] bibtex
T. Teige, "Stochastic Satisfiability Modulo Theory: A Technique for the Analysis of Probabilistic Hybrid Systems" in Proc. Proceedings des gemeinsamen Workshops der Graduiertenkollegs 2008, Dagstuhl, Berlin, 2008.
@INPROCEEDINGS{TeigeDagstuhl08:SSMT, author = {Tino Teige}, title = {{Stochastic Satisfiability Modulo Theory: A Technique for the Analysis of Probabilistic Hybrid Systems}}, booktitle = {Proceedings des gemeinsamen Workshops der Graduiertenkollegs 2008, Dagstuhl}, year = {2008}, editor = {Malte Diehl and Henrik Lipskoch and Roland Meyer and Christian Storm}, series = {Trustworthy Software Systems}, pages = {33--34}, address = {Berlin}, month = {May}, publisher = {Gito Verlag}, note = {ISBN: 978-3-940019-39-4}, location = {May 19--21, 2008, Dagstuhl, Germany} }
[inproceedings] bibtex
T. Teige und M. Fränzle, "Stochastic Satisfiability modulo Theories for Non-linear Arithmetic" in Proc. Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 5th International Conference, CPAIOR 2008, 2008.
@InProceedings{TeiFra08:nonlinearSSMT, author = {T. Teige and M. Fr{\"a}nzle}, title = {{Stochastic Satisfiability modulo Theories for Non-linear Arithmetic}}, booktitle = {Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 5th International Conference, CPAIOR 2008}, editor = {L. Perron and M.~A. Trick}, year = {2008}, pages = {248--262}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5015}, note = {ISBN: 978-3-540-68154-0}, subproject = {H1/2,H4}, access = {restricted}, bibtex = {teige.cpaior08.bib}, pdf = {teige.cpaior08.pdf}, abstract = {The stochastic satisfiability modulo theories (SSMT) problem is a generalization of the SMT problem on existential and randomized (aka. stochastic) quantification over discrete variables of an SMT formula. This extension permits the concise description of diverse problems combining reasoning under uncertainty with data dependencies. Solving problems with various kinds of uncertainty has been extensively studied in Artificial Intelligence. Famous examples are stochastic satisfiability and stochastic constraint programming. In this paper, we extend the algorithm for SSMT for decidable theories presented in [FHT08] to non-linear arithmetic theories over the reals and integers which are in general undecidable. Therefore, we combine approaches from Constraint Programming, namely the iSAT algorithm tackling mixed Boolean and non-linear arithmetic constraint systems, and from Artificial Intelligence handling existential and randomized quantifiers. Furthermore, we evaluate our novel algorithm and its enhancements on benchmarks from the probabilistic hybrid systems domain.} }
[techreport] bibtex
A. Eggers, M. Fränzle, und C. Herde, "SAT Modulo ODE: A Direct SAT approach to Hybrid Systems" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 37 with 14 Pages, 2008.
@TECHREPORT{atr37, author = {Andreas Eggers and Martin Fr{\"a}nzle and Christian Herde}, title = {{{SAT} Modulo {ODE}: A Direct {SAT} approach to Hybrid Systems}}, institution = {SFB/TR 14 AVACS}, year = {2008}, type = {Reports of SFB/TR 14 AVACS}, number = {37 with 14 Pages}, month = {April}, note = {ISSN: 1860-9821, http://www.avacs.org}, abstract = {In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving ordinary differential equations (ODEs), we provide a seamless integration of safe numeric overapproximation of initial-value problems into a SAT-modulo-theory (SMT) approach to interval-based arithmetic constraint solving. Interval-based safe numeric approximation of ODEs is used as an interval contractor being able to narrow candidate sets in phase space in both temporal directions: post-images of ODEs (i.e., sets of states reachable from a set of initial values) are narrowed based on partial information about the initial values and, vice versa, pre-images are narrowed based on partial knowledge about post-sets. In contrast to the related CLP(F) approach of Hickey and Wittenberg, we do (a) support coordinate transformations mitigating the wrapping effect encountered upon iterating interval-based overapproximations of reachable state sets and (b) embed the approach into an SMT framework, thus accelerating the solving process through the algorithmic enhacements of recent SAT solving technology. }, access = {open}, bibtex = {atr037.bib}, pdf = {avacs_technical_report_037.pdf}, editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, series = {ATR}, subproject = {H1/2} }
[inproceedings] bibtex
A. Eggers, M. Fränzle, und C. Herde, "SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems" in Proc. Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08), 2008.
@inproceedings{EggFraHer:ATVA08:SATmodODE, author = {Andreas Eggers and Martin Fr{\"a}nzle and Christian Herde}, title = {{SAT} Modulo {ODE}: A Direct {SAT} Approach to Hybrid Systems}, booktitle = {Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08)}, year = {2008}, pages = {171--185}, editor = {Sungdeok (Steve) Cha and Jin-Young Choi and Moonzoo Kim and Insup Lee and Mahesh Viswanathan}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5311}, note = {ISBN: 978-3-540-88386-9}, subproject = {H1/2}, bibtex = {eggers.atva08.bib}, pdf = {eggers.atva08.pdf}, access = {restricted}, abstract = {In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving ordinary differential equations (ODEs), we provide a seamless integration of safe numeric overapproximation of initial-value problems into a SAT-modulo-theory (SMT) approach to interval-based arithmetic constraint solving. Interval-based safe numeric approximation of ODEs is used as an interval contractor being able to narrow candidate sets in phase space in both temporal directions: post-images of ODEs (i.e., sets of states reachable from a set of initial values) are narrowed based on partial information about the initial values and, vice versa, pre-images are narrowed based on partial knowledge about post-sets. In contrast to the related CLP(F) approach of Hickey and Wittenberg, we do (a) support coordinate transformations mitigating the wrapping effect encountered upon iterating interval-based overapproximations of reachable state sets and (b) embed the approach into an SMT framework, thus accelerating the solving process through the algorithmic enhancements of recent SAT solving technology.} }
[inproceedings] bibtex
C. Herde, A. Eggers, M. Fränzle, und T. Teige, "Analysis of Hybrid Systems using HySAT" in Proc. The Third International Conference on Systems (ICONS 2008), 2008.
@InProceedings{HerEggFraTei08:HySAT, author = {C. Herde and A. Eggers and M. Fr{\"a}nzle and T. Teige}, title = {{Analysis of Hybrid Systems using {HySAT}}}, booktitle = {The Third International Conference on Systems (ICONS 2008)}, publisher = {IEEE Computer Society}, year = {2008}, pages = {196--201}, note = {ISBN: 978-0-7695-3105-2}, access = {restricted}, subproject = {H1/2}, bibtex = {herde.icons08.bib}, pdf = {herde.icons08.pdf}, abstract = {In this paper we describe the complete workflow of analyzing the dynamic behavior of safety-critical embedded systems with HySAT. HySAT is an arithmetic constraint solver with a tightly integrated bounded model checker for hybrid discrete-continuous systems which - in contrast to many other solvers - is not confined to linear arithmetic, but can also deal with nonlinear constraints involving transcendental functions. Based on a controller for train separation implementing a "moving block" interlocking scheme in the forthcoming European Train Control System Level 3, we exemplify the usage of the tool over the whole cycle from encoding a hybrid system to interpreting the results.} }
[inproceedings] bibtex | Dokument aufrufen
M. Swaminathan, M. Fränzle, und J. Katoen, "The Surprising Robustness of (Closed) Timed Automata against Clock-Drift." in Proc. Fifth IFIP International Conference on Theoretical Computer Science, 2008-09-15 2008.
@inproceedings{conf/ifipTCS/SwaminathanFK08, title = {{The Surprising Robustness of (Closed) Timed Automata against Clock-Drift.}}, author = {Mani Swaminathan and Martin Fr\"anzle and Joost-Pieter Katoen}, booktitle = {Fifth IFIP International Conference on Theoretical Computer Science}, editor = {Giorgio Ausiello and Juhani Karhum�ki and Giancarlo Mauri and C.-H. Luke Ong}, pages = {537-553}, publisher = {Springer}, series = {IFIP International Federation for Information Processing}, url = {http://dblp.uni-trier.de/db/conf/ifipTCS/ifipTCS2008.html#SwaminathanFK08}, volume = {273}, year = {2008}, biburl = {http://www.bibsonomy.org/bibtex/298ace7a31631e78231d29048d947dadd/dblp}, description = {dblp}, date = {2008-09-15}, ee = {http://dx.doi.org/10.1007/978-0-387-09680-3_36}, note = {ISBN: 978-0-387-09679-7}, keywords = {dblp } }
[inproceedings] bibtex
M. Fränzle und M. R. Hansen, "Efficient Model Checking for Duration Calculus Based on Branching-Time Approximations" in Proc. 6th IEEE International Conferences on Software Engineering and Formal Methods, 2008.
@InProceedings{FraenzleHansen08, author = {Fr\"anzle, Martin and Hansen, Michael R.}, title = {{Efficient Model Checking for Duration Calculus Based on Branching-Time Approximations}}, booktitle = {6th IEEE International Conferences on Software Engineering and Formal Methods}, pages = {63-72}, year = {2008}, month = {November}, publisher = {IEEE Computer Society Press}, note = {ISBN: 978-0-7695-3437-4}, subproject = {R1}, access = {restricted}, bibtex = {fraenzle.sefm08.bib}, pdf = {fraenzle.sefm08.pdf}, abstract = {Duration Calculus (abbreviated to DC) is an intervalbased, metric-time temporal logic designed for reasoning about embedded real-time systems at a high level of abstraction. But the complexity of model checking any decidable fragment featuring both negation and chop, DC's only modality, is non-elementary and thus impractical. We here investigate a similar approximation as frequently employed in model checking situation-based temporal logics, where linear-time problems are safely approximated by branching-time counterparts amenable to more efficient model-checking algorithms. Mimicking the role that a situation has in (A)CTL as origin of a set of linear traces, we define a branching-time counterpart to intervalbased temporal logics building on situation pairs spanning sets of intervals. While this branching-time interval semantics yields the desired reduction in complexity of the modelchecking problem, from non-elementary to linear in the size of the formula and cubic in the size of the model, the approximation is too coarse to be practical. We therefore refine the semantics by an occurrence count for crucial states (e.g., cuts of loops) in the model, arriving at a 4-fold exponential model-checking problem sufficiently accurately approximating the original one.}, }
[inproceedings] bibtex
M. Baumann, H. Colonius, H. Hungar, F. Köster, M. Langner, A. Lüdtke, C. Möbus, J. Peinke, S. Puch, C. Schiessl, R. Steenken, und L. Weber, "Integrated Modeling for Safe Transportation - Driver modeling and driver experiments." in Proc. Fahrermodellierung in Wissenschaft und Wirtschaft, 2. Berliner Fachtagung für Fahrermodellierung, 2008.
@INPROCEEDINGS {baumann_et_al_a08, author = {Baumann, M. and Colonius, H. and Hungar, H. and K\"oster, F. and Langner, M. and L\"udtke, A. and M\"obus, C. and Peinke, J. and Puch, S. and Schiessl, C. and Steenken, R. and Weber, L. }, BOOKTITLE = {Fahrermodellierung in Wissenschaft und Wirtschaft, 2. Berliner Fachtagung f\"ur Fahrermodellierung}, EDITOR = {J\"urgensohn and Kolrep}, PUBLISHER = {VDI Verlag}, SERIES = {Fortschrittsbericht des VDI in der Reihe 22 (Mensch-Maschine-Systeme)}, TITLE = {Integrated Modeling for Safe Transportation - Driver modeling and driver experiments. }, YEAR = {2008}

2007

[article] bibtex
B. Badban, J. van de Pol, O. Tveretina, und H. Zantema, "Generalizing DPLL and Satisfiability for Equalities" Journal of Information and Computation, vol. 205, iss. 8.
doi: 10.1016/j.ic.2007.03.003
@Article{bad07, author = "Bahareh Badban and Jaco van de Pol and Olga Tveretina and Hans Zantema", title = "Generalizing {DPLL} and Satisfiability for Equalities", year = "2007", journal = "Journal of Information and Computation", volume = {205}, number = {8}, year = {2007}, issn = {0890-5401}, pages = {1188--1211}, doi = {http://dx.doi.org/10.1016/j.ic.2007.03.003}, publisher = {Academic Press, Inc.}, address = {Duluth, MN, USA}, keywords = "satisfiability, DPLL procedure, equality, ground term algebra, inductive datatypes, decision procedure", }
[article] bibtex
B. Becker, W. Damm, M. Fränzle, E. Olderog, A. Podelski, und R. Wilhelm, "SFB/TR 14 AVACS -- Automatic Verification and Analysis of Complex Systems" it -- Information Technology, vol. 49, iss. 2.
@article{it2007, author = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, title = {{SFB/TR 14 AVACS} -- Automatic Verification and Analysis of Complex Systems}, journal= {it -- Information Technology}, volume = {49}, year = {2007}, number = {2}, pages = {118-126}, publisher={Oldenbourg Wissenschaftsverlag}, address= {M{\"u}nchen, Germany}, note = {http://it-Information-Technology.de, DOI 10.1524/itit.2007.49.2.118}, }
[inproceedings] bibtex
T. Teige, C. Herde, M. Fränzle, N. Kalinnik, und A. Eggers, "A Generalized Two-watched-literal Scheme in a mixed Boolean and Non-linear Arithmetic Constraint Solver" in Proc. Proceedings of the $13^th$ Portuguese Conference on Artificial Intelligence (EPIA 2007), 2007.
@inproceedings{TeigeEtAl2WAS, author = {Tino Teige and Christian Herde and Martin Fr\"anzle and Natalia Kalinnik and Andreas Eggers}, title = {A Generalized Two-watched-literal Scheme in a mixed Boolean and Non-linear Arithmetic Constraint Solver}, booktitle = {Proceedings of the $13^{th}$ Portuguese Conference on Artificial Intelligence (EPIA 2007)}, series = {New Trends in Artificial Intelligence}, editor = {Jos{\'e} Neves and Manuel Filipe Santos and Jos{\'e} Manuel Machado}, publisher = {APPIA}, year = {2007}, month = {December}, location = {Guimar\~{a}es, Portugal}, pages = {729--741}, subproject = {H1, H2}, access={restricted}, bibtex={teige.epia07.bib}, pdf={teige.epia07.pdf}, abstract = {In its combination with conflict-driven clause learning the two-watched-literal scheme led to enormous performance gains in propositional SAT solving. The idea of this approach is to accelerate the deduction phase of a SAT solver by saving a high number of unnecessary and expensive computation steps originating in visits of indefinite clauses. In this paper we give a detailed explanation of the generalized watch scheme, called \emph{two-watched-atom scheme}, implemented in our interval-based constraint solver HySAT, the latter being a solver for mixed Boolean and non-linear arithmetic constraint formulae. As opposed to the purely Boolean setting, the more general form of atomic formulae to be watched in our solver necessitates an extension of the original scheme and calls for a careful design of the data structures employed in the implementation. We present experimental results to demonstrate the speed-up obtained by the proposed scheme.}, }
[inproceedings] bibtex
M. Swaminathan und M. Fränzle, "A Symbolic Decision Procedure for Robust Safety of Timed Systems" in Proc. proceedings on the 14th International Symposium on Temporal Representation and Reasoning (TIME 2007), 2007.
@INPROCEEDINGS{swaminathan07, author={Mani Swaminathan and Martin Fr{\"a}nzle}, title={A Symbolic Decision Procedure for Robust Safety of Timed Systems}, note={To appear as a short paper/poster}, booktitle={proceedings on the 14th International Symposium on Temporal Representation and Reasoning (TIME 2007)}, publisher={IEEE CS Press}, year={2007}, subproject={H1}, access={restricted}, bibtex={swaminathan.time07.bib}, pdf={swaminathan.time07.pdf}, abstract={We present a symbolic algorithm for deciding safety (reachability) of timed systems modelled as Timed Automata (TA), under the notion of robustness w.r.t infinitesimal clock-drift. The algorithm uses a ``neighbourhood'' operator on zones that is efficient to compute. In contrast to other approaches for robustly deciding reachability of TA, which are either region-based (Puri, 2000), (DeWulf, Doyen, Markey, and Raskin, 2004), or involve a combination of forward and backward analyses when zone-based (Daws and Kordy, 2006), ours is a zone-based fully forward algorithm that is guaranteed to terminate, requires no special treatment of cycles in TA, and can be applied to target states that need not be closed.}, }
[inproceedings] bibtex
M. Fränzle und M. R. Hansen, "Deciding an Interval Logic with Accumulated Durations" in Proc. Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 07), 2007.
@InProceedings{FraenzleHansen:TACAS07, author = {Fr{\"a}nzle, Martin and Hansen, Michael R.}, title = {Deciding an Interval Logic with Accumulated Durations}, booktitle = {Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 07)}, year = {2007}, editor = {Grumberg, Orna and Huth, Michael}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, volume = {4424}, pages = {201--215}, keywords = {Real-time systems, metric-time temporal logic, decidability, model-checking, multi-priced timed automata}, subproject = {H1}, access = {restricted}, pdf = {fraenzle.tacas07.pdf}, bibtex = {fraenzle.tacas07.bib}, abstract = {A decidability result and a model-checking procedure for a rich subset of Duration Calculus (DC) [19] is obtained through reductions to is obtained through reductions to First-order logic over the real-closed field and to Multi-Priced Timed Automata (MPTA) [13]. In contrast to other reductions of fragments of DC to reachability problems in timed automata, the reductions do also cover constraints on positive linear combinations of accumulated durations. By being able to handle accumulated durations under chop as well as in arbitrary positive Boolean contexts, the procedures extend the results of Zhou et al. [22] on decidability of linear duration invariants to a much wider fragment of DC.}, }
[inproceedings] bibtex
T. Teige, "SAT-Modulo-Theory based Analysis of Probabilistic Hybrid Systems" in Proc. Proceedings of the Dagstuhl Graduate School Meeting 2007 ``Dagstuhl Zehn plus Eins'', Aachen, 2007.
@InProceedings{Teige07:SSMT, author = {T. Teige}, title = {{SAT-Modulo-Theory based Analysis of Probabilistic Hybrid Systems}}, booktitle = {{Proceedings of the Dagstuhl Graduate School Meeting 2007 ``Dagstuhl Zehn plus Eins''}}, address = {Aachen}, year = {2007}, pages = {86--87}, publisher = {Verlag Mainz}, note = {{ISBN:} 3-86130-882-7}, }
[article] bibtex
M. Fränzle, C. Herde, S. Ratschan, T. Schubert, und T. Teige, "Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure" JSAT Special Issue on Constraint Programming and SAT, vol. 1.
@Article{FraenzleEA:iSAT:JSAT, author = {Martin Fr{\"a}nzle and Christian Herde and Stefan Ratschan and Tobias Schubert and Tino Teige}, title = {Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure}, editor = {Y. Hamadi and L. Bordeaux}, journal = {JSAT Special Issue on Constraint Programming and SAT}, volume = {1}, pages = {209-236}, year = {2007}, note = {accepted for publication}, subproject = {H1,H2}, access={restricted}, bibtex={fraenzle.jsat07.bib}, pdf={fraenzle.jsat07.pdf}, abstract={ In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions, we provide a tight integration of recent SAT solving techniques with interval-based arithmetic constraint solving. Our approach deviates substantially from lazy theorem proving approaches in that it directly controls arithmetic constraint propagation from the SAT solver rather than delegating arithmetic decisions to a subordinate solver. Through this tight integration, all the algorithmic enhancements that were instrumental to the enormous performance gains recently achieved in propositional SAT solving do smoothly carry over to the rich domain of non-linear arithmetic constraints. As a consequence, our approach is able to handle large constraint systems with extremely complex Boolean structure, involving Boolean combinations of multiple thousand arithmetic constraints over some thousands of variables.}, }
[article] bibtex | Dokument aufrufen
M. Fränzle und C. Herde, "HySAT: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems" Formal Methods in System Design, vol. 30.
@article{ FraenzleHerde05, author = {Martin Fr{\"a}nzle and Christian Herde}, title = {{HySAT}: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems}, journal = {Formal Methods in System Design}, volume = 30, year = 2007, pages = {179--198}, publisher = {Springer Verlag}, keywords = {verification, bounded model checking, hybrid systems, infinite-state systems, decision procedures, satisfiability}, url = {http://dx.doi.org/10.1007/s10703-006-0031-0}, subproject = {H2}, language = {USenglish}, access = {restricted}, abstract = {In this paper we present HySAT, a new bounded model checker for linear hybrid systems, incorporating a tight integration of a DPLL--based pseudo--Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits all of the various optimizations that arise naturally in the bounded model checking context, e.g.~isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.}, bibtex = {FMSD05_Fraenzle_Herde.bib}, pdf = {FMSD05_Fraenzle_Herde.pdf}, postscript = {FMSD05_Fraenzle_Herde.ps} }
[techreport] bibtex
T. Teige, C. Herde, M. Fränzle, und E. Ábrahám, "Conflict Analysis and Restarts in a mixed Boolean and Non-linear Arithmetic Constraint Solver" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 34, 2008.
@techreport{atr34, author = {Tino Teige and Christian Herde and Martin Fr{\"a}nzle and Erika \'Abrah\'am}, title = {Conflict Analysis and Restarts in a mixed Boolean and Non-linear Arithmetic Constraint Solver}, editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, institution = {SFB/TR 14 AVACS}, subproject = {H1/2}, year = {2008}, month = {January}, type = {Reports of SFB/TR 14 AVACS}, series = {ATR}, number = 34, note = {ISSN: 1860-9821, http://www.avacs.org.}, access = {open}, abstract = { The recently presented constraint solver HySAT tackles the in general undecidable problem of solving mixed Boolean and non-linear arithmetic constraint formulae over the reals involving transcendental functions. The algorithmic core of HySAT is the iSAT algorithm, a tight integration of the Davis-Putnam-Logemann-Loveland algorithm with interval constraint propagation enriched by enhancements like conflict-driven clause learning and non-chronological backtracking. However, it was an open question whether HySAT's conflict analysis scheme, an adapted first unique implication point technique as applied in most modern SAT solvers, performs favorably compared to other schemes. In this paper, we compare several conflict analysis heuristics to answer this question. Furthermore, we consider the integration of restarts into the iSAT algorithm and investigate their impact. For our empirical results we use benchmarks from the hybrid systems domain.}, bibtex = {atr034.bib}, pdf = {avacs_technical_report_034.pdf} }
[techreport] bibtex
M. Fränzle, H. Hungar, C. Schmitt, und B. Wirtz, "HLang: Compositional Representation of Hybrid Systems via Predicates" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 20, 2007.
@techreport{atr20, author = {Martin Fr{\"a}nzle and Hardi Hungar and Christian Schmitt and Boris Wirtz}, title = {HLang: Compositional Representation of Hybrid Systems via Predicates}, editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, institution = {SFB/TR 14 AVACS}, subproject = {H1/2,H3}, year = {2007}, month = {July}, type = {Reports of SFB/TR 14 AVACS}, series = {ATR}, number = 20, note = {ISSN: 1860-9821, http://www.avacs.org}, access = {open}, abstract = { Given the structural diversity of modeling paradigms for hybrid systems that are in widespread use, which ranges from a signal-transducer-based view like in Simulink/Stateflow to an automaton-based view in various hybrid automata frameworks, there is need for an intermediate-level language that can accommodate these structures in a concise way, thereby isolating verification backends from the particular modeling frontend used. This technical report provides a description of the intermediate-level modeling language for hybrid systems used in project area H of AVACS as a gateway to verification backends. }, bibtex = {atr020.bib}, pdf = {avacs_technical_report_020.pdf} }
[inproceedings] bibtex
E. Ábrahám, T. Schubert, B. Becker, M. Fränzle, und C. Herde, "Parallel SAT Solving in Bounded Model Checking" in Proc. Formal Methods: Applications and Technology, 11th International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers, 2007.
@inproceedings{DBLP:conf/fmics/AbrahamSBFH06, author = {Erika {\'A}brah{\'a}m and Tobias Schubert and Bernd Becker and Martin Fr{\"a}nzle and Christian Herde}, title = {Parallel SAT Solving in Bounded Model Checking}, editor = {Lubos Brim and Boudewijn R. Haverkort and Martin Leucker and Jaco van de Pol}, booktitle = {Formal Methods: Applications and Technology, 11th International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4346}, year = {2007}, isbn = {978-3-540-70951-0}, pages = {301-315}, ee = {http://dx.doi.org/10.1007/978-3-540-70952-7_21}, }
[inproceedings] bibtex
M. Fränzle, "Verification of Hybrid Systems (Invited Tutorial)" in Proc. Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, 2007, p. 38.
@inproceedings{DBLP:conf/cav/Franzle07, author = {Martin Fr{\"a}nzle}, title = {Verification of Hybrid Systems (Invited Tutorial)}, booktitle = {Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings}, editor = {Werner Damm and Holger Hermanns}, year = {2007}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4590}, pages = {38}, ee = {http://dx.doi.org/10.1007/978-3-540-73368-3_7}, isbn = {978-3-540-73367-6}, bibsource = {DBLP, http://dblp.uni-trier.de}

2006

[phdthesis] bibtex
B. Badban, "Verification techniques for Extensions of equality logic" PhD Thesis , 2006.
@PhdThesis{badban07, author = "Bahareh Badban", title = "Verification techniques for Extensions of equality logic", school = "Vrije Universiteit of Amsterdam", year = "2006", OPTmonth = "September", }
[inproceedings] bibtex
M. Fränzle, C. Herde, S. Ratschan, T. Schubert, und T. Teige, "Interval Constraint Solving Using Propositional SAT Solving Techniques" in Proc. Proceedings of the CP 2006 First International Workshop on the Integration of SAT and CP Techniques, 2006.
@InProceedings{FraenzleEA:iSAT, author = "Martin Fr{\"a}nzle and Christian Herde and Stefan Ratschan and Tobias Schubert and Tino Teige", title = "Interval Constraint Solving Using Propositional {SAT} Solving Techniques", booktitle = "Proceedings of the CP 2006 First International Workshop on the Integration of SAT and CP Techniques", pages = "81--95", year = "2006", }
[inproceedings] bibtex
A. Metzner, M. Fränzle, C. Herde, und I. Stierand, "An Optimal Approach to the Task Allocation Problem on Hierarchical Architectures" in Proc. Proceedings of the 20th IEEE International Parallel and Distributed Processing Symposium, 2006.
@InProceedings{wpdrts, author = "A. Metzner and M. Fr{\"a}nzle and C. Herde and I. Stierand", title = "{An Optimal Approach to the Task Allocation Problem on Hierarchical Architectures}", booktitle = "{Proceedings of the 20th IEEE International Parallel and Distributed Processing Symposium}", publisher = "IEEE Computer Society", year = "2006", access = "restricted", subproject = "R2,H2", bibtex = "wpdrts06.bib", annote = "(8 pages)", }
[article] bibtex
M. Fränzle und C. Herde, "HySAT: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems" Formal Methods in System Design.
@Article{FraenzleHerde05, author = "Martin Fr{\"a}nzle and Christian Herde", title = "{HySAT}: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems", journal = "Formal Methods in System Design", year = "2006", publisher = "Springer", keywords = "verification, bounded model checking, hybrid systems, infinite-state systems, decision procedures, satisfiability", subproject = "H2", language = "USenglish", access = "restricted", }
[inproceedings] bibtex
A. Metzner und C. Herde, "RTSAT -- An Optimal and Efficient Approach to the Task Allocation Problem in Distributed Architectures" in Proc. Proceedings of the IEEE Real-Time Systems Symposium, 2006.
@InProceedings{rtss06, author = "Alexander Metzner and Christian Herde", title = "{RTSAT} -- An Optimal and Efficient Approach to the Task Allocation Problem in Distributed Architectures", booktitle = "Proceedings of the IEEE Real-Time Systems Symposium", year = "2006", pages = "147--156", publisher = "IEEE Computer Society", }
[inproceedings] bibtex
B. Badban, M. Fränzle, J. Peleska, und T. Teige, "Test Automation for Hybrid Systems" in Proc. Proceedings of the Third International Workshop on SOFTWARE QUALITY ASSURANCE (SOQUA 2006), Portland Oregon, USA, 2006.
@InProceedings{bfpt2006a, author = "Bahareh Badban and Martin Fr{\"{a}}nzle and Jan Peleska and Tino Teige", title = "Test Automation for Hybrid Systems", booktitle = "Proceedings of the Third International Workshop on SOFTWARE QUALITY ASSURANCE (SOQUA 2006)", pages = "14--21", year = "2006", address = "Portland Oregon, USA", }
[inproceedings] bibtex
M. Swaminathan und M. Fränzle, "Robust Zone-Based Forward Reachability Analysis of Timed Automata" in Proc. Proceedings of the 7th School on Modelling and Verifying of parallel Processes (MOVEP 06), Bordeaux, France, 2006.
@InProceedings{SwaFr06, author = "Mani Swaminathan and Martin Fr{\"a}nzle", title = "Robust Zone-Based Forward Reachability Analysis of Timed Automata", booktitle = "Proceedings of the 7th School on Modelling and Verifying of parallel Processes (MOVEP 06)", year = "2006", month = jun, address = "Bordeaux, France",

2005

[inproceedings] bibtex
A. Metzner, M. Fränzle, C. Herde, und I. Stierand, "Scheduling Distributed Real-Time Systems by Satisfiability Checking" in Proc. Proceedings of the IEEE Conference on Embedded and Real-Time Computing Systems and Applications, 2005.
@InProceedings{rtcsa, author = "A. Metzner and M. Fr{\"a}nzle and C. Herde and I. Stierand", title = "{Scheduling Distributed Real-Time Systems by Satisfiability Checking}", booktitle = "Proceedings of the IEEE Conference on Embedded and Real-Time Computing Systems and Applications", publisher = "IEEE Computer Society", pages = "409--415", year = "2005", subproject = "R2,H2", access = "restricted", }
[inproceedings] bibtex
M. Fränzle und M. R. Hansen, "A robust interpretation of duration calculus" in Proc. Proceedings of ICTAC 05 International Colloquium on Theoretical Aspects of Computing, 2005.
@InProceedings{Franzle05, author = "M. Fr{\"a}nzle and M. R. Hansen", title = "A robust interpretation of duration calculus", booktitle = "Proceedings of ICTAC 05 International Colloquium on Theoretical Aspects of Computing", year = "2005", editor = "Dang Van Hung and Martin Wirsing", volume = "3722", series = LNCS, pages = "257--271", publisher = "Springer Verlag", }
[article] bibtex
M. Fränzle und C. Herde, "Efficient proof engines for bounded model checking of hybrid systems" Electronic Notes in Theoretical Computer Science, vol. 133.
@Article{Franzle05b, author = "M. Fr{\"a}nzle and C. Herde", title = "Efficient proof engines for bounded model checking of hybrid systems", journal = "Electronic Notes in Theoretical Computer Science", year = "2005", volume = "133", number = "", pages = "119--137", month = "", note = "", }
[inproceedings] bibtex
A. Metzner und C. Herde, "RTSAT -- Scheduling Tasks in Distributed Real-Time Systems by Enhanced Satisifiability Checking" in Proc. Proceedings of the IEEE Real-Time Systems Symposium, Work in Progress Session, 2005.
@InProceedings{rtss05, author = "Alexander Metzner and Christian Herde", title = "{{RTSAT} -- Scheduling Tasks in Distributed Real-Time Systems by Enhanced Satisifiability Checking}", booktitle = "Proceedings of the IEEE Real-Time Systems Symposium, Work in Progress Session", year = "2005", }
[inproceedings] bibtex
J. Enslev, A. Nielsen, M. Fränzle, und M. R. Hansen, "Bounded Model Construction for Duration Calculus" in Proc. Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05), Københavns Universitet, 2005.
@InProceedings{EnslevNielsenFraenzleHansenBMCforDC, author = "Jacob Enslev and Anne-Sofie Nielsen and Martin Fr{\"a}nzle and Michael R. Hansen", title = "Bounded Model Construction for Duration Calculus", booktitle = "Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05)", editor = "Jones, Neil et al.", year = "2005", month = oct, address = "K{\o}benhavns Universitet", }
[inproceedings] bibtex
M. Swaminathan und M. Fränzle, "Automatic and scalable verification of robust real-time systems" in Proc. Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05), Københavns Universitet, 2005.
@InProceedings{SwaminathanFraenzle, author = "Mani Swaminathan and Martin Fr{\"a}nzle", title = "Automatic and scalable verification of robust real-time systems", booktitle = "Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05)", editor = "Jones, Neil et al.", year = "2005", month = oct, address = "K{\o}benhavns Universitet",

2004

[inproceedings] bibtex
M. Fränzle und M. R. Hansen, "A robust interpretation of duration calculus" in Proc. Proceedings of NWPT 04 16th Nordic Workshop on Programming Theory, 2004.
@InProceedings{Franzle04, author = "M. Fr{\"a}nzle and M. R. Hansen", title = "A robust interpretation of duration calculus", booktitle = "Proceedings of NWPT 04 16th Nordic Workshop on Programming Theory", year = "2004", editor = "P. Pettersson and W. Yi", pages = "", organization = "Uppsala University", publisher = "Dept. of Information Technology", address = "", month = "", note = "", }
[article] bibtex
M. Fränzle, "Model-checking dense-time duration calculus" Formal Aspects of Computing, vol. 16, iss. 2.
@Article{Franzle04a, author = "M. Fr{\"a}nzle", title = "Model-checking dense-time duration calculus", journal = "Formal Aspects of Computing", year = "2004", volume = "16", number = "2", pages = "121--139", month = "", note = "", publisher = "Springer Verlag", }
[inproceedings] bibtex
B. Becker, M. Behle, F. Eisenbrand, M. Fränzle, M. Herbstritt, C. Herde, J. Hoffmann, D. Kröning, B. Nebel, I. Polian, und R. Wimmer, "Bounded model checking and inductive verification of hybrid discrete-continuous systems" in Proc. GI/ITG/GMM Workshop 'Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen', 2004.
@InProceedings{Franzle04b, author = "B. Becker and M. Behle and F. Eisenbrand and M. Fr{\"a}nzle and M. Herbstritt and C. Herde and J. Hoffmann and D. Kr{\"o}ning and B. Nebel and I. Polian and R. Wimmer", title = "Bounded model checking and inductive verification of hybrid discrete-continuous systems", booktitle = "{GI/ITG/GMM Workshop 'Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'}", year = "2004", editor = "", pages = "65--75", organization = "", publisher = "Universit{\"a}t Kaiserslautern", address = "", month = feb, note = "",

2003

[inproceedings] bibtex
M. Fränzle und C. Herde, "Efficient SAT Engines for Concise Logics: Accelerating Proof Search for Zero-One Linear Constraint Systems" in Proc. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003, 2003.
@inproceedings{FraenzleHerdeLPAR2003, author = {Martin Fr{\"a}nzle and Christian Herde}, title = {Efficient SAT Engines for Concise Logics: Accelerating Proof Search for Zero-One Linear Constraint Systems}, editor = {Mosche Vardi and Andrei Voronkov}, year = 2003, isbn = {978-3-540-20101-4}, publisher = {Springer}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003}, series = {Lecture Notes in Artificial Intelligence}, volume = 2850, pages = {302--316} }
[article] bibtex | Dokument aufrufen
M. Fränzle, J. Niehaus, A. Metzner, und W. Damm, "A Semantics for Distributed Execution of Statemate" Formal Aspects of Computing, vol. V15, iss. 4.
doi: 10.1007/s00165-003-0015-4
@article{franzle_03_semantics, author = {Fr\"{a}nzle, Martin and Niehaus, J\"{u}rgen and Metzner, Alexander and Damm, Werner }, citeulike-article-id = {887517}, doi = {http://dx.doi.org/10.1007/s00165-003-0015-4}, journal = {Formal Aspects of Computing}, keywords = {2003, distributed, semantics, statecharts, statemate}, month = {December}, number = {4}, pages = {390--405}, posted-at = {2006-10-06 20:32:37}, priority = {3}, title = {A Semantics for Distributed Execution of Statemate}, url = {http://dx.doi.org/10.1007/s00165-003-0015-4}, volume = {V15}, year = {2003}

2002

[inproceedings] bibtex
M. Fränzle, "Take It NP-Easy: Bounded Model Construction for Duration Calculus" in Proc. FTRTFT '02: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, London, UK, 2002.
@inproceedings{707111, author = {Martin Fr\"{a}nzle}, title = {Take It NP-Easy: Bounded Model Construction for Duration Calculus}, booktitle = {FTRTFT '02: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems}, year = {2002}, series= {Lecture Notes in Computer Science}, volume= {2469}, isbn = {3-540-44165-4}, pages = {245--264}, publisher = {Springer-Verlag}, address = {London, UK},

Sprache wechseln

Change Language

Hell-/Dunkelmodus

Light mode / Dark mode

Publikationen

Kontakt

Leitung

Sekretariat

Publikationen

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002