B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory" in
Proc. 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), 2022.
doi:
10.4230/LIPIcs.CSL.2022.20@inproceedings{DBLP:conf/csl/FinkbeinerGHO22,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
title = {Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory},
booktitle = {30th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2022, February 14-19, 2022, G{\"{o}}ttingen, Germany (Virtual Conference)},
pages = {20:1--20:19},
year = {2022},
url = {https://doi.org/10.4230/LIPIcs.CSL.2022.20},
doi = {10.4230/LIPIcs.CSL.2022.20},
timestamp = {Thu, 27 Jan 2022 17:51:51 +0100},
biburl = {https://dblp.org/rec/conf/csl/FinkbeinerGHO22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
K. R. Apt und E. -R. Olderog,
Nondeterminism and Guarded CommandsACM / Morgan & Claypool, 2022.
doi:
10.1145/3544585.3544595@incollection{DBLP:books/mc/22/AptO22,
author = {Krzysztof R. Apt and E.-R. Olderog},
editor = {Krzysztof R. Apt and Tony Hoare},
title = {Nondeterminism and Guarded Commands},
booktitle = {Edsger Wybe Dijkstra: His Life, Work, and Legacy},
pages = {169--204},
publisher = {{ACM} / Morgan {\&} Claypool},
year = {2022},
url = {https://doi.org/10.1145/3544585.3544595},
doi = {10.1145/3544585.3544595},
timestamp = {Fri, 15 Jul 2022 10:31:05 +0200},
biburl = {https://dblp.org/rec/books/mc/22/AptO22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
G. K. A. -, S. Haar, L. Paulevé, S. Schwoon, und N. Würdemann, "Avoid One's Doom: Finding Cliff-Edge Configurations in Petri Nets" in
Proc. Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2022, Madrid, Spain, September 21-23, 2022, 2022.
doi:
10.4204/EPTCS.370.12@inproceedings{DBLP:journals/corr/abs-2209-10323,
author = {Giann Karlo Aguirre{-}Samboni and Stefan Haar and Loic Paulev{\'{e}} and Stefan Schwoon and Nick W{\"{u}}rdemann},
editor = {Pierre Ganty and Dario Della Monica},
title = {Avoid One's Doom: Finding Cliff-Edge Configurations in Petri Nets},
booktitle = {Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2022, Madrid, Spain, September 21-23, 2022},
series = {{EPTCS}},
volume = {370},
pages = {178--193},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.370.12},
doi = {10.4204/EPTCS.370.12},
timestamp = {Mon, 31 Oct 2022 12:23:58 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2209-10323.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
P. Hannibal und E. -R. Olderog, "The Synthesis Problem for Repeatedly Communicating Petri Games" in
Proc. Application and Theory of Petri Nets and Concurrency - 43rd International Conference, PETRI NETS 2022, Bergen, Norway, June 19-24, 2022, Proceedings, 2022.
doi:
10.1007/978-3-031-06653-5_13@inproceedings{DBLP:conf/apn/HannibalO22,
author = {Paul Hannibal and E.-R. Olderog},
editor = {Luca Bernardinello and Laure Petrucci},
title = {The Synthesis Problem for Repeatedly Communicating Petri Games},
booktitle = {Application and Theory of Petri Nets and Concurrency - 43rd International Conference, {PETRI} {NETS} 2022, Bergen, Norway, June 19-24, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13288},
pages = {236--257},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-06653-5\_13},
doi = {10.1007/978-3-031-06653-5\_13},
timestamp = {Mon, 20 Jun 2022 16:55:49 +0200},
biburl = {https://dblp.org/rec/conf/apn/HannibalO22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
B. Finkbeiner, M. Gieseking, J. H. -, und E. -R. Olderog, "Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory" in
Proc. 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), 2022.
doi:
10.4230/LIPIcs.CSL.2022.20@inproceedings{DBLP:conf/csl/FinkbeinerGHO22,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking{-}Harbusch and E.-R Olderog},
editor = {Florin Manea and Alex Simpson},
title = {Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory},
booktitle = {30th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2022, February 14-19, 2022, G{\"{o}}ttingen, Germany (Virtual Conference)},
series = {LIPIcs},
volume = {216},
pages = {20:1--20:19},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022},
url = {https://doi.org/10.4230/LIPIcs.CSL.2022.20},
doi = {10.4230/LIPIcs.CSL.2022.20},
timestamp = {Thu, 27 Jan 2022 17:51:51 +0100},
biburl = {https://dblp.org/rec/conf/csl/FinkbeinerGHO22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
C. Bischopink und E. -R. Olderog, "Spatial and Timing Properties in Highway Traffic" in
Proc. Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings, 2022.
doi:
10.1007/978-3-031-17715-6_9@inproceedings{DBLP:conf/ictac/BischopinkO22,
author = {Christopher Bischopink and E.-R. Olderog},
editor = {Helmut Seidl and Zhiming Liu and Corina S. Pasareanu},
title = {Spatial and Timing Properties in Highway Traffic},
booktitle = {Theoretical Aspects of Computing - {ICTAC} 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13572},
pages = {114--131},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-17715-6\_9},
doi = {10.1007/978-3-031-17715-6\_9},
timestamp = {Fri, 07 Oct 2022 16:33:00 +0200},
biburl = {https://dblp.org/rec/conf/ictac/BischopinkO22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
M. Gieseking und N. Würdemann, "Canonical Representations for Direct Generation of Strategies in High-level Petri Games (Full Version)" CoRR, vol. abs/2103.10207, 2021.
@article{DBLP:journals/corr/abs-2103-10207,
author = {Manuel Gieseking and Nick W{\"{u}}rdemann},
title = {Canonical Representations for Direct Generation of Strategies in High-level Petri Games (Full Version)},
journal = {CoRR},
volume = {abs/2103.10207},
year = {2021},
url = {https://arxiv.org/abs/2103.10207},
archiveprefix = {arXiv},
eprint = {2103.10207},
biburl = {https://dblp.org/rec/journals/corr/abs-2103-10207.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/mc/21/AptO21,
author = {Krzysztof R. Apt and Ernst-R{\"{u}}diger Olderog},
title = {Assessing the Success and Impact of Hoare's Logic},
booktitle = {Theories of Programming: The Life and Works of Tony Hoare},
pages = {41--76},
year = {2021},
url = {https://doi.org/10.1145/3477355.3477359},
doi = {10.1145/3477355.3477359},
timestamp = {Tue, 05 Oct 2021 10:22:06 +0200},
biburl = {https://dblp.org/rec/books/mc/21/AptO21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
M. Gieseking und E. Olderog, "High-Level Representation of Benchmark Families for Petri Games" in
Proc. Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday, 2021.
doi:
10.1007/978-3-030-91384-7_7@inproceedings{DBLP:conf/birthday/GiesekingO21,
author = {Manuel Gieseking and Ernst-R{\"{u}}diger Olderog},
title = {High-Level Representation of Benchmark Families for Petri Games},
booktitle = {Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday},
pages = {115--137},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-91384-7\_7},
doi = {10.1007/978-3-030-91384-7\_7},
timestamp = {Fri, 21 Jan 2022 22:02:45 +0100},
biburl = {https://dblp.org/rec/conf/birthday/GiesekingO21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
E. Olderog, B. Steffen, und W. Yi, "Model Checking, Synthesis, and Learning" in
Proc. Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday, 2021.
doi:
10.1007/978-3-030-91384-7_1@inproceedings{DBLP:conf/birthday/OlderogS021,
author = {Ernst-R{\"{u}}diger Olderog and Bernhard Steffen and Wang Yi},
title = {Model Checking, Synthesis, and Learning},
booktitle = {Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday},
pages = {1--7},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-91384-7\_1},
doi = {10.1007/978-3-030-91384-7\_1},
timestamp = {Tue, 11 Jan 2022 18:34:32 +0100},
biburl = {https://dblp.org/rec/conf/birthday/OlderogS021.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
O. Özkan und N. Würdemann, "Resilience of Well-structured Graph Transformation Systems" CoRR, vol. abs/2108.00889, 2021.
@article{DBLP:journals/corr/abs-2108-00889,
author = {Okan {\"{O}}zkan and Nick W{\"{u}}rdemann},
title = {Resilience of Well-structured Graph Transformation Systems},
journal = {CoRR},
volume = {abs/2108.00889},
year = {2021},
url = {https://arxiv.org/abs/2108.00889},
eprinttype = {arXiv},
eprint = {2108.00889},
timestamp = {Thu, 05 Aug 2021 14:27:08 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2108-00889.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
E. Olderog, M. Fränzle, O. E. Theel, und P. Kröger, "System correctness under adverse conditions"
it Inf. Technol. vol. 63, iss. 5-6, 2021.
doi:
10.1515/itit-2021-0043@article{DBLP:journals/it/OlderogFTK21,
author = {Ernst-R{\"{u}}diger Olderog and Martin Fr{\"{a}}nzle and Oliver E. Theel and Paul Kr{\"{o}}ger},
title = {System correctness under adverse conditions},
journal = {it Inf. Technol.},
volume = {63},
number = {5-6},
pages = {249--251},
year = {2021},
url = {https://doi.org/10.1515/itit-2021-0043},
doi = {10.1515/itit-2021-0043},
timestamp = {Fri, 19 Nov 2021 11:34:13 +0100},
biburl = {https://dblp.org/rec/journals/it/OlderogFTK21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
N. Würdemann, "Exploiting symmetries of high-level Petri games in distributed synthesis"
it Inf. Technol. vol. 63, iss. 5-6, 2021.
doi:
10.1515/itit-2021-0012@article{DBLP:journals/it/Wurdemann21,
author = {Nick W{\"{u}}rdemann},
title = {Exploiting symmetries of high-level Petri games in distributed synthesis},
journal = {it Inf. Technol.},
volume = {63},
number = {5-6},
pages = {321--331},
year = {2021},
url = {https://doi.org/10.1515/itit-2021-0012},
doi = {10.1515/itit-2021-0012},
timestamp = {Fri, 19 Nov 2021 11:34:13 +0100},
biburl = {https://dblp.org/rec/journals/it/Wurdemann21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th BirthdaySpringer, 2021.
doi:
10.1007/978-3-030-91384-7 @proceedings{DBLP:conf/birthday/2021jonsson, editor = {Ernst-R{\"{u}}diger Olderog and Bernhard Steffen and Wang Yi},
title = {Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday},
series = {Lecture Notes in Computer Science},
volume = {13030},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-91384-7},
doi = {10.1007/978-3-030-91384-7},
isbn = {978-3-030-91383-0},
timestamp = {Tue, 11 Jan 2022 18:33:29 +0100},
biburl = {https://dblp.org/rec/conf/birthday/2021jonsson.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
M. Gieseking und N. Würdemann, "Canonical Representations for Direct Generation of Strategies in High-Level Petri Games" in
Proc. Application and Theory of Petri Nets and Concurrency - 42nd International Conference, PETRI NETS 2021, Virtual Event, June 23-25, 2021, Proceedings, 2021.
doi:
10.1007/978-3-030-76983-3_6@inproceedings{DBLP:conf/apn/GiesekingW21,
author = {Manuel Gieseking and Nick W{\"{u}}rdemann},
editor = {Didier Buchs and Josep Carmona},
title = {Canonical Representations for Direct Generation of Strategies in High-Level Petri Games},
booktitle = {Application and Theory of Petri Nets and Concurrency - 42nd International Conference, {PETRI} {NETS} 2021, Virtual Event, June 23-25, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12734},
pages = {95--117},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-76983-3\_6},
doi = {10.1007/978-3-030-76983-3\_6},
timestamp = {Wed, 16 Jun 2021 13:05:52 +0200},
biburl = {https://dblp.org/rec/conf/apn/GiesekingW21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
M. Gieseking, J. Hecking-Harbusch, und A. Yanich, "A Web Interface for Petri Nets with Transits and Petri Games" in
Proc. Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Part II, 2021.
doi:
10.1007/978-3-030-72013-1_22@inproceedings{DBLP:conf/tacas/GiesekingHY21,
author = {Manuel Gieseking and Jesko Hecking-Harbusch and Ann Yanich},
editor = {Jan Friso Groote and Kim Guldstrand Larsen},
title = {A Web Interface for Petri Nets with Transits and Petri Games},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, {TACAS} 2021, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {12652},
pages = {381--388},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-72013-1\_22},
doi = {10.1007/978-3-030-72013-1\_22},
timestamp = {Wed, 24 Mar 2021 17:22:09 +0100},
biburl = {https://dblp.org/rec/conf/tacas/GiesekingHY21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)" CoRR, vol. abs/2005.07130, 2020.
@article{DBLP:journals/corr/abs-2005-07130,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
title = {AdamMC: {A} Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)},
journal = {CoRR},
volume = {abs/2005.07130},
year = {2020},
url = {https://arxiv.org/abs/2005.07130},
archiveprefix = {arXiv},
eprint = {2005.07130},
timestamp = {Fri, 22 May 2020 16:21:28 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2005-07130.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "Model Checking Branching Properties on Petri Nets with Transits (Full Version)" CoRR, vol. abs/2007.07235, 2020.
@article{DBLP:journals/corr/abs-2007-07235,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
title = {Model Checking Branching Properties on Petri Nets with Transits (Full Version)},
journal = {CoRR},
volume = {abs/2007.07235},
year = {2020},
url = {https://arxiv.org/abs/2007.07235},
archiveprefix = {arXiv},
eprint = {2007.07235},
timestamp = {Tue, 21 Jul 2020 12:53:33 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2007-07235.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "Model Checking Branching Properties on Petri Nets with Transits" in
Proc. Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, 2020.
doi:
10.1007/978-3-030-59152-6_22@inproceedings{DBLP:conf/atva/FinkbeinerGHO20,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
title = {Model Checking Branching Properties on Petri Nets with Transits},
booktitle = {Automated Technology for Verification and Analysis - 18th International Symposium, {ATVA} 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings},
pages = {394--410},
year = {2020},
optcrossref = {DBLP:conf/atva/2020},
url = {https://doi.org/10.1007/978-3-030-59152-6\_22},
doi = {10.1007/978-3-030-59152-6\_22},
timestamp = {Tue, 13 Oct 2020 16:57:38 +0200},
biburl = {https://dblp.org/rec/conf/atva/FinkbeinerGHO20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL" in
Proc. Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, 2020.
doi:
10.1007/978-3-030-53291-8_5@inproceedings{DBLP:conf/cav/FinkbeinerGHO20,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
title = {AdamMC: {A} Model Checker for Petri Nets with Transits against Flow-LTL},
booktitle = {Computer Aided Verification - 32nd International Conference, {CAV} 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}},
pages = {64--76},
year = {2020},
optcrossref = {DBLP:conf/cav/2020-2},
url = {https://doi.org/10.1007/978-3-030-53291-8\_5},
doi = {10.1007/978-3-030-53291-8\_5},
timestamp = {Fri, 17 Jul 2020 12:05:42 +0200},
biburl = {https://dblp.org/rec/conf/cav/FinkbeinerGHO20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
M. Gieseking, E. Olderog, und N. Würdemann, "Solving high-level Petri games"
Acta Inf. vol. 57, iss. 3-5, 2020.
doi:
10.1007/s00236-020-00368-5@article{DBLP:journals/acta/GiesekingOW20,
author = {Manuel Gieseking and Ernst-R{\"{u}}diger Olderog and Nick W{\"{u}}rdemann},
title = {Solving high-level Petri games},
journal = {Acta Inf.},
volume = {57},
number = {3-5},
pages = {591--626},
year = {2020},
url = {https://doi.org/10.1007/s00236-020-00368-5},
doi = {10.1007/s00236-020-00368-5},
timestamp = {Fri, 22 May 2020 21:54:01 +0200},
biburl = {https://dblp.org/rec/journals/acta/GiesekingOW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
M. Gieseking und E. Olderog, "High-Level Representation of Benchmark Families for Petri Games" CoRR, vol. abs/1904.05621, 2019.
@article{DBLP:journals/corr/abs-1904-05621,
author = {Manuel Gieseking and Ernst-R{\"{u}}diger Olderog},
title = {High-Level Representation of Benchmark Families for Petri Games},
journal = {CoRR},
volume = {abs/1904.05621},
year = {2019},
url = {http://arxiv.org/abs/1904.05621},
archiveprefix = {arXiv},
eprint = {1904.05621},
timestamp = {Thu, 25 Apr 2019 13:55:01 +0200},
biburl = {https://dblp.org/rec/bib/journals/corr/abs-1904-05621},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "Model Checking Data Flows in Concurrent Network Updates (Full Version)" CoRR, vol. abs/1907.11061, 2019.
@article{DBLP:journals/corr/abs-1907-11061,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
title = {Model Checking Data Flows in Concurrent Network Updates (Full Version)},
journal = {CoRR},
volume = {abs/1907.11061},
year = {2019},
url = {http://arxiv.org/abs/1907.11061},
archiveprefix = {arXiv},
eprint = {1907.11061},
timestamp = {Thu, 01 Aug 2019 08:59:33 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1907-11061.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "Model Checking Data Flows in Concurrent Network Updates" in
Proc. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, 2019.
doi:
10.1007/978-3-030-31784-3_30@inproceedings{DBLP:conf/atva/FinkbeinerGHO19,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
title = {Model Checking Data Flows in Concurrent Network Updates},
booktitle = {Automated Technology for Verification and Analysis - 17th International Symposium, {ATVA} 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings},
pages = {515--533},
year = {2019},
optcrossref = {DBLP:conf/atva/2019},
url = {http://www.uni-oldenburg.de/fileadmin/user\_upload/f2inform-csd/FinGieHecOld19.pdf},
opturl = {https://doi.org/10.1007/978-3-030-31784-3\_30},
doi = {10.1007/978-3-030-31784-3\_30},
timestamp = {Tue, 22 Oct 2019 15:35:01 +0200},
biburl = {https://dblp.org/rec/bib/conf/atva/FinkbeinerGHO19},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
C. Bischopink und M. Schwammberger, "Verification of Fair Controllers for Urban Traffic Manoeuvres at Intersections" in
Proc. Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I, 2019.
doi:
10.1007/978-3-030-54994-7_18@inproceedings{DBLP:conf/fm/BischopinkS19,
author = {Christopher Bischopink and Maike Schwammberger},
editor = {Emil Sekerinski and Nelma Moreira and Jos{\'{e}} N. Oliveira and Daniel Ratiu and Riccardo Guidotti and Marie Farrell and Matt Luckcuck and Diego Marmsoler and Jos{\'{e}} Campos and Troy Astarte and Laure Gonnord and Antonio Cerone and Luis Couto and Brijesh Dongol and Martin Kutrib and Pedro Monteiro and David Delmas},
title = {Verification of Fair Controllers for Urban Traffic Manoeuvres at Intersections},
booktitle = {Formal Methods. {FM} 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {12232},
pages = {249--264},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-54994-7\_18},
doi = {10.1007/978-3-030-54994-7\_18},
timestamp = {Mon, 17 Aug 2020 17:09:20 +0200},
biburl = {https://dblp.org/rec/conf/fm/BischopinkS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
D. Rahmatov, O. Theel, und M. Gieseking, "Towards a Composition of Region-Adherent Systems" in Proc. The Fourteenth International Conference on Networking and Services, ICNS 2018, 20-24 May 2018, Nice, France, 2018.
@inproceedings{conf/icns/RahmatovTG18,
author = {Dilshod Rahmatov and Oliver Theel and Manuel Gieseking},
title = {Towards a Composition of Region-Adherent Systems},
booktitle = {The Fourteenth International Conference on Networking and Services, {ICNS} 2018, 20-24 May 2018, Nice, France},
pages = {21--26},
year = {2018}
}
M. Schwammberger, "Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL" in Proc. Proceedings 2nd International Workshop on Safe Control of Autonomous Vehicles, SCAV@CPSWeek 2018, Porto, Portugal, 10th April 2018., 2018.
@inproceedings{Schwammberger18a,
author = {Maike Schwammberger},
title = {Introducing Liveness into Multi-lane Spatial Logic lane change controllers using {UPPAAL}},
editor = {Mario Gleirscher and Stefan Kugele and Sven Linker},
booktitle = {Proceedings 2nd International Workshop on Safe Control of Autonomous Vehicles, SCAV@CPSWeek 2018, Porto, Portugal, 10th April 2018.},
series = {{EPTCS}},
volume = {269},
pages = {17--31},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.269.3}
}
E. -R. Olderog, "Space for Traffic Manoeuvres -- An Overview" in Proc. Symposium on Real-Time and Hybrid Systems, 2018.
@inproceedings{Olderog18,
author = {E.-R. Olderog},
title = {Space for Traffic Manoeuvres -- An Overview},
editor = {Cliff Jones and Ji Wang and Naijun Zhan},
booktitle = {Symposium on Real-Time and Hybrid Systems},
pages = {211--230},
series = {LNCS},
volume = {11180},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-030-01461-2_11}
}
M. Schwammberger, "An abstract model for proving safety of autonomous urban traffic"
Theor. Comput. Sci. vol. 744, 2018.
doi:
10.1016/j.tcs.2018.05.028@article{DBLP:journals/tcs/Schwammberger18,
author = {Maike Schwammberger},
title = {An abstract model for proving safety of autonomous urban traffic},
journal = {Theor. Comput. Sci.},
volume = {744},
pages = {143--169},
year = {2018},
url = {https://doi.org/10.1016/j.tcs.2018.05.028},
doi = {10.1016/j.tcs.2018.05.028},
timestamp = {Fri, 28 Sep 2018 17:00:52 +0200},
biburl = {https://dblp.org/rec/bib/journals/tcs/Schwammberger18},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
Provably Correct Systems, Hinchey, M. G., Bowen, J. P., und Olderog, E. -R. Eds., Springer-Verlag, 2017.
@book{HBO17, editor = {M. G. Hinchey and J. P. Bowen and E.-R. Olderog },
title = {Provably Correct Systems},
series = {NASA Monographs in System and Software Engineering},
publisher = {Springer-Verlag},
year = {2017},
note = {328 pp, ISBN 978-3-319-48627-7},
url = {https://link.springer.com/book/10.1007/978-3-319-48628-4}
}
B. Finkbeiner und E. -R. Olderog, "Petri Games: Synthesis of Distributed Systems with Causal Memory" Information and Computation, vol. 253, Part 2, 2017.
@article{FinkbeinerOlderog16, title = {Petri Games: Synthesis of Distributed Systems with Causal Memory},
author = {B. Finkbeiner and E.-R. Olderog},
journal = {Information and Computation},
volume = {253, Part 2 },
year = {2017},
pages = {181--203},
url = {https://www.uni-oldenburg.de/fileadmin/user_upload/f2inform-csd/pub/mainPG-IC.pdf},
abstract = {We present a new multiplayer game model for the interaction and the flow of information in a distributed system. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete.}
}
G. v. Bochmann, M. Hilscher, S. Linker, und E. -R. Olderog, "Synthesizing and Verifying Controllers for Multi-lane Traffic Maneuvers"
Formal Aspects of Computing, vol. 29, iss. 4, 2017.
doi:
10.1007/s00165-017-0424-4@article{BHLO17,
author = {G. v. Bochmann and M. Hilscher and S. Linker and E.-R. Olderog},
title = {Synthesizing and Verifying Controllers for Multi-lane Traffic Maneuvers},
journal = {Formal Aspects of Computing},
volume = {29},
number = {4},
year = {2017},
pages = {583--600},
doi = {10.1007/s00165-017-0424-4},
url = {https://www.uni-oldenburg.de/fileadmin/user_upload/informatik/ag/csd/pub/faoc-synthesis.pdf}
}
E. -R. Olderog, A.P.Ravn, und R. Wisniewski, Linking Discrete and Dynamic Models: Applied to Traffic ManoevresSpringer, 2017.
@incollection{ORW17,
author = {E.-R. Olderog and A.P.Ravn and R. Wisniewski},
title = {Linking Discrete and Dynamic Models: Applied to Traffic Manoevres},
editor = {M.G. Hinchey and J.P. Bowen and E.-R. Olderog},
booktitle = {Provably Correct Systems},
note = {NASA Monographs in Systems and Software Engineering},
publisher = {Springer},
year = {2017},
pages = {95-120},
url = {https://www.uni-oldenburg.de/fileadmin/user_upload/informatik/ag/csd/pub/main-ORW.pdf}
}
M. Schwammberger, "Imperfect Knowledge in Autonomous Urban Traffic Manoeuvres" in
Proc. Proceedings First Workshop on Formal Verification of Autonomous Vehicles, FVAV@iFM 2017, Turin, Italy, 19th September 2017., 2017.
doi:
10.4204/EPTCS.257.7@inproceedings{DBLP:journals/corr/abs-1709-02559,
author = {Maike Schwammberger},
title = {Imperfect Knowledge in Autonomous Urban Traffic Manoeuvres},
booktitle = {Proceedings First Workshop on Formal Verification of Autonomous Vehicles, FVAV@iFM 2017, Turin, Italy, 19th September 2017.},
pages = {59--74},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.257.7},
doi = {10.4204/EPTCS.257.7},
timestamp = {Mon, 16 Oct 2017 16:32:11 +0200},
biburl = {http://dblp.org/rec/bib/journals/corr/abs-1709-02559},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
E. -R. Olderog und M. Schwammberger, "Formalising a Hazard Warning Communication Protocol with Timed Automata" in Proc. Models, Algorithms, Logics and Tools, 2017.
@inproceedings{OlderogSchwammberger17,
author = {E.-R. Olderog and M. Schwammberger},
title = {Formalising a Hazard Warning Communication Protocol with Timed Automata},
editor = {Luca Aceto and Giorgio Bacci and Giovanni Bacci and Anna Ing{\'{o}}lfsd{\'{o}}ttir and Axel Legay and Radu Mardare},
booktitle = {Models, Algorithms, Logics and Tools},
pages = {640--660},
series = {LNCS},
volume = {10460},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-63121-9_32}
}
B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "Symbolic vs. Bounded Synthesis for Petri Games" in
Proc. Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017, 2017.
doi:
10.4204/EPTCS.260.5@inproceedings{DBLP:journals/corr/abs-1711-10637,
author = {Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-R\"udiger},
year = {2017},
title = {Symbolic vs. Bounded Synthesis for Petri Games},
editor = {Fisman, Dana and Jacobs, Swen},
booktitle = {Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017},
series = {Electronic Proceedings in Theoretical Computer Science {(EPTCS)}},
volume = {260},
publisher = {Open Publishing Association},
pages = {23--43},
doi = {10.4204/EPTCS.260.5},
url = {https://arxiv.org/abs/1711.10637}
}
H. Ody, "Monitoring of Traffic Manoeuvres with Imprecise Information" in
Proc. Proceedings First Workshop on Formal Verification of Autonomous Vehicles, Turin, Italy, 19th September 2017, 2017.
doi:
10.4204/EPTCS.257.6@inproceedings{Ody17,
author = {Ody, Heinrich},
year = {2017},
title = {Monitoring of Traffic Manoeuvres with Imprecise Information},
editor = {Bulwahn, Lukas and Kamali, Maryam and Linker, Sven},
booktitle = {{Proceedings First Workshop on} Formal Verification of Autonomous Vehicles, {Turin, Italy, 19th September 2017}},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {257},
publisher = {Open Publishing Association},
pages = {43-58},
doi = {10.4204/EPTCS.257.6},
url = {https://arxiv.org/abs/1709.02558v1}
}
B. Engelmann und E. Olderog, "A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs" in Proc. Proc. Theory and Practice of Formal Methods, 2016.
@inproceedings{EngelmannOlderog2015,
author = {Bj\"orn Engelmann and Ernst-R\"udiger Olderog},
title = {{A} {S}ound and {C}omplete {H}oare {L}ogic for {D}ynamically-{T}yped, {O}bject-{O}riented {P}rograms},
booktitle = {Proc. Theory and Practice of Formal Methods},
year = {2016},
editor = {Erika {\' A}brah{\' a}m and Marcello Bonsangue and Einar Broch Johnsen},
volume = {9660},
series = {LNCS},
publisher = {Springer},
pages = {173--193},
url = {http://link.springer.com/chapter/10.1007%2F978-3-319-30734-3_13},
optaddress = {Eindhoven, The Netherlands}
}
M. Hilscher und M. Schwammberger, "An Abstract Model for Proving Safety of Autonomous Urban Traffic" in
Proc. Theoretical Aspects of Computing (ICTAC), 2016.
doi:
10.1007/978-3-319-46750-4_16@inproceedings{HS16,
author = {Hilscher, Martin and Schwammberger, Maike},
editor = {Sampaio, Augusto and Wang, Farn},
title = {An Abstract Model for Proving Safety of Autonomous Urban Traffic},
booktitle = {Theoretical Aspects of Computing (ICTAC)},
optbooktitle = {Theoretical Aspects of Computing -- ICTAC 2016: 13th International Colloquium, Taipei, Taiwan, ROC, October 24--31, 2016, Proceedings},
year = {2016},
publisher = {Springer},
optaddress = {Cham},
volume = {9965},
series = {LNCS},
pages = {274--292},
isbn = {978-3-319-46750-4},
doi = {10.1007/978-3-319-46750-4_16}
}
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.
doi:
10.1007/978-3-319-48989-6_35@inproceedings{OFH16,
author = {Heinrich Ody and Martin Fr{\"{a}}nzle and Michael R. Hansen},
editor = {John S. Fitzgerald and Constance L. Heitmeyer and Stefania Gnesi and Anna Philippou},
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},
pages = {577--592},
year = {2016},
url = {http://theoretica.informatik.uni-oldenburg.de/~sefie/files/discounted-duration-calculus.pdf},
doi = {10.1007/978-3-319-48989-6_35},
timestamp = {Mon, 22 May 2017 17:11:19 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/fm/OdyFH16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
B. Engelmann, "Formally Verifying Dynamically-typed Programs like Statically-typed Ones -- Another perspective" in Proc. Proceedings of the Young Researchers Conference Frontiers of Formal Methods, 2015.
@inproceedings{Eng2015,
author = {Bj{\"o}rn Engelmann},
title = {Formally Verifying Dynamically-typed Programs like Statically-typed Ones -- Another perspective},
booktitle = {Proceedings of the Young Researchers Conference Frontiers of Formal Methods},
year = {2015},
url = {http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2015/2015-06.pdf}
}
M. Schwammberger, "Properties of Communicating Controllers for Safe Traffic Manoeuvres" in Proc. Proceedings of the Doctoral Symposium of Formal Methods 2015, 2015.
@inproceedings{MS15,
author = {Maike Schwammberger},
title = {Properties of Communicating Controllers for Safe Traffic Manoeuvres},
booktitle = {Proceedings of the Doctoral Symposium of Formal Methods 2015},
editor = {Aichernig, Bernhard K. and Rossini, Alessandro},
pages = {3--7},
year = 2015 }
E. -R. Olderog und M. Swaminathan, "Structural Transformations for Data-Enriched Real-Time Systems" Formal Asp. Comput. vol. 27, 2015.
@article{OlderogSwaminathan14,
author = {E.-R Olderog and M. Swaminathan},
title = {Structural Transformations for Data-Enriched Real-Time Systems},
journal = {Formal Asp. Comput.},
volume = {27},
pages = {727--750},
year = {2015},
url = {http://dx.doi.org/10.1007/s00165-014-0306-y}
}
B. Engelmann, E. -R. Olderog, und N. Flick, Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic, 2015.
@misc{EOF2015,
author = {Bj{\"o}rn Engelmann and E.-R Olderog and Nils-Erik Flick},
title = {Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic},
month = {January},
year = {2015},
howpublished = {arXiv:1501.02699v1 [cs.PL]},
abstract = {Dynamically typed object-oriented languages enable programmers to write elegant, reusable and extensible programs. However, with the current methodology for program verification, the absence of static type information creates significant overhead. Our proposal is two-fold: First, we propose a layer of abstraction hiding the complexity of dynamic typing when provided with sufficient type information. Since this essentially creates the illusion of verifying a statically-typed program, the effort required is equivalent to the statically-typed case. Second, we show how the required type information can be efficiently derived for all type-safe programs by integrating a type inference algorithm into Hoare logic, yielding a semi-automatic procedure allowing the user to focus on those typing problems really requiring his attention. While applying type inference to dynamically typed programs is a well-established method by now, our approach complements conventional soft typing systems by offering formal proof as a third option besides modifying the program (static typing) and accepting the presence of runtime type errors (dynamic typing).},
url = {http://arxiv.org/abs/1501.02699}
}
M. Fränzle, M. R. Hansen, und H. Ody, "Discounted Duration Calculus" School of Computer Science, Reykjavik University, RUTR-SCS16001, 2015.
@techreport{FHO15b, title = {Discounted Duration Calculus},
author = {Fr{\"a}nzle, Martin and Hansen, Michael R. and Ody, Heinrich},
year = {2015},
booktitle = {Nordic Workshop on Programming Theory - NWPT},
editor = {Luca Aceto, Ignacio Fabregas, Alvaro Garcia-Perez and Anna Ingolfsdottir},
institution = {School of Computer Science, Reykjavik University},
number = {RUTR-SCS16001},
url = {http://icetcs.ru.is/nwpt2015/NWPT15Proceedings.pdf}
}
S. Linker und M. Hilscher, "Proof Theory of a Multi-Lane Spatial Logic" Logical Methods in Computer Science, vol. 11, iss. 3, 2015.
@article{LH15,
author = {S. Linker and M. Hilscher},
editor = {Zhiming Liu and Jim Woodcock and Huibiao Zhu},
title = {Proof Theory of a Multi-Lane Spatial Logic},
journal = {Logical Methods in Computer Science},
volume = {11},
number = {3},
pages = {},
year = {2015},
url = {http://www.lmcs-online.org/ojs/regularIssues.php?id=46}
}
M. Gieseking, "Trace Refinement of $\pi$-Calculus Processes" in Proc. Frontiers of Formal Methods 2015, 2015.
@inproceedings{gie2015, booktitle = {Frontiers of Formal Methods 2015},
type = {Technical Report},
organization = {RWTH Aachen},
month = {February},
title = {Trace Refinement of $\pi$-Calculus Processes},
author = {Manuel Gieseking},
year = {2015},
series = {Proceedings of the Young Researchers' Conference "Frontiers of Formal Methods"},
pages = {109--114},
url = {http://www.uni-oldenburg.de/fileadmin/user\_upload/f2inform-csd/gieseking15\_ffm.pdf}
}
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, 2015.
doi:
10.1007/978-3-319-23506-6_11@inproceedings{FHO15a,
author = {Martin Fr{\"{a}}nzle and Michael R. Hansen and Heinrich Ody},
title = {No Need Knowing Numerous Neighbours - Towards a Realizable Interpretation of {MLSL}},
editor = {Roland Meyer and Andr{\'{e}} Platzer and Heike Wehrheim},
booktitle = {Correct System Design},
pages = {152--171},
year = {2015},
series = {Lecture Notes in Computer Science},
volume = {9360},
publisher = {Springer},
url = {http://theoretica.informatik.uni-oldenburg.de/~sefie/files/neighbours-csd15.pdf},
doi = {10.1007/978-3-319-23506-6_11},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/birthday/FranzleHO15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
E. -R. Olderog, A. P. Ravn, und R. Wisniewski, "Linking Spatial and Dynamic Models for Traffic Maneuvers" in
Proc. 54th IEEE Conf. on Decision and Control (CDC), Osaka, Japan, 2015.
doi:
10.1109/CDC.2015.7403292@inproceedings{ORW2015,
author = {E.-R. Olderog and A.P. Ravn and R. Wisniewski},
title = {Linking Spatial and Dynamic Models for Traffic Maneuvers},
booktitle = {54th IEEE Conf. on Decision and Control (CDC), Osaka, Japan },
year = {2015},
pages = {6809-6816},
month = {Dec},
publisher = {IEEE},
url = {https://www.uni-oldenburg.de/fileadmin/user_upload/f2inform-csd/pub/root-ORW15.pdf},
doi = {10.1109/CDC.2015.7403292},
subproject = {H3},
conference-short = {CDC},
conference-long = {IEEE Conference on Decision and Control},
abstract = {For traffic maneuvers of multiple vehicles on highways we build an abstract spatial and a concrete dynamic model. In the spatial model we show the safety (collision freedom) of lane-change maneuvers. By linking the spatial and dynamic model via suitable refinements of the spatial atoms to distance measures, the safety carries over to the concrete mode}
}
H. Ody, "Undecidability Results for Multi-Lane Spatial Logic" in
Proc. Theoretical Aspects of Computing - ICTAC, 2015.
doi:
10.1007/978-3-319-25150-9_24@inproceedings{Ody15b,
author = {Heinrich Ody},
title = {Undecidability Results for Multi-Lane Spatial Logic},
booktitle = {Theoretical Aspects of Computing - {ICTAC}},
pages = {404--421},
year = {2015},
editor = {Martin Leucker and Camilo Rueda and Frank D. Valencia},
volume = {9399},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
url = {http://theoretica.informatik.uni-oldenburg.de/~sefie/files/mlsl-undec-ictac15.pdf},
doi = {10.1007/978-3-319-25150-9_24},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/ictac/Ody15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
G. v. Bochmann, M. Hilscher, S. Linker, und E. Olderog, "Synthesizing Controllers for Multi-Lane Traffic Maneuvers" in Proc. International Symposium on Dependable Software Engineering (SETTA), 2015.
@inproceedings{avacs-h3-dec-15, title = {Synthesizing Controllers for Multi-Lane Traffic Maneuvers},
author = {Gregor v. Bochmann AND Martin Hilscher AND Sven Linker AND Ernst-Rüdiger Olderog},
editor = {Xuandong Li AND Zhiming Liu AND Wang Yi},
booktitle = {International Symposium on Dependable Software Engineering (SETTA)},
year = {2015},
month = {Nov.},
pages = {71-86},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 9409, abstract = {The dynamic behavior of a car can be modeled as a hybrid system involving continuous state changes and discrete state transitions. However, we show that the control of safe (collision free) lane change maneuvers in multi-lane traffic on highways can be described by finite state machines extended with continuousvariables coming from the environment. We use standard theory for controller synthesis to derive the dynamic behavior of a lane-change controller. Thereby, we contrast the setting of interleaving semantics and synchronous concurrent semantics. We also consider the possibility of exchanging knowledge between neighboring cars in order to come up with the right decisions.},
conference-long = {International Symposium on Dependable Software Engineering},
conference-short = {SETTA}
}
B. Finkbeiner, M. Gieseking, und E. Olderog, "Adam: Causality-Based Synthesis of Distributed Systems" in Proc. Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, 2015.
@inproceedings{fingieold15, title = {Adam: Causality-Based Synthesis of Distributed Systems},
author = {Bernd Finkbeiner and Manuel Gieseking and Ernst-R{\"{u}}diger Olderog},
booktitle = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {I}},
year = {2015},
editor = {Daniel Kroening and Corina S. Pasareanu},
pages = {433--439},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {9206},
abstract = {We present ADAM, a tool for the automatic synthesis of distributed systems with multiple concurrent processes. For each process, an individual controller is synthesized that acts on locally available information obtained through synchronization with the environment and with other system processes. ADAM is based on Petri games, an extension of Petri nets where each token is a player in a multiplayer game. ADAM implements the first symbolic game solving algorithm for Petri games. We report on experience from several case studies with up to 38 system processes.},
conference-long = {International Conference on Computer Aided Verification},
conference-short = {CAV},
url = {http://www.uni-oldenburg.de/fileadmin/user\_upload/f2inform-csd/fingieold15.pdf}
}
H. Ody, "Undecidability Results for Multi-Lane Spatial Logic" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 112, 2015.
@techreport{Ody15a, title = {Undecidability Results for Multi-Lane Spatial Logic},
author = {Heinrich Ody},
institution = {SFB/TR 14 AVACS},
year = {2015},
month = {September},
note = {http://www.avacs.org},
number = {112},
type = {Reports of SFB/TR 14 AVACS},
abstract = {We consider (un)decidability of Multi-Lane Spatial Logic (MLSL), a multi-dimensional modal logic introduced for reasoning about traffic manoeuvres. MLSL with length measurement has been shown to be undecidable. However, the proof relies on exact values. This raises the question whether the logic remains undecidable when we consider robust satisfiability, i.e. when values are known only approximately. Our main result is that robust satisfiability of MLSL is undecidable. Furthermore, we prove that even MLSL without length measurement is undecidable. In both cases we reduce the intersection emptiness of two context-free languages to the respective satisfiability problem. This is the full version of a paper with the same title published at the ICTAC 2015.},
access = {open},
bibtex = {atr112.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski},
pdf = {avacs_technical_report_112.pdf},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs\_technical\_report\_112.pdf},
series = {ATR},
subproject = {H3,R1}
}
N. Flick und B. Engelmann, "Properties of Petri Nets with Context-free Structure Changes" in Proc. Fifth International Workshop on Graph Computation Models, 2014.
@inproceedings{FE2014,
author = {Nils-Erik Flick and Bj{\"o}rn Engelmann},
title = {Properties of Petri Nets with Context-free Structure Changes},
booktitle = {Fifth International Workshop on Graph Computation Models},
year = {2014},
abstract = {Petri nets model systems with distributed state and syn- chronised state changes. Extending them with rewriting rules allows for evolving structure. In this paper, we investigate dynamic properties of simple structure-changing Petri nets. We show undecidability of checking a language-based notion of correctness even for very restricted classes of structure-changing nets. We also introduce a colour-based abstraction and use it to specify, and in special cases decide, reachability properties.},
url = {http://gcm2014.imag.fr/proceedingsGCM2014.pdf}
}
B. Finkbeiner und E. -R. Olderog, "Petri Games: Synthesis of Distributed Systems with Causal Memory" in Proc. Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, September 10-12, 2014., 2014.
@inproceedings{FinOld14,
author = {Bernd Finkbeiner and E.-R Olderog},
title = {Petri Games: Synthesis of Distributed Systems with Causal Memory},
editor = {Adriano Peron and Carla Piazza},
booktitle = {Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, September 10-12, 2014.},
series = {{EPTCS}},
year = {2014},
volume = {161},
pages = {217--230},
url = {http://arxiv.org/abs/1406.1069v2}
}
S. Linker und M. Hilscher, "Proof theory of a multi-lane spatial logic" in Proc. Theoretical Aspects of Computing--ICTAC 2013, 2013.
@inproceedings{LH13, title = {Proof theory of a multi-lane spatial logic},
author = {Linker, Sven and Hilscher, Martin},
booktitle = {Theoretical Aspects of Computing--ICTAC 2013},
pages = {231--248},
year = {2013},
publisher = {Springer}
}
B. Engelmann, "Towards Practical Verification of Dynamically Typed Programs" in Proc. 25th Nordic Workshop on Programming Theory, 2013.
@inproceedings{Eng2013,
author = {Bj{\"o}rn Engelmann},
title = {Towards Practical Verification of Dynamically Typed Programs},
booktitle = {25th Nordic Workshop on Programming Theory},
year = {2013},
abstract = {Dynamically typed languages enable programmers to write elegant, reusable and extendable programs. Recently, some progress has been made regarding their verification. However, the user is currently required to manually show the absence of type errors, a tedious task usually involving large amounts of repetitive work. As most dynamically typed programs only occasionally divert from what would also be possible in statically typed languages, properly designed type inference algorithms should be able to supply the missing type information in most cases. We propose integrating a certified type inference algorithm into an interactive verification environment in order to a) provide a layer of abstraction, allowing the users to verify their programs like in a statically typed language whenever possible and b) use verification results to improve type inference and thus allow type checking of difficult cases.},
pdf = {http://theoretica.informatik.uni-oldenburg.de/~ben/papers/nwpt2013-paper.pdf},
slides = {http://theoretica.informatik.uni-oldenburg.de/~ben/slides/nwpt2013/},
url = {http://theoretica.informatik.uni-oldenburg.de/~ben/papers/nwpt2013-paper.pdf}
}
M. Hilscher, S. Linker, und E. -R. Olderog, "Proving Safety of Traffic Manoeuvres on Country Roads" in Proc. Theories of Programming and Formal Methods, 2013.
@inproceedings{HLO13,
author = {M. Hilscher and S. Linker and E.-R. Olderog},
editor = {Zhiming Liu and Jim Woodcock and Huibiao Zhu},
title = {Proving Safety of Traffic Manoeuvres on Country Roads},
booktitle = {Theories of Programming and Formal Methods},
publisher = {Springer},
series = {LNCS},
volume = {8051},
year = {2013},
pages = {196--212}
}
S. Kemper und C. Etzien, "A Visual Logic for the Description of Highway Traffic Scenarios" in
Proc. Complex Systems Design & Management, Proceedings of the Fourth International Conference on Complex Systems Design & Management CSD&M 2013, Paris, France, December 4-6, 2013, 2013.
doi:
10.1007/978-3-319-02812-5_17@inproceedings{DBLP:conf/csdm/KemperE13,
author = {Stephanie Kemper and Christoph Etzien},
title = {A Visual Logic for the Description of Highway Traffic Scenarios},
booktitle = {Complex Systems Design {\&} Management, Proceedings of the Fourth International Conference on Complex Systems Design {\&} Management CSD{\&}M 2013, Paris, France, December 4-6, 2013},
pages = {233--245},
year = {2013},
url = {http://dx.doi.org/10.1007/978-3-319-02812-5_17},
doi = {10.1007/978-3-319-02812-5_17},
timestamp = {Sun, 08 Dec 2013 13:34:23 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/csdm/KemperE13},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
E. -R. Olderog und M. Swaminathan, "Structural Transformations for Data-Enriched Real-Time Systems" in Proc. Integrated Formal Methods (iFM), 2013.
@inproceedings{OlderogSwaminathan13,
author = {E.-R. Olderog and Mani Swaminathan},
title = {Structural Transformations for Data-Enriched Real-Time Systems},
editor = {Einar Broch Johnsen and Luigia Petre},
booktitle = {Integrated Formal Methods (iFM)},
volume = {7940},
series = {Lecture Notes in Computer Science},
pages = {378-393},
publisher = {Springer-Verlag},
year = {2013},
url = {http://dx.doi.org/10.1007/978-3-642-38613-8_26}
}
K. R. Apt, F. S. de Boer, E. -R. Olderog, und S. de Gouw, "Verification of object-oriented programs: A transformational approach" J Computer System Sciences, vol. 78, 2012.
@article{ABOG12,
author = {K. R. Apt and F. S. de Boer and E.-R. Olderog and S. de Gouw},
title = {Verification of object-oriented programs: A transformational approach},
journal = {J Computer System Sciences},
volume = {78},
number = {},
pages = {823--852},
year = {2012},
optnote = {DOI information: 10.1016/j.jcss.2011.08.002}
}
E. -R. Olderog und R. Wilhelm, "Turing und die Verifikation" Informatik-Spektrum, vol. 35, iss. 4, 2012.
@article{OW12,
author = {E.-R. Olderog and R. Wilhelm},
title = {Turing und die {Verifikation}},
journal = {Informatik-Spektrum},
volume = {35},
number = {4},
pages = {271--279},
year = {2012},
optnote = {Themenheft: Turing}
}
M. Swaminathan, J. -P. Katoen, und E. -R. Olderog, "Layered Reasoning for randomized distributed algorithms" Formal Asp. Comput. vol. 24, iss. 4-6, 2012.
@article{SwaminathanKatoenOlderog12,
author = {M. Swaminathan and J.-P. Katoen and E.-R. Olderog},
title = {Layered Reasoning for randomized distributed algorithms},
journal = {Formal Asp. Comput.},
volume = {24},
number = {4-6},
year = {2012},
pages = {477-496},
url = {http://dx.doi.org/10.1007/s00165-012-0231-x}
}
S. Linker, "Translating Structural Process Properties to Petri Net Markings" in Proc. Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12), 2012.
@inproceedings{Lin12,
author = {S. Linker},
title = {Translating Structural Process Properties to Petri Net Markings},
booktitle = {Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12)},
pages = {82--91},
publisher = {IEEE Computer Society Conference Publishing Services},
year = {2012},
month = {June},
abstract = {We introduce a spatio-temporal logic PSTL defined on Pi-Calculus processes. This logic is especially suited to formulate properties in relation to the structural semantics of the Pi-Calculus due to Meyer, a representation of processes as Petri nets. To allow for the use of well-researched verification techniques, we present a translation of a subset of PSTL to LTL on Petri nets. We further prove soundness of our translation.}
}
E. -R. Olderog, "Automatic Verification of Real-Time Systems with Rich Data -- An Overview" in Proc. Theory and Applications of Models of Computation (TAMC), 2012.
@inproceedings{Old12,
author = {E.-R. Olderog},
title = {Automatic Verification of Real-Time Systems with Rich Data -- An Overview},
booktitle = {Theory and Applications of Models of Computation (TAMC)},
editor = {Manindra Agrawal and S. Barry Cooper and Angsheng Li},
series = {LNCS},
volume = {7287},
pages = {84--93},
publisher = {Springer},
year = {2012}
}
T. Strazny und R. Meyer, "An Algorithmic Framework for Coverability in Well-Structured Systems" in Proc. Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12), 2012.
@inproceedings{straznymeyer:2012:framework,
author = {T. Strazny and R. Meyer},
title = {An Algorithmic Framework for Coverability in Well-Structured Systems},
booktitle = {Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12)},
year = {2012},
pages = {173--182},
month = {June},
publisher = {IEEE Computer Society Conference Publishing Services},
abstract = {We generalize the backward algorithm for coverability in WSTS's to an algorithmic framework. The idea is to consider the predecessor computation, the witness function, and the processing order as parameters. On the theoretical side, we prove that every instantiation of the functions (that satisfies some requirements) still yields a decision procedure for coverability. On the practical side, we show that known optimizations like partial order reduction and pruning can be formulated in our framework. We also give a novel acceleration based instantiation. For well-known classes of WSTS's (PN, PN+Transfer, LCS), we optimize the selection function inspired by $A^*$. We implemented our instantiations and comment on the data structures. Extensive experiments show that the new algorithms can compete with a state-of-the-art tool: MIST2.},
note = {Best Paper Award of ACSD}
}
S. Kemper, "SAT-based verification for timed component connectors"
Science of Computer Programming, vol. 77, iss. 7–8, 2012.
doi:
10.1016/j.scico.2011.02.003@article{Kemper2012779,
author = {S. Kemper},
title = {SAT-based verification for timed component connectors },
journal = {Science of Computer Programming },
year = {2012},
volume = {77},
pages = {779 - 798},
number = {7–8},
note = {(1) FOCLASA’09 (2) FSEN’09 },
abstract = {Component-based software construction relies on suitable models underlying components, and in particular the coordinators which orchestrate component behaviour. Verifying correctness and safety of such systems amounts to model checking the underlying system model. The model checking techniques not only need to be correct (since system sizes increase), but also scalable and efficient. In this paper, we present a SAT-based approach for bounded model checking of Timed Constraint Automata, which permits true concurrency in the timed orchestration of components. We present an embedding of bounded model checking into propositional logic with linear arithmetic. We define a product that is linear in the size of the system, and in this way overcome the state explosion problem to deal with larger systems. To further improve model checking performance, we show how to embed our approach into an extension of counterexample guided abstraction refinement with Craig interpolants. },
doi = {http://dx.doi.org/10.1016/j.scico.2011.02.003},
issn = {0167-6423},
keywords = {Timed constraint automata},
url = {http://www.sciencedirect.com/science/article/pii/S0167642311000499}
}
J. Quesel und A. Platzer, "Playing Hybrid Games with KeYmaera." SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 84, 2012.
@techreport{DBLP:conf/cade/QueselP12:TR,
author = {Jan-David Quesel and Andr{\'e} Platzer},
title = {Playing Hybrid Games with {KeYmaera}.},
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 = {H3},
year = {2012},
month = {April},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 84, note = {ISSN: 1860-9821, http://www.avacs.org.},
abstract = { We propose a new logic, called differential dynamic game logic (dDGL), for expressing properties of parametric hybrid games, and develop a theorem prover for it. We give an operational and a modal semantics of dDGL and prove their equivalence. To allow for deductive reasoning, we exploit the fact that dDGL is a conservative extension of differential dynamic logic(dL). We provide rules for extending the dL sequent proof calculus to handle the dDGL specifics. We have implemented dDGL in the theorem prover KeYmaera and consider a case study in which a robot plays a game against other agents in a factory automation scenario. },
access = {open},
bibtex = {atr084.bib},
pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_084.pdf}
}
J. Quesel und A. Platzer, "Playing Hybrid Games with KeYmaera." in
Proc. Automated Reasoning, Sixth International Joint Conference, IJCAR 2012, Manchester, UK, Proceedings, 2012.
doi:
10.1007/978-3-642-31365-3_34@inproceedings{DBLP:conf/cade/QueselP12,
author = {Jan-David Quesel and Andr{\'e} Platzer},
title = {Playing Hybrid Games with {KeYmaera}.},
booktitle = {Automated Reasoning, Sixth International Joint Conference, IJCAR 2012, Manchester, UK, Proceedings},
month = {June},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
publisher = {Springer},
volume = {7364},
series = {LNCS},
pages = {439--453},
doi = {10.1007/978-3-642-31365-3_34},
pdf = {http://csd.informatik.uni-oldenburg.de/~jdq/paper/cdgl-ijcar.pdf},
slides = {http://csd.informatik.uni-oldenburg.de/~jdq/slides/ijcar-2012-06-26.pdf},
note = {The original publication is available at \url{http://www.springerlink.com/content/l44k5x507h67737q}{www.springerlink.com}.},
keywords = {differential dynamic logic, hybrid games, sequent calculus, theorem proving, logics for hybrid systems, factory automation},
abstract = { We propose a new logic, called differential dynamic game logic (dDGL), for expressing properties of parametric hybrid games, and develop a theorem prover for it. We give an operational and a modal semantics of dDGL and prove their equivalence. To allow for deductive reasoning, we exploit the fact that dDGL is a conservative extension of differential dynamic logic(dL). We provide rules for extending the dL sequent proof calculus to handle the dDGL specifics. We have implemented dDGL in the theorem prover KeYmaera and consider a case study in which a robot plays a game against other agents in a factory automation scenario. }
}
J. Faber, S. Linker, E. Olderog, und J. Quesel, "Syspect - Modelling, Specifying, and Verifying Real-Time Systems with Rich Data" International Journal of Software and Informatics, vol. 5, iss. 1-2, 2011.
@article{FLO+2011,
author = {Johannes Faber and Sven Linker and Ernst-R{\"u}diger Olderog and Jan-David Quesel},
title = {Syspect - Modelling, Specifying, and Verifying Real-Time Systems with Rich Data},
journal = {International Journal of Software and Informatics},
year = {2011},
volume = {5},
number = {1-2},
part = {1},
pages = {117--137},
note = {ISSN 1673-7288.},
url = {http://www.ijsi.org/IJSI/ch/reader/create_pdf.aspx?file_no=i78&flag=1&journal_id=ijsi},
abstract = {We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous real-time constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSP-OZ-DC of CSP (Communicating Sequential Processes), OZ (Object-Z) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect. },
publists = {syspect}
}
T. Strazny, "Accelerating Backward Reachability Analysis" in Proc. Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11), 2011.
@inproceedings{strazny:2011:accelerating,
author = {Tim Strazny},
title = {Accelerating Backward Reachability Analysis},
booktitle = {Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11)},
year = {2011},
editor = {Paul Pettersson and Cristina Seceleanu},
pages = {2--4},
month = {October},
organization = {M\"{a}lardalen University Sweden},
note = {Technical report 254/2011},
abstract = {In the context of depth-first backward reachability analysis, we identify two general operations which allow for performance improvements, while covering well-known techniques such as partial order methods and pruning. We instantiate these operations with novel \emph{backward acceleration} techniques and employ methods of \emph{guided search} in this context. Further, we introduce \emph{support-based search trees},
a data structure to represent upward-closed sets (ucs's) which allows for efficient implementation of operations necessary for the analysis.},
comment = {M\"{a}lardalen Real-Time Research Centre, Box 883, 72123 V\"{a}ster\r{a}s, Sweden},
issn = {1404-3041}
}
B. Wirtz, T. Strazny, J. Rakow, und A. Rakow, "A Lane Change Assistance System: Cooperation and Hybrid Control" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 78, 2011.
@techreport{atr078,
author = {Boris Wirtz and Tim Strazny and Jan Rakow and Astrid Rakow},
title = {A Lane Change Assistance System: Cooperation and Hybrid Control},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {78},
month = {July},
note = {ISSN: 1860-9821, http://www.avacs.org},
abstract = { Automated Highway Systems (AHS's) are considered as a key technology that promises increased safety, reduced energy consumption and optimized traffic flow. Safe and dependable operation of AHS's is of paramount importance and requires the application of rigid formal methods at design time. In this report we present a model for a lane change assistance system which is meant to serve as a foundation for benchmarks boosting theoretic and algorithmic advances in formal verification of the challenging class of cyber-physical systems. The assistance system implements an autonomous lane change manoeuvre conducted in cooperation with other communicating agents. The model implements a layered design for traffic agents where aspects of communication and autonomous control are described as real-time and hybrid systems, respectively, which are intertwined by synchronous message passing. },
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski},
series = {ATR},
subproject = {H3}
}
J. -D. Quesel, M. Fränzle, und W. Damm, "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.
@inproceedings{AVACS-H3-BRG-11,
author = {J.-D. Quesel AND M. Fr\"{a}nzle AND W. Damm},
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},
year = {2011},
editor = {Stavros Tripakis and Uli Fahrenberg},
series = {LNCS},
volume = {6919},
pages = {160--176},
month = {Sep.},
publisher = {Springer},
note = {The original publication is available at \url{http://www.springerlink.com/content/e6r94n5820k08626}{www.springerlink.com}.},
subproject = {H3},
pdf = {http://csd.informatik.uni-oldenburg.de/~jdq/paper/bridging.pdf},
slides = {http://csd.informatik.uni-oldenburg.de/~jdq/slides/bridging-formats-2011-09-21.pdf},
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. 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.}
}
M. Hilscher, S. Linker, E. -R. Olderog, und A. P. Ravn, "An Abstract Model for Proving Safety of Multi-Lane Traffic Manoeuvres" in Proc. Int'l Conf. on Formal Engineering Methods (ICFEM), 2011.
@inproceedings{avacs-h3-dec-11,
author = {M. Hilscher AND S. Linker AND E.-R. Olderog AND A.P. Ravn},
title = {An Abstract Model for Proving Safety of Multi-Lane Traffic Manoeuvres},
booktitle = {Int'l Conf.\ on Formal Engineering Methods (ICFEM)},
year = {2011},
editor = {Shengchao Qin AND Zongyan Qiu},
volume = {6991},
series = {Lecture Notes in Computer Science},
pages = {404--419},
month = {Oct.},
publisher = {Springer-Verlag},
note = {The original publication is available at \url{http://www.springerlink.com/content/y4721k1525v23520}{www.springerlink.com}.},
subproject = {H3},
pdf = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hlor2011-icfem.pdf},
url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hlor2011-icfem.pdf},
abstract = { We present an approach to prove safety (collision freedom) of multi-lane motorway trac with lane-change manoeuvres. This is ultimately a hybrid veri cation problem due to the continuous dynamics of the cars. We abstract from the dynamics by introducing a new spatial interval logic based on the view of each car. To guarantee safety, we present two variants of a lane-change controller, one with perfect knowledge of the safety envelopes of neighbouring cars and one which takes only the size of the neighbouring cars into account. Based on these controllers we provide a local safety proof for unboundedly many cars by showing that at any moment the reserved space of each car is disjoint from the reserved space of any other car. }
}
S. Fröschle, P. Janvcar, S. Lasota, und Z. Sawa, "Non-interleaving bisimulation equivalences on Basic Parallel Processes" Inf. Comput. vol. 208, iss. 1, 2010.
@article{FrJaLaSa:InfComput10,
author = {Fr\"{o}schle, Sibylle and Jan\v{c}ar, Petr and Lasota, Slawomir and Sawa, Zden\v{e}k},
title = {Non-interleaving bisimulation equivalences on Basic Parallel Processes},
journal = {Inf. Comput.},
volume = {208},
number = {1},
year = {2010},
pages = {42--62},
publisher = {Academic Press, Inc.}
}
A. Platzer,
Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Heidelberg: Springer, 2010.
doi:
10.1007/978-3-642-14509-4@book{Platzer10,
author = {Andr{\'e} Platzer},
title = {Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics},
publisher = {Springer},
address = {Heidelberg},
year = {2010},
isbn = {978-3-642-14509-4},
doi = {10.1007/978-3-642-14509-4},
url = {http://symbolaris.com/lahs/}
}
H. Baumgartner, M. Gieseking, C. Concolato, und J. L. Feuvre, "Individual Supportive Audio Signal Processing" in Proc. 26th Tonmeistertagung -- VDT International Convention, Leipzig, Germany, 2010.
@inproceedings{bauGieConFeu10,
author = {Hannah Baumgartner and Manuel Gieseking and Cyril Concolato and Jean Le Feuvre},
title = {Individual Supportive Audio Signal Processing},
publisher = {Verband Deutscher Tonmeister e.V.},
booktitle = {26th Tonmeistertagung -- VDT International Convention},
month = {Nov.},
year = {2010},
pages = {282--284},
address = {Leipzig, Germany}
}
J. Hoenicke, E. -R. Olderog, und A. Podelski, "Fairness for Dynamic Control" in Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2010.
@inproceedings{HOP10,
author = {J. Hoenicke and E.-R. Olderog and A. Podelski},
title = {Fairness for Dynamic Control},
editor = {J. Esparza and R. Majumdar },
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS) },
series = {Lecture Notes in Computer Science},
volume = {6015},
publisher = {Springer-Verlag},
pages = {251--265},
year = {2010}
}
E. -R. Olderog und A. Podelski, "Explicit Fair Scheduling for Dynamic Control" in Proc. Concurrency, Compositionality, and Correctness, 2010.
@inproceedings{OlPo10,
author = {E.-R. Olderog and A. Podelski},
editor = {D. Dams and U. Hannemann and M. Steffen},
title = { Explicit Fair Scheduling for Dynamic Control },
booktitle = {Concurrency, Compositionality, and Correctness },
series = {Lecture Notes in Computer Science},
volume = {5930 },
publisher = {Springer-Verlag },
pages = {96--117 },
year = {2010}
}
J. Hoenicke, R. Meyer, und E. -R. Olderog, "Kleene, Rabin, and Scott Are Available" in Proc. CONCUR 2010 - Concurrency Theory (CONCUR), 2010.
@inproceedings{HMO10,
author = {J. Hoenicke and R. Meyer and E.-R. Olderog},
title = {Kleene, Rabin, and Scott Are Available},
editor = {Paul Gastin and Fran\c{c}ois Laroussinie},
booktitle = {CONCUR 2010 - Concurrency Theory (CONCUR)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6269},
pages = {462-477},
year = {2010},
url = {http://dx.doi.org/10.1007/978-3-642-15375-4_32}
}
E. -R. Olderog und M. Swaminathan, "Layered Composition for Timed Automata" in Proc. Formal Modeling and Analysis of Timed Systems (FORMATS), 2010.
@inproceedings{OS10,
author = {E.-R. Olderog and M. Swaminathan},
title = {Layered Composition for Timed Automata},
editor = {K. Chatterjee and T. A Henzinger},
booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS) },
series = {Lecture Notes in Computer Science},
volume = {6246},
publisher = {Springer-Verlag},
pages = {228-242},
year = {2010},
url = {http://dx.doi.org/10.1007/978-3-642-15297-9_18}
}
S. Kemper, "Compositional Construction of Real-Time Dataflow Networks" in
Proc. Coordination Models and Languages, 12th International Conference, COORDINATION 2010, Amsterdam, The Netherlands, June 7-9, 2010. Proceedings, 2010.
doi:
10.1007/978-3-642-13414-2_7@inproceedings{Kem10,
author = {Stephanie Kemper},
editor = {Dave Clarke and Gul A. Agha},
title = {Compositional Construction of Real-Time Dataflow Networks},
booktitle = {Coordination Models and Languages, 12th International Conference, COORDINATION 2010, Amsterdam, The Netherlands, June 7-9, 2010. Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6116},
year = {2010},
pages = {92-106},
doi = {10.1007/978-3-642-13414-2_7},
url = {http://csd.informatik.uni-oldenburg.de/~stephie/Kemper_COORDINATION10.pdf}
}
R. Meyer und T. Strazny, "Petruchio: From dynamic networks to nets" in Proc. Proceedings of the 22nd International Conference on Computer Aided Verification 2010, CAV 2010, 2010.
@inproceedings{MS2010, editor = {Tayssir Touili and Byron Cook and Paul Jackson},
volume = {6174},
year = {2010},
pages = {175--179},
isbn = {978-3-642-14294-9},
author = {R. Meyer and T. Strazny},
title = {Petruchio: From dynamic networks to nets},
booktitle = {Proceedings of the 22nd International Conference on Computer Aided Verification 2010, CAV 2010},
series = {LNCS},
publisher = {Springer-Verlag},
publists = {rmeyer},
abstract = {We introduce Petruchio, a tool for computing Petri net translations of dynamic networks. To cater for unbounded architectures beyond the capabilities of existing implementations, the principle fixed-point engine runs interleaved with coverability queries. We discuss algorithmic enhancements and provide experimental evidence that Petruchio copes with models of reasonable size.}
}
S. Linker, Diagrammatic Specification of Mobile Real-Time SystemsSpringer Berlin / Heidelberg, 2010.
@incollection{springerlink:10.1007/978-3-642-14600-8_40,
author = {Linker, Sven},
affiliation = {Carl von Ossietzky University of Oldenburg},
title = {Diagrammatic Specification of Mobile Real-Time Systems},
booktitle = {Diagrammatic Representation and Inference},
series = {Lecture Notes in Computer Science},
editor = {Goel, Ashok and Jamnik, Mateja and Narayanan, N.},
publisher = {Springer Berlin / Heidelberg},
isbn = {},
pages = {316-318},
volume = {6170},
url = {http://dx.doi.org/10.1007/978-3-642-14600-8_40},
note = {10.1007/978-3-642-14600-8_40},
year = {2010}
}
J. Faber, C. Ihlemann, S. Jacobs, und V. Sofronie-Stokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies" in
Proc. Integrated Formal Methods, 2010.
doi:
10.1007/978-3-642-16265-7_12@inproceedings{FIJ+2010,
author = {J. Faber and C. Ihlemann and S. Jacobs and V. Sofronie-Stokkermans},
title = {Automatic Verification of Parametric Specifications with Complex Topologies},
series = {Lecture Notes in Computer Science},
booktitle = {Integrated Formal Methods},
year = {2010},
editor = {D. M{\'e}ry and S. Merz},
volume = {6396},
pages = {152--167},
publisher = {Springer, Heidelberg},
abstract = {The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.},
pdf = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/IFM2010b.pdf},
note = {This publication is available at \url{http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/978-3-642-16265-7_12} {SpringerLink}},
doi = {http://dx.doi.org/10.1007/978-3-642-16265-7_12}
}
J. Faber, "Verification Architectures: Compositional Reasoning for Real-time Systems" in
Proc. Integrated Formal Methods, 2010.
doi:
10.1007/978-3-642-16265-7_11@inproceedings{Faber2010,
author = {J. Faber},
title = {{Verification Architectures}: Compositional Reasoning for Real-time Systems},
booktitle = {Integrated Formal Methods},
year = {2010},
editor = {D. M{\'e}ry and S. Merz},
volume = {6396},
series = {Lecture Notes in Computer Science},
pages = {136--151},
publisher = {Springer, Heidelberg},
doi = {10.1007/978-3-642-16265-7_11},
abstract = { We introduce a conceptual approach to decompose real-time systems, specified by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Verification Architecture, a safe behavioural protocol with unknowns and local real-time assumptions. We examine how different verification techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are specified in CSP, extended by data and unknown processes with local assumptions in a real-time logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined specifications, here illustrated by CSP-OZ-DC. Using an example, we show that this approach helps us verify specifications that are too complex for direct verification. },
pdf = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/IFM2010a.pdf},
note = {This publication is available at \url{http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/978-3-642-16265-7_11} {SpringerLink}}
}
J. Faber, C. Ihlemann, S. Jacobs, und V. Sofronie-Stokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 66, 2010.
@techreport{FIJS2010,
author = {Johannes Faber and Carsten Ihlemann and Swen Jacobs and Viorica Sofronie-Stokkermans},
title = {Automatic Verification of Parametric Specifications with Complex Topologies},
institution = {SFB/TR 14 AVACS},
year = {2010},
type = {Reports of SFB/TR 14 AVACS},
number = {66},
note = {ISSN: 1860-9821, \url{http://www.avacs.org}{http://www.avacs.org}.},
abstract = {The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.},
access = {open},
bibtex = {atr066.bib},
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 = {R1},
url = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/ATR066.pdf},
publists = {syspect}
}
J. Faber, "Verification Architectures: Compositional Reasoning for Real-time Systems" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 65, 2010.
@techreport{Faber2010a,
author = {J. Faber},
title = {Verification {A}rchitectures: Compositional Reasoning for Real-time Systems},
institution = {SFB/TR 14 AVACS},
year = {2010},
type = {Reports of SFB/TR 14 AVACS},
number = {65},
month = {August},
note = {ISSN: 1860-9821, \url{http://www.avacs.org}{http://www.avacs.org}.},
abstract = { We introduce a conceptual approach to decompose real-time systems, specified by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Verification Architecture, a safe behavioural protocol with unknowns and local real-time assumptions. We examine how different verification techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are specified in CSP, extended by data and unknown processes with local assumptions in a real-time logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined specifications, here illustrated by CSP-OZ-DC. Using an example, we show that this approach helps us verify specifications that are too complex for direct verification. },
access = {open},
bibtex = {atr065.bib},
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 = {R1},
url = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/ATR065.pdf}
}
S. B. Fröschle und D. Gorla, "Proceedings 16th International Workshop on Expressiveness in Concurrency" CoRR, vol. abs/0911.3189, 2009.
@article{FrGo:Express09,
author = {Sibylle B. Fr{\"o}schle and Daniele Gorla},
title = {Proceedings 16th International Workshop on Expressiveness in Concurrency},
journal = {CoRR},
volume = {abs/0911.3189},
year = {2009}
}
S. Fröschle und G. Steel, "Analysing PKCS\#11 Key Management APIs with Unbounded Fresh Data" , 2009.
@article{FrSt:ArspaWits09,
author = {Fr\"{o}schle, Sibylle and Steel, Graham},
title = {Analysing PKCS\#11 Key Management APIs with Unbounded Fresh Data},
book = {Foundations and Applications of Security Analysis: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS 2009, York, UK, March 28-29, 2009, Revised Selected Papers},
year = {2009},
pages = {92--106},
publisher = {Springer-Verlag}
}
W. Czerwi'nski, S. Fröschle, und S. Lasota, "Partially-Commutative Context-Free Processes" in Proc. CONCUR 2009: Proceedings of the 20th International Conference on Concurrency Theory, 2009.
@inproceedings{CzFrLa:Concur09,
author = {Czerwi\'{n}ski, Wojciech and Fr\"{o}schle, Sibylle and Lasota, S\lawomir},
title = {Partially-Commutative Context-Free Processes},
booktitle = {CONCUR 2009: Proceedings of the 20th International Conference on Concurrency Theory},
year = {2009},
pages = {259--273},
publisher = {Springer-Verlag}
}
S. Fröschle und S. Lasota, "Normed Processes, Unique Decomposition, and Complexity of Bisimulation Equivalences" Electron. Notes Theor. Comput. Sci. vol. 239, 2009.
@article{FrLa:Infinity06,
author = {Fr\"{o}schle, Sibylle and Lasota, S\lawomir},
title = {Normed Processes, Unique Decomposition, and Complexity of Bisimulation Equivalences},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {239},
year = {2009},
pages = {17--42},
publisher = {Elsevier Science Publishers B. V.}
}
K. R. Apt, F. S. de Boer, und E. -R. Olderog, Verification of Sequential and Concurrent Programs, 3rd Edition, Springer-Verlag, 2009.
@book{ABO09-Book3,
author = { K. R. Apt and F. S. de Boer and E.-R. Olderog },
title = {Verification of Sequential and Concurrent Programs, 3rd Edition},
series = {Texts in Computer Science},
publisher = {Springer-Verlag},
year = {2009},
note = {502 pp, ISBN 978-1-84882-744-8},
url = {http://www.springer.com/computer/theoretical+computer+science/book/978-1-84882-744-8}
}
S. Fröschle, "Adding Branching to the Strand Space Model" Electron. Notes Theor. Comput. Sci. vol. 242, iss. 1, 2009.
@article{Fr:Express08,
author = {Fr\"{o}schle, Sibylle},
title = {Adding Branching to the Strand Space Model},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {242},
number = {1},
year = {2009},
pages = {139--159},
publisher = {Elsevier Science Publishers B. V.}
}
E. -R. Olderog und R. Meyer, "Automata-theoretic verification based on counterexample specification" in Proc. Informatik als Dialog zwischen Theorie und Anwendung, 2009.
@inproceedings{ero-rm-09,
author = {E.-R. Olderog and R. Meyer},
title = {Automata-theoretic verification based on counterexample specification},
editor = {V. Diekert and K. Weicker and N. Weicker},
booktitle = {Informatik als Dialog zwischen Theorie und Anwendung},
year = {2009},
pages = {217--225},
publisher = {Vieweg-Teubner},
publists = {rmeyer}
}
S. Kemper, "SAT-based Verification for Timed Component Connectors"
Electr. Notes Theor. Comput. Sci. vol. 255, 2009.
doi:
10.1016/j.entcs.2009.10.027@article{Kem09,
author = {Stephanie Kemper},
title = {{SAT}-based {V}erification for {T}imed {C}omponent {C}onnectors},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {255},
year = {2009},
pages = {103-118},
url = {http://csd.informatik.uni-oldenburg.de/~stephie/Kemper_FOCLASA09.pdf},
doi = {10.1016/j.entcs.2009.10.027},
keywords = {Timed Constraint Automata, Abstraction Refinement, Model Checking, SAT, Component-Based Software Engineering}
}
M. Fränzle und M. Swaminathan, "Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata" in Proc. Formal Modeling and Analysis of Timed Systems (FORMATS), 2009.
@inproceedings{MS09,
author = {M. Fr{\"a}nzle and M. Swaminathan},
title = {Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata},
editor = {J. Ouaknine and F. Vaandrager},
booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS) },
series = {Lecture Notes in Computer Science},
volume = {5813},
publisher = {Springer-Verlag},
pages = {149-163},
year = {2009},
url = {http://dx.doi.org/10.1007/978-3-642-04368-0_13}
}
A. Schäfer und M. John, "Conceptional Modeling and Analysis of Spatio-Temporal Processes in Biomolecular Systems" in Proc. Sixth Asia-Pacific Conference on Conceptual Modelling (APCCM 2009), Wellington, New Zealand, January 2009, 2009.
@inproceedings{sj09,
author = {Sch\"afer, A. and John, M.},
title = {Conceptional Modeling and Analysis of Spatio-Temporal Processes in Biomolecular Systems},
booktitle = {Sixth Asia-Pacific Conference on Conceptual Modelling (APCCM 2009), Wellington, New Zealand, January 2009},
editor = {Markus Kirchberg and Sebastian Link},
series = {CRPIT},
volume = {96},
publisher = {Australian Computer Society},
year = {2009},
pages = {39--48},
publists = {schaefer}
}
R. Meyer, V. Khomenko, und T. Strazny, "A Practical Approach to Verification of Mobile Systems Using Net Unfoldings" Fundamenta Informaticae, vol. 94, iss. 3--4, 2009.
@article{MeyerKhomenkoStrazny2009Unfolding,
author = {R. Meyer and V. Khomenko and T. Strazny},
title = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
journal = {Fundamenta Informaticae},
publisher = {IOS Press},
note = {Special Issue on Petri Nets 2008, invited version of the ATPN 2008 paper},
volume = {94},
number = {3--4},
pages = {439--471},
year = {2009},
publists = {rmeyer},
keywords = {finite control processes, safe processes, $\pi$-Calculus, mobile systems, model checking, Petri net unfoldings},
abstract = { We propose a technique for verification of mobile systems. We translate \emph{finite control processes,} which are a well-known subset of \picalc, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of \emph{safe processes,} which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime. We also demonstrate the applicability of our method on a realistic model of an automated manufacturing system.}
}
J. Faber, "Verification Architectures for Real-time Systems" in Proc. Proceedings of Formal Methods 2009 Doctoral Symposium, 2009.
@inproceedings{Faber2009,
author = {J. Faber},
title = {Verification Architectures for Real-time Systems},
booktitle = {Proceedings of Formal Methods 2009 Doctoral Symposium},
year = {2009},
editor = {M. Mousavi and E. Sekerinski},
number = {09-15},
series = {CS-Report, Eindhoven University of Technology},
pages = {14--19},
pdf = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/FM09_DS.pdf},
url = {http://alexandria.tue.nl/repository/books/654108.pdf },
institution = {Eindhoven University of Technology},
type = {CS-Report}
}
A. Platzer, J. Quesel, und P. Rümmer, "Real World Verification" in
Proc. Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2 - 7, 2009, Proceedings, 2009.
doi:
10.1007/978-3-642-02959-2_35@inproceedings{DBLP:conf/cade/PlatzerQR09,
author = {Andr{\'e} Platzer and Jan-David Quesel and Philipp R{\"u}mmer},
title = {Real World Verification},
booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2 - 7, 2009, Proceedings},
editor = {Renate A. Schmidt},
publisher = {Springer},
volume = {5663},
pages = {485-501},
series = {LNCS},
year = {2009},
doi = {10.1007/978-3-642-02959-2_35},
pdf = {http://symbolaris.com/pub/rwv.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-642-02959-2_35}{(c) Springer-Verlag}},
abstract = {Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of real-world applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of real-closed fields: approaches based on quantifier elimination, Gr{\"o}bner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gr{\"o}bner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.}
}
A. Platzer und J. Quesel, "European Train Control System: A Case Study in Formal Verification" in
Proc. Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, December 9-12, 2009, Proceedings, Heidelberg, 2009.
doi:
10.1007/978-3-642-10373-5_13@inproceedings{conf/icfem/PlatzerQ09,
author = {Andr{\'e} Platzer and Jan-David Quesel},
title = {European Train Control System: A Case Study in Formal Verification},
booktitle = {Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, December 9-12, 2009, Proceedings},
editor = {Ana Cavalcanti and Karin Breitman},
publisher = {Springer},
address = {Heidelberg},
series = {LNCS},
volume = {5885},
pages = {246-265},
year = {2009},
doi = {10.1007/978-3-642-10373-5_13},
pdf = {http://symbolaris.com/pub/etcs.pdf},
slides = {http://csd.informatik.uni-oldenburg.de/~jdq/slides/ETCS-slides.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-642-10373-5_13}{(c) Springer-Verlag}},
abstract = {Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. Finally we verify that safety is preserved when a PI controller is used for speed supervision.}
}
A. Platzer, J. Quesel, und P. Rümmer, "Real World Verification" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 52, 2009.
@techreport{DBLP:conf/cade/PlatzerQR09:TR,
author = {Andr{\'e} Platzer and Jan-David Quesel and Philipp R{\"u}mmer},
title = {Real World Verification},
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 = {H3},
year = {2009},
month = {June},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 52, note = {ISSN: 1860-9821, http://www.avacs.org.},
access = {open},
abstract = {Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of real-world applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of real-closed fields: approaches based on quantifier elimination, Gr{\"o}bner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gr{\"o}bner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.},
bibtex = {atr052.bib},
pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_052.pdf}
}
A. Platzer und J. Quesel, "European Train Control System: A Case Study in Formal Verification" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 54, 2009.
@techreport{conf/icfem/PlatzerQ09:TR,
author = {Andr{\'e} Platzer and Jan-David Quesel},
title = {European Train Control System: A Case Study in Formal Verification},
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 = {H3},
year = {2009},
month = {Oct},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 54, note = {ISSN: 1860-9821, http://www.avacs.org.},
access = {open},
abstract = {Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. Finally we verify that safety is preserved when a PI controller is used for speed supervision.},
bibtex = {atr054.bib},
pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_054.pdf}
}
E. -R. Olderog und H. Dierks, Real-Time Systems --- Formal Specification and Automatic Verification -- Errata: see below, Cambridge University Press, 2008.
@book{OD08,
author = {E.-R. Olderog and H. Dierks},
title = {Real-Time Systems --- Formal Specification and Automatic Verification -- Errata: see below},
publisher = {Cambridge University Press},
year = 2008, note = {ISBN 978-0-521-88333-7. For more information see: \url{http://csd.informatik.uni-oldenburg.de/rt-book/}{http://csd.informatik.uni-oldenburg.de/rt-book/}},
url = {http://www.cambridge.org/de/academic/subjects/computer-science/distributed-networked-and-mobile-computing/real-time-systems-formal-specification-and-automatic-verification}
}
M. Möller, E. -R. Olderog, H. Rasch, und H. Wehrheim, "Integrating a Formal Method into a Software Engineering Process with UML and Java" Formal Apsects of Computing, vol. 20, 2008.
@article{MORW08,
author = {M. M{\"o}ller and E.-R. Olderog and H. Rasch and H. Wehrheim},
title = {Integrating a Formal Method into a Software Engineering Process with {UML} and {Java}},
journal = {Formal Apsects of Computing},
year = {2008},
volume = {20},
pages = {161--204},
abstract = {We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed {\em reactive systems}. To this end, we propose a specific UML {\em profile} for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for {\em verifying} properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating {\em contracts} for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by \CSPjassda{},
an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts.},
publists = {syspect}
}
A. Platzer, "Differential-Algebraic Dynamic Logic for Differential-Algebraic Programs"
Journal of Logic and Computation, 2008.
doi:
10.1093/logcom/exn070@article{DBLP:journals/logcom/Platzer08,
author = {Andr{\'e} Platzer},
title = {Differential-Algebraic Dynamic Logic for Differential-Algebraic Programs},
journal = {Journal of Logic and Computation},
year = {2008},
note = {Accepted for publication},
doi = {10.1093/logcom/exn070},
pdf = {http://symbolaris.com/pub/DAL.pdf},
keywords = {dynamic logic, differential constraints, sequent calculus, verification of hybrid systems, differential induction, theorem proving},
abstract = { We generalise dynamic logic to a logic for differential-algebraic programs, i.e., discrete programs augmented with first-order differential-algebraic formulas as continuous evolution constraints in addition to first-order discrete jump formulas. These programs characterise interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new \emph{differential induction} with which differential-algebraic programs can be verified by exploiting their differential constraints algebraically without having to solve them. We develop the theory of differential induction and differential refinement and analyse their deductive power. As a case study, we present parametric tangential roundabout maneuvers in air traffic control and prove collision avoidance in our calculus.}
}
M. Johns, B. Engelmann, und J. Posegga, "XSSDS: Server-Side Detection of Cross-Site Scripting Attacks" in
Proc. ACSAC, 2008.
doi:
10.1109/ACSAC.2008.36@inproceedings{JEP08,
author = {Martin Johns and Bj{\"o}rn Engelmann and Joachim Posegga},
title = {XSSDS: Server-Side Detection of Cross-Site Scripting Attacks},
booktitle = {ACSAC},
year = {2008},
pages = {335-344},
abstract = {Cross-site Scripting (XSS) has emerged to one of the most prevalent type of security vulnerabilities. While the reason for the vulnerability primarily lies on the serverside, the actual exploitation is within the victim's web browser on the client-side. Therefore, an operator of a web application has only very limited evidence of XSS issues. In this paper, we propose a passive detection system to identify successful XSS attacks. Based on a prototypical implementation, we examine our approach's accuracy and verify its detection capabilities. We compiled a data-set of 500.000 individual HTTP request/response-pairs from 95 popular web applications for this, in combination with both real word and manually crafted XSS-exploits; our detection approach results in a total of zero false negatives for all tests, while maintaining an excellent false positive rate for more than 80\% of the examined web applications.},
bibtex = {jep08.bib},
doi = {10.1109/ACSAC.2008.36},
pdf = {http://www.acsac.org/openconf2008/modules/request.php?module=oc_proceedings&action=view.php&a=Accept&id=104}
}
M. Swaminathan, M. Fränzle, und J-. P. Katoen, "The Surprising Robustness of (Closed) Timed Automata against Clock-Drift" in Proc. IFIP International Conference on Theoretical Computer Science (IFIP TCS), 2008.
@inproceedings{SFK08,
author = {M. Swaminathan and M. Fr{\"a}nzle and J-.P. Katoen},
title = {The Surprising Robustness of (Closed) Timed Automata against Clock-Drift},
editor = {Giorgio Ausiello and Juhani Karhum{\"a}ki},
booktitle = {IFIP International Conference on Theoretical Computer Science (IFIP TCS) },
series = {International Federation for Information Processing},
volume = {273},
publisher = {Springer},
pages = {537-553},
year = {2008},
url = {http://dx.doi.org/10.1007/978-0-387-09680-3_36}
}
V. Khomenko und R. Meyer, "Checking $\pi$-Calculus Structural Congruence is Graph Isomorphism Complete" School of Computing Science, Newcastle University, CS-TR: 1100, 2008.
@techreport{KhomenkoMeyer2008ComplexityStructCong,
author = {V. Khomenko and R. Meyer},
title = {Checking $\pi$-Calculus Structural Congruence is Graph Isomorphism Complete},
number = {CS-TR: 1100},
institution = {School of Computing Science, Newcastle University},
year = {2008},
note = {20 pages},
url = {http://www.cs.ncl.ac.uk/publications/trs/abstract/1100},
publists = {rmeyer},
keywords = {structural congruence, graph isomorphism, $\pi$-Calculus, computational complexity},
abstract = {We show that the problems of checking $\pi$-Calculus structural congruence ($\pi$SC) and graph isomorphism (GI) are Karp reducible to each other. The reduction from GI to $\pi$SC is given explicitly, and the reduction in the opposite direction proceeds by transforming $\pi$SC into an instance of the term equality problem (i.e., the problem of deciding equivalence of two terms in the presence of associative and/or commutative operations and commutative variable-binding quantifiers), which is known to be Karp reducible to GI. Our result is robust in the sense that it holds for several variants of structural congruence and some rather restrictive fragments of $\pi$-Calculus. Furthermore, we address the question of solving $\pi$SC in practice, and describe a number of optimisations exploiting specific features of $\pi$-Calculus terms, which allow one to significantly reduce the size of the resulting graphs that have to be checked for isomorphism.}
}
R. Meyer, V. Khomenko, und T. Strazny, "A Practical Approach to Verification of Mobile Systems Using Net Unfoldings" School of Computing Science, Newcastle University, CS-TR: 1064, 2008.
@techreport{MeyerKhomenkoStrazny2008UnfoldingTR,
author = {R. Meyer and V. Khomenko and T. Strazny},
title = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
institution = {School of Computing Science, Newcastle University},
month = {January},
year = {2008},
number = {CS-TR: 1064},
note = {29 pages},
publists = {rmeyer},
keywords = {finite control processes, safe processes, $\pi$-Calculus, mobile systems, model checking, Petri net unfoldings},
abstract = { In this paper we propose a technique for verification of mobile systems.We translate finite control processes, which are a well-known subset of $\pi$-Calculus, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe pro- cesses, which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime. }
}
R. Meyer, V. Khomenko, und T. Strazny, "A Practical Approach to Verification of Mobile Systems Using Net Unfoldings" in Proc. Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008, 2008.
@inproceedings{MeyerKhomenkoStrazny2008Unfolding,
author = {R. Meyer and V. Khomenko and T. Strazny},
title = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
booktitle = {Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008},
series = {LNCS},
volume = {5062},
publisher = {Springer-Verlag},
pages = {327--347},
year = {2008},
publists = {rmeyer},
keywords = {finite control processes, safe processes, $\pi$-Calculus, mobile systems, model checking, Petri net unfoldings},
abstract = { In this paper we propose a technique for verification of mobile systems.We translate finite control processes, which are a well-known subset of $\pi$-Calculus, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe pro- cesses, which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime.}
}
A. Platzer und E. M. Clarke, "Computing Differential Invariants of Hybrid Systems as Fixedpoints" School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, CMU-CS-08-103, 2008.
@techreport{DBLP:conf/cav/PlatzerC08:TR,
author = {Andr{\'e} Platzer and Edmund M. Clarke},
title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints},
number = {CMU-CS-08-103},
year = {2008},
month = {},
institution = {School of Computer Science, Carnegie Mellon University},
address = {Pittsburgh, PA},
annote = {Long version of~\cite{PlatzerC08}},
keywords = {verification of hybrid systems, differential invariants, verification logic, fixedpoint engine},
abstract = { We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations that have right-hand sides that are polynomials in the state variables. In order to verify non-trivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.},
pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2008/CMU-CS-08-103.pdf}
}
A. Platzer, "Differential Dynamic Logic for Hybrid Systems."
Journal of Automated Reasoning, vol. 41, iss. 2, 2008.
doi:
10.1007/s10817-008-9103-8@article{DBLP:journals/jar/Platzer08,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logic for Hybrid Systems.},
journal = {Journal of Automated Reasoning},
year = {2008},
volume = {41},
number = {2},
pages = {143-189},
doi = {10.1007/s10817-008-9103-8},
pdf = {http://symbolaris.com/pub/freedL.pdf},
note = {\url{http://dx.doi.org/10.1007/s10817-008-9103-8}{(c) Springer-Verlag}},
keywords = {dynamic logic, differential equations, sequent calculus, axiomatisation, automated theorem proving, verification of hybrid systems},
abstract = { Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics. }
}
A. Schäfer, "Beschreibung und Verifikation räumlicher und zeitlicher Eigenschaften mobiler Systeme"
it -- Information Technology, vol. 50, iss. 5, 2008.
doi:
DOI 10.1524/itit.2008.0503@article{schaefer2008,
author = {A. Sch\"afer},
title = {{Beschreibung und Verifikation r\"aumlicher und zeitlicher Eigenschaften mobiler Systeme}},
journal = {it -- Information Technology},
year = {2008},
volume = {50},
pages = {324-326},
number = {5},
doi = {DOI 10.1524/itit.2008.0503},
publists = {schaefer},
url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/itti0805_324a.pdf},
note = {\url{http://it-Information-Technology.de}{http://it-Information-Technology.de}},
abstract = { This paper provides an overview over a formal method for the analysis of mobile real-time systems. Control systems for cars and trains as well as mobile robots are examples of such systems. We develop a spatio-temporal logic that is used to model both the systems and safety requirements. We investigate the theoretical foundations like decidability and axiomatisability and develop a prototype tool for the automatic verification based on these results. The application of this logic is exemplified with an industrial case study.}
}
R. Meyer, "On Boundedness in Depth in the $\pi$-Calculus" in Proc. Proc. of the 5th IFIP International Conference on Theoretical Computer Science, IFIP TCS 2008, 2008.
@inproceedings{Meyer2008BoundedDepth,
author = {R. Meyer},
title = {On Boundedness in Depth in the $\pi$-Calculus},
booktitle = {Proc. of the 5th IFIP International Conference on Theoretical Computer Science, IFIP TCS 2008},
series = {IFIP},
volume = {273},
publisher = {Springer-Verlag},
year = {2008},
pages = {},
note = {To appear},
publists = {rmeyer},
keywords = {$\pi$-Calculus, structural congruence, well-structured transition systems, termination},
abstract = { We investigate the class $P_{\mathit{BD}}$ of $\pi$-Calculus processes that are bounded in the function depth. First, we show that boundedness in depth has an intuitive characterisation when we understand processes as graphs: a process is bounded in depth if and only if the length of the simple paths is bounded. The proof is based on a new normal form for the $\pi$-Calculus called anchored fragments. Using this concept, we then show that processes of bounded depth have well-structured transition systems (WSTS). As a consequence, the termination problem is decidable for this class of processes. The instantiation of the WSTS framework employs a new well-quasi-ordering for processes in $P_{\mathit{BD}}$.}
}
A. Platzer und J. Quesel, "Logical Verification and Systematic Parametric Analysis in Train Control." in
Proc. Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings, 2008.
doi:
10.1007/978-3-540-78929-1_55@inproceedings{DBLP:conf/hybrid/PlatzerQ08,
author = {Andr{\'e} Platzer and Jan-David Quesel},
title = {Logical Verification and Systematic Parametric Analysis in Train Control.},
year = {2008},
pages = {646-649},
doi = {10.1007/978-3-540-78929-1_55},
editor = {Magnus Egerstedt and Bud Mishra},
booktitle = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings},
publisher = {Springer},
series = {LNCS},
volume = {4981},
isbn = {},
keywords = {parametric verification, logic for hybrid systems, symbolic decomposition},
abstract = { We formally verify hybrid safety properties of cooperation protocols in a fully parametric version of the European Train Control System (ETCS). We present a formal model using hybrid programs and verify correctness using our logic-based decomposition procedure. This procedure supports free parameters and parameter discovery, which is required to determine correct design choices for free parameters of ETCS.},
url = {http://symbolaris.com/pub/ETCS-short.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-540-78929-1_55}{(c) Springer-Verlag}}
}
R. Meyer, J. Faber, J. Hoenicke, und A. Rybalchenko, "Model Checking Duration Calculus: A Practical Approach"
Formal Aspects of Computing, vol. 20, iss. 4--5, 2008.
doi:
10.1007/s00165-008-0082-7@article{Meyer2008,
author = {R. Meyer and J. Faber and J. Hoenicke and A. Rybalchenko},
title = {Model Checking Duration Calculus: A Practical Approach},
journal = {Formal Aspects of Computing},
year = {2008},
publisher = {Springer London},
volume = {20},
pages = {481--505},
number = {4--5},
month = jul, note = {{ISSN} 0934-5043 (Print) 1433-299X (Online)},
abstract = {Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into sub-properties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and real-time aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).},
doi = {10.1007/s00165-008-0082-7},
issn = {0934-5043},
keywords = {Model checking, Verification, Duration Calculus, Timed automata, Real-time systems, European Train Control System, Case study},
url = {http://www.springerlink.com/content/81g876074077601g/fulltext.pdf},
publists = {rmeyer,pea,syspect}
}
A. Platzer und E. M. Clarke, "Computing Differential Invariants of Hybrid Systems as Fixedpoints" in
Proc. Computer-Aided Verification, CAV 2008, Princeton, USA, Proceedings, 2008.
doi:
10.1007/978-3-540-70545-1_17@inproceedings{DBLP:conf/cav/PlatzerC08,
author = {Andr{\'e} Platzer and Edmund M. Clarke},
title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints},
year = {2008},
month = {},
editor = {Aarti Gupta and Sharad Malik},
booktitle = {Computer-Aided Verification, CAV 2008, Princeton, USA, Proceedings},
publisher = {Springer},
series = {LNCS},
pages = {176-189},
volume = {5123},
isbn = {},
doi = {10.1007/978-3-540-70545-1_17},
keywords = {verification of hybrid systems, differential invariants, verification logic, fixedpoint engine},
abstract = { We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.},
pdf = {http://symbolaris.com/pub/fpdi.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-540-70545-1_17}{(c) Springer-Verlag}}
}
E. -R. Olderog, "Automatic Verification of Combined Specifications" in Proc. Proc. of the 1st Internat. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2007), Macau, 2008.
@inproceedings{Old08,
author = {E.-R. Olderog},
title = {Automatic Verification of Combined Specifications},
booktitle = {Proc. of the 1st Internat. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2007), Macau},
year = {2008},
editor = {G. Pu and V. Stolz},
series = {ENTCS},
journal = {Electr. Notes Theor. Comput. Sci.},
issn = {1571-0661},
volume = {207},
number = {},
month = {April},
pages = {3--16},
ee = {http://dx.doi.org/10.1016/j.entcs.2008.03.082},
url = {},
keywords = {Real-time systems, complex data, CSP, Object-Z, Duration Calculus, model checking, abstraction refinement, UML profile, tool support},
abstract = { This paper gives an overview of results of the project ``Beyond Timed Automata'' carried out in the Collaborative Research Center AVACS (Automatic Verification and Analysis of Complex Systems) of the Universities of Oldenburg, Freiburg, and Saarbr\"ucken. We discuss how properties of high-level specifications of real-time systems combining the dimensions of process behaviour, data, and time can be automatically verified, exploiting recent advances in semantics, constraint-based model checking, and decision procedures for complex data. As specification language we consider CS-OZ-DC, which integrates concepts from Communicating Sequential Processes (CSP), Object-Z (OZ), and Duration Calculus (DC). Our approach to automatic verification of CSP-OZ-DC rests on a compositional semantics of this languages in terms of Phase-Event-Automata. These can be translated into Transition Constraint Systems which serve as an input language of an abstract refinement model checker called ARMC which can handle constraints covering both real-time and infinite data. This is demonstrated by a case study concerning emergency messages in the European Train Control System (ETCS). For CSP-OZ-DC we also discuss a UML profile and tool support. }
}
A. Platzer und J. Quesel, "KeYmaera: A Hybrid Theorem Prover for Hybrid Systems." in
Proc. Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, 2008.
doi:
10.1007/978-3-540-71070-7_15@inproceedings{DBLP:conf/cade/PlatzerQ08,
author = {Andr{\'e} Platzer and Jan-David Quesel},
title = {{KeYmaera}: A Hybrid Theorem Prover for Hybrid Systems.},
booktitle = {Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings},
year = {2008},
pages = {171-178},
editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
publisher = {Springer},
series = {LNCS},
volume = {5195},
doi = {10.1007/978-3-540-71070-7_15},
isbn = {10.1007/978-3-540-71070-7_15},
issn = {0302-9743},
keywords = {dynamic logic, automated theorem proving, decision procedures, computer algebra, verification of hybrid systems},
abstract = { KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.},
note = {\url{http://dx.doi.org/10.1007/978-3-540-71070-7_15}{(c) Springer-Verlag}},
url = {http://symbolaris.com/pub/KeYmaera.pdf},
slides = {http://csd.informatik.uni-oldenburg.de/~jdq/slides/keymaera-slides.pdf}
}
S. Fröschle, "The Insecurity Problem: tackling Unbounded Data" in Proc. IEEE Computer Security Foundations Symposium 2007, 2007.
@inproceedings{Froeschle:CSF07,
author = {Sibylle Fr{\"o}schle},
title = {The Insecurity Problem: tackling Unbounded Data},
booktitle = {IEEE Computer Security Foundations Symposium 2007},
year = {2007},
publisher = {IEEE Computer Society},
abstract = { In this paper we focus on tackling the insecurity problem of security protocols in the presence of an unbounded number of data such as nonces or session keys. First, we pinpoint four open problems in this category. The first two problems concern protocols with natural restrictions that any `realistic' protocol should satisfy while the second two concern protocols with disequality constraints. For protocols with disequality constraints we will prove: (1)~Insecurity is decidable in NEXPTIME when bounding the size of messages and not requiring data to be \emph{freshly} generated. (2)~Insecurity is NEXPTIME-complete when bounding the size of messages and the number of freshly generated data used in honest sessions. This shows that unbounded data can be tackled in settings which do not trivially reduce to the case of bounded data. The second result is in contrast with a recently published proof, which appears to prove the same problem undecidable. We will point out why this proof cannot be considered to be valid. },
publists = {froeschle}
}
R. Meyer, "A Petri Net Semantics for $\pi$-Calculus Verification" in Proc. Dagstuhl ''zehn plus eins'', 2007.
@inproceedings{Meyer2007Dagstuhl,
author = {R. Meyer},
title = {{A Petri Net Semantics for $\pi$-Calculus Verification}},
booktitle = {Dagstuhl ''zehn plus eins''},
pages = {76--77},
year = {2007},
publisher = {Verlagshaus Mainz GmbH Aachen},
publists = {rmeyer}
}
S. Fröschle und S. l, "Causality versus true-concurrency" Theoretical Computer Science, vol. 386, iss. 3, 2007.
@article{FrLa:TCS07,
author = {Sibylle Fr{\"o}schle and S{\l}awomir Lasota},
title = {Causality versus true-concurrency},
journal = {Theoretical Computer Science},
year = {2007},
volume = {386},
number = {3},
pages = {169--187},
publists = {froeschle}
}
B. Becker, A. Podelski, W. Damm, M. Fränzle, E. -R. Olderog, und R. Wilhelm, "SFB/TR 14 AVACS -- Automatic Verification and Analysis of Complex Systems" it -- Information Technology, vol. 49, iss. 2, 2007.
@article{AVACS07,
author = {B. Becker and A. Podelski and W. Damm and M. Fr{\"a}nzle and E.-R. Olderog and R. Wilhelm},
title = {{SFB/TR 14 AVACS -- Automatic Verification and Analysis of Complex Systems}},
journal = {it -- Information Technology},
publisher = {Oldenbourg},
year = {2007},
number = {2},
volume = {49},
pages = {118--126},
note = {See also \url{http://www.avacs.org}{http://www.avacs.org}}
}
A. Schäfer, "Axiomatisation and Decidability of Multi-Dimensional Duration Calculus" TIME'05 special issue of Information and Computation, vol. 205, iss. 1, 2007.
@article{schaefer07,
author = {A. Sch\"afer},
title = {Axiomatisation and Decidability of Multi-Dimensional Duration Calculus},
journal = {TIME'05 special issue of Information and Computation},
year = {2007},
volume = {205},
number = {1},
note = {DOI \url{http://dx.doi.org/10.1016/j.ic.2006.08.005}{10.1016/j.ic.2006.08.005} },
publists = {schaefer},
abstract = { The Shape Calculus is a spatio-temporal logic based on an $n$-dimensional Duration Calculus tailored for the specification and verification of mobile real-time systems. After showing non-axiomatisability, we give a complete embedding in $n$-dimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use. }
}
D. Basin, E. -R. Olderog, und P. E. Sevinç, "Specifying and analyzing security automata using CSP-OZ" in Proc. Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007), 2007.
@inproceedings{BSO07,
author = {D. Basin and E.-R. Olderog and P.E. Sevin\c{c}},
title = {Specifying and analyzing security automata using {CSP-OZ}},
booktitle = {Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007)},
pages = {70--81},
year = 2007, month = {March},
publisher = {ACM Press},
location = {Singapore},
abstract = { Security automata are a variant of B\"uchi automata used to specify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSP-OZ, a specification language combining Communicating Sequential Processes (CSP) and Object-Z (OZ), to specify security automata, formalize their combination with target systems, and analyze the security of the resulting system specifications. We provide theoretical results relating CSP-OZ specifications and security automata and show how refinement can be used to reason about specifications of security automata and their combination with target systems. Through a case study, we provide evidence for the practical usefulness of this approach. This includes the ability to specify concisely complex operations and complex control, support for structured specifications, refinement, and transformational design, as well as automated, tool-supported analysis. }
}
A. Schäfer, "PhD Abstract: Specification and Verification of Mobile Real-Time Systems" Bulletin of the EATCS, vol. 92, 2007.
@article{sch07b,
author = {A. Sch\"afer},
title = {{PhD Abstract: Specification and Verification of Mobile Real-Time Systems}},
editor = {V. Sassone},
year = {2007},
pages = {193-195},
publisher = {EATCS},
journal = {Bulletin of the EATCS},
volume = {92},
publists = {schaefer},
url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/as07b.pdf}
}
A. Schäfer, "Spezifikation und Verifikation mobiler Realzeitsysteme" in Proc. Ausgezeichnete Informatikdissertationen 2007, 2007.
@inproceedings{sch07a,
author = {A. Sch\"afer},
title = {{Spezifikation und Verifikation mobiler Realzeitsysteme}},
booktitle = {{Ausgezeichnete Informatikdissertationen 2007}},
editor = {D. Wagner},
year = {2007},
pages = {169-177},
series = {GI-Edition-Lecture Notes in Informatics (LNI)},
publisher = {Gesellschaft f\"ur Informatik},
publists = {schaefer},
url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/as07a.pdf}
}
A. Platzer, "A Temporal Dynamic Logic for Verifying Hybrid System Invariants." , Reports of SFB/TR 14 AVACS 12, 2007.
@techreport{DBLP:conf/lfcs/Platzer07:TR,
author = {Andr{\'e} Platzer},
title = {A Temporal Dynamic Logic for Verifying Hybrid System Invariants.},
number = {12},
year = {2007},
month = {February},
editor = {B. Becker and W. Damm and M. Fr{\"a}nzle and E.-R. Olderog and A. Podelski and R. Wilhelm},
optinstitution = {{SFB/TR~14 AVACS}},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
note = {ISSN: 1860-9821, http://www.avacs.org.},
url = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_012.pdf},
annote = {Long version of~\cite{DBLP:conf/lfcs/Platzer07}}
}
J. Faber, S. Jacobs, und V. Sofronie-Stokkermans, "Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters" in Proc. Integrated Formal Methods, 2007.
@inproceedings{FJSS07,
author = {J. Faber and S. Jacobs and V. Sofronie-Stokkermans},
title = {Verifying {CSP-OZ-DC} Specifications with Complex Data Types and Timing Parameters},
booktitle = {Integrated Formal Methods},
year = {2007},
editor = {J. Davies and J. Gibbons},
volume = {4591},
series = {Lecture Notes in Computer Science},
pages = {233--252},
publisher = {Springer-Verlag},
month = jul, publists = {pea},
abstract = {We extend existing verification methods for CSP-OZ-DC to reason about real-time systems with complex data types and timing parameters. We show that important properties of systems can be encoded in well-behaved logical theories in which hierarchical reasoning is possible. Thus, testing invariants and bounded model checking can be reduced to checking satisfiability of ground formulae over a simple base theory. We illustrate the ideas by means of a simplified version of a case study from the European Train Control System standard.},
url = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/FaberJacobsSofronie.pdf}
}
J. Faber und I. Stierand, "From High-Level Verification to Real-Time Scheduling: A Property-Preserving Integration" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 19, 2007.
@techreport{atr19,
author = {J. Faber and I. Stierand},
title = {From High-Level Verification to Real-Time Scheduling: A Property-Preserving Integration},
editor = {B. Becker and W. Damm and M. Fr{\"a}nzle and E.-R. Olderog and A. Podelski and R. Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {R1,R2},
year = {2007},
month = {June},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 19, note = {{ISSN} 1860-9821, \url{http://www.avacs.org}{http://www.avacs.org}.},
abstract = { In the design process of real-time systems, formal verification establishes global properties of high-level specifications while real-time scheduling analysis ensures that concrete realisations meet essential timing properties with respect to a given target platform. But a formal link between these phases is missing. It is unclear (1) whether timing assumptions that are required to verify properties of high-level specifications can actually be realised on a target platform and (2) whether verified properties remain valid for a schedulable task network. Our approach bridges this gap by guaranteeing that properties verified on specification level are preserved on the implementation level, and vice versa, schedulability results can be propagated back to the specification. To this end, we provide a property-preserving translation from a subclass of the high-level real-time language CSP-OZ-DC into Cyclic Timed Automata, a Timed Automata based task network formalism. We apply our method to a case study from the European Train Control System standard. },
url = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/FaberStierand2007.pdf}
}
A. Platzer und E. M. Clarke, "The Image Computation Problem in Hybrid Systems Model Checking." in
Proc. Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, 2007.
doi:
10.1007/978-3-540-71493-4_37@inproceedings{DBLP:conf/hybrid/PlatzerC07,
author = {Andr{\'e} Platzer and Edmund M. Clarke},
title = {The Image Computation Problem in Hybrid Systems Model Checking.},
year = {2007},
doi = {10.1007/978-3-540-71493-4_37},
editor = {A. Bemporad and A. Bicchi and G. Buttazzo},
booktitle = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings},
publisher = {Springer-Verlag},
series = {LNCS},
pages = {473--486},
volume = {4416},
keywords = {model checking, hybrid systems, image computation},
note = {\url{http://dx.doi.org/10.1007/978-3-540-71493-4_37}{(c) Springer-Verlag}},
url = {http://symbolaris.com/pub/happroximation.pdf},
abstract = { In this paper, we analyze limits of approximation techniques for (non-linear) continuous image computation in model checking hybrid systems. In particular, we show that even a single step of continuous image computation is not semidecidable numerically even for a very restricted class of functions. Moreover, we show that symbolic insight about derivative bounds provides sufficient additional information for approximation refinement model checking. Finally, we prove that purely numerical algorithms can perform continuous image computation with arbitrarily high probability. Using these results, we analyze the prerequisites for a safe operation of the roundabout maneuver in air traffic collision avoidance. }
}
A. Platzer, "A Temporal Dynamic Logic for Verifying Hybrid System Invariants." in
Proc. Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, 2007.
doi:
10.1007/978-3-540-72734-7_32@inproceedings{DBLP:conf/lfcs/Platzer07,
author = {Andr{\'e} Platzer},
title = {A Temporal Dynamic Logic for Verifying Hybrid System Invariants.},
editor = {S. Artemov and A. Nerode},
doi = {10.1007/978-3-540-72734-7_32},
booktitle = {Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings},
publisher = {Springer},
series = {LNCS},
year = {2007},
pages = {457--471},
volume = {4514},
note = {\url{http://dx.doi.org/10.1007/978-3-540-72734-7_32}{(c) Springer-Verlag}},
url = {http://symbolaris.com/pub/dTL.pdf},
keywords = {dynamic logic, sequent calculus, logic for hybrid systems, temporal logic, deductive verification of embedded systems},
abstract = { We combine first-order dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with first-order definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to non-temporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints. }
}
A. Platzer, "Combining Deduction and Algebraic Constraints for Hybrid System Analysis." in Proc. 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, 2007.
@inproceedings{DBLP:conf/verify/Platzer07,
author = {Andr{\'e} Platzer},
title = {Combining Deduction and Algebraic Constraints for Hybrid System Analysis.},
booktitle = {4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany},
year = {2007},
pages = {164-178},
editor = {Bernhard Beckert},
volume = {259},
publisher = {CEUR-WS.org},
series = {},
note = {\url{http://ceur-ws.org/Vol-259}{CEUR Workshop Proceedings}},
issn = {1613-0073},
keywords = {modular prover combination, analytic tableaux, verification of hybrid systems, dynamic logic},
abstract = { We show how theorem proving and methods for handling real algebraic constraints can be combined for hybrid system verification. In particular, we highlight the interaction of deductive and algebraic reasoning that is used for handling the joint discrete and continuous behaviour of hybrid systems. We illustrate proof tasks that occur when verifying scenarios with cooperative traffic agents. From the experience with these examples, we analyse proof strategies for dealing with the practical challenges for integrated algebraic and deductive verification of hybrid systems, and we propose an iterative background closure strategy.},
url = {http://symbolaris.com/pub/cdachsa.pdf}
}
S. Kemper und A. Platzer, "SAT-based Abstraction Refinement for Real-time Systems" in
Proc. Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, 2007.
doi:
10.1016/j.entcs.2006.09.034@inproceedings{DBLP:journals/entcs/KemperP07,
author = {Stephanie Kemper and Andr{\'e} Platzer},
title = {SAT-based Abstraction Refinement for Real-time Systems},
booktitle = {Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings},
year = {2007},
editor = {Frank S. de Boer and Vladimir Mencl},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {182},
series = {ENTCS},
issn = {1571-0661},
pages = {107-122},
doi = {10.1016/j.entcs.2006.09.034},
url = {http://symbolaris.com/pub/SAAtRe.pdf},
keywords = {abstraction refinement, model checking, real-time systems, SAT, Craig interpolation},
abstract = { In this paper, we present an abstraction refinement approach for model checking safety properties of real-time systems using SAT-solving. With a faithful embedding of bounded model checking for systems of timed automata into propositional logic and linear arithmetic, we achieve both, quick abstraction techniques and a linear-size representation of parallel composition. In this logical setting, we introduce an abstraction that works uniformly for clocks, events, and states. When necessary, abstractions are refined by analysing spurious counterexamples using a promising extension of counterexample-guided abstraction refinement with syntactic information about Craig interpolants. To support generalisations, our overall approach identifies the algebraic and logical principles required for logic-based abstraction refinement. }
}
W. Damm, A. Mikschl, J. Oehlerking, E. Olderog, J. Pang, A. Platzer, M. Segelken, und B. Wirtz, "Automating Verification of Cooperation, Control, and Design in Traffic Applications." in
Proc. Formal Methods and Hybrid Real-Time Systems, 2007.
doi:
10.1007/978-3-540-75221-9_6@inproceedings{DammMOOPPSW07,
author = {Werner Damm and Alfred Mikschl and Jens Oehlerking and Ernst-R{\"u}diger Olderog and Jun Pang and Andr{\'e} Platzer and Marc Segelken and Boris Wirtz},
title = {Automating Verification of Cooperation, Control, and Design in Traffic Applications.},
year = {2007},
pages = {115--169},
editor = {Cliff Jones and Zhiming Liu and Jim Woodcock},
booktitle = {Formal Methods and Hybrid Real-Time Systems},
publisher = {Springer-Verlag},
series = {LNCS},
volume = {4700},
doi = {10.1007/978-3-540-75221-9_6},
issn = {},
keywords = {},
abstract = { We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.},
note = {\url{http://dx.doi.org/10.1007/978-3-540-75221-9_6}{(c) Springer-Verlag}}
}
I. Brückner, K. Dräger, B. Finkbeiner, und H. Wehrheim, "Slicing Abstractions" in Proc. FSEN 2007: IPM International Symposium on Fundamentals of Software Engineering, 2007.
@inproceedings{BDFW07,
author = {I. Br\"uckner and K. Dr\"ager and B. Finkbeiner and H. Wehrheim},
title = {{Slicing Abstractions}},
booktitle = {FSEN 2007: IPM International Symposium on Fundamentals of Software Engineering},
series = {Lecture Notes in Computer Science},
volume = {4767},
publisher = {Springer},
issn = {},
isbn = {978-3-540-75697-2},
editor = {F. Arbab and M. Sirjani},
pages = {17--32},
month = {April},
year = {2007},
abstract = { Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for infinite-state concurrent systems that interleaves automatic abstraction refinement, which splits states according to new predicates obtained by Craig interpolation, with slicing, which removes irrelevant states and transitions from the abstraction. The effects of abstraction and slicing complement each other. As the refinement progresses, the increasing accuracy of the abstract model allows for a more precise slice; the resulting smaller representation gives room for additional predicates in the abstraction. The procedure terminates when an error path in the abstraction can be concretized, which proves that the system is erroneous, or when the slice becomes empty, which proves that the system is correct. },
publists = {brueckner,wehrheim},
url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib07fsen.pdf}
}
A. Platzer, "Differential Logic for Reasoning about Hybrid Systems." in
Proc. Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, 2007.
doi:
10.1007/978-3-540-71493-4_75@inproceedings{DBLP:conf/hybrid/Platzer07,
author = {Andr{\'e} Platzer},
title = {Differential Logic for Reasoning about Hybrid Systems.},
year = {2007},
optee = {},
editor = {A. Bemporad and A. Bicchi and G. Buttazzo},
booktitle = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings},
publisher = {Springer-Verlag},
series = {LNCS},
pages = {746--749},
doi = {10.1007/978-3-540-71493-4_75},
volume = {4416},
note = {\url{http://dx.doi.org/10.1007/978-3-540-71493-4_75}{(c) Springer-Verlag}},
url = {http://symbolaris.com/pub/dL-short.pdf},
keywords = {dynamic logic, hybrid systems, parametric verification},
abstract = { We propose a first-order dynamic logic for reasoning about hybrid systems. As a uniform model for discrete and continuous evolutions in hybrid systems, we introduce hybrid programs with differential actions. Our logic can be used to specify and verify correctness statements about hybrid programs, which are suitable for symbolic processing by calculus rules. Using first-order variables, our logic supports systems with symbolic parameters. With dynamic modalities, it is prepared to handle multiple system components. }
}
A. Platzer, "Differential Dynamic Logic for Verifying Parametric Hybrid Systems." in
Proc. Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, 2007.
doi:
10.1007/978-3-540-73099-6_17@inproceedings{DBLP:conf/tableaux/Platzer07,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logic for Verifying Parametric Hybrid Systems.},
pages = {216-232},
doi = {10.1007/978-3-540-73099-6_17},
keywords = {dynamic logic, sequent calculus, verification of parametric hybrid systems, quantifier elimination},
abstract = { We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and first-order definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system.},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings},
year = {2007},
editor = {Nicola Olivetti},
volume = {4548},
series = {LNCS},
publisher = {Springer-Verlag},
isbn = {},
note = {\url{http://dx.doi.org/10.1007/978-3-540-73099-6_17}{(c) Springer-Verlag}},
url = {http://symbolaris.com/pub/dL.pdf}
}
I. Brückner, "Slicing Concurrent Real-Time System Specifications for Verification" in Proc. Integrated Formal Methods, 2007.
@inproceedings{ib07ifm,
author = {I. Br{\"u}ckner},
title = {{Slicing Concurrent Real-Time System Specifications for Verification}},
booktitle = {Integrated Formal Methods},
series = {Lecture Notes in Computer Science},
volume = {4591},
publisher = {Springer-Verlag},
issn = {0302-9743},
isbn = {978-3-540-73209-9},
editor = {J. Davies and J. Gibbons},
pages = {54--74},
month = jul, year = {2007},
abstract = { The high-level specification language CSP-OZ-DC has been shown to be well-suited for modelling and analysing industrially relevant concurrent real-time systems. It allows to model each of the most important functional aspects such as control flow, data, and real-time requirements in adequate notations, maintaining a common semantical foundation for subsequent verification. Slicing on the other hand has become an established technique to complement the fight against state space explosion during verification which inherently accompanies increasing system complexity. In this paper, we exploit the special structure of CSP-OZ-DC specifications by extending the dependence graph---which usually serves as a basis for slicing---with several new types of dependencies, including timing dependencies derived from the specification's DC part. Based on this we show how to compute a specification slice and prove correctness of our approach. },
publists = {brueckner},
url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib07ifm.pdf}
}
A. Platzer, "Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems" in
Proc. Proc., LICS International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, 2007.
doi:
10.1016/j.entcs.2006.11.026@inproceedings{DBLP:journals/entcs/Platzer07,
author = {Andr{\'e} Platzer},
title = {Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems},
booktitle = {Proc., LICS International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA},
year = {2007},
editor = {Patrick Blackburn and Thomas Bolander and Torben Bra\"{u}ner and Valeria de Paiva and J{\o}rgen Villadsen},
series = {ENTCS},
journal = {Electr. Notes Theor. Comput. Sci.},
issn = {1571-0661},
volume = {174},
number = {6},
month = {Jun},
pages = {63-77},
doi = {10.1016/j.entcs.2006.11.026},
url = {http://symbolaris.com/pub/hdL.pdf},
keywords = {hybrid logic, dynamic logic, sequent calculus, compositional verification, real-time hybrid dynamic systems},
abstract = { We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces state-based reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic advances the capabilities for compositional reasoning about (semialgebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goal-oriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus. }
}
E. -R. Olderog und B. Steffen, "Formale Semantik und Programmverifikation" in Proc. Informatik-Handbuch, 4. Auflage, 2006.
@inproceedings{erobs06,
author = {E.-R. Olderog and B. Steffen},
title = {{F}ormale {S}emantik und {P}rogrammverifikation},
booktitle = {Informatik-Handbuch, 4. Auflage},
editor = {P. Rechenberg and G. Pomberger},
year = 2006, publisher = {Hanser Verlag},
pages = {145--166}
}
R. Meyer, "Model Checking the $\pi$-Calculus" in Proc. Proceedings of the International Research Training Groups Workshop, 2006, p. 15.
@inproceedings{Meyer2006Dagstuhl,
author = {R. Meyer},
title = {Model Checking the $\pi$-Calculus},
booktitle = {Proceedings of the International Research Training Groups Workshop},
pages = {15},
year = {2006},
volume = {3},
series = {Trustworthy Software Systems},
publisher = {GITO},
publists = {rmeyer}
}
J. -D. Quesel und A. Schäfer, "Spatio-Temporal Model Checking for Mobile Real-Time Systems" in Proc. 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, 2006.
@inproceedings{QS06,
author = {J.-D. Quesel and A. Sch\"afer},
title = {Spatio-Temporal Model Checking for Mobile Real-Time Systems},
booktitle = {3rd International Colloquium on Theoretical Aspects of Computing, ICTAC},
year = {2006},
editor = {K. Barkaoui and A. Cavalcanti and A. Cerone},
series = {LNCS},
pages = {347--361},
publists = {schaefer,quesel},
abstract = { This paper presents an automatic verification method for combined temporal and spatial properties of mobile real-time systems. To this end, we provide a translation of the Shape Calculus (SC), a spatio-temporal extension of Duration Calculus, into weak second order logic of one successor (WS1S). A prototypical implementation facilitates successful verification of spatio-temporal properties by translating SC specifications into the syntax of the WS1S checker MONA. For demonstrating the formalism and tool usage, we apply it to the benchmark case study ``generalised railroad crossing'' (GRC) enriched by requirements inexpressible in non-spatial formalisms. }
}
W. Damm, H. Hungar, und E. -R. Olderog, "Verification of cooperating traffic agents" International Journal of Control, vol. 79, iss. 5, 2006.
@article{DHO06,
author = {W. Damm and H. Hungar and E.-R. Olderog},
title = {Verification of cooperating traffic agents},
journal = {International Journal of Control},
year = {2006},
optkey = {},
volume = {79},
number = {5},
month = {May},
pages = {395--421},
abstract = { This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented verification methodology is equally applicable for avionics applications (such as TCAS, the Traffic Alert and Collision Avoidance System), train applications (such as ETCS, the European Train Control System), or automotive applications (such as platooning). We present a verification rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind ``a collision will never occur'', and whose premises can either be established by off-line analysis of the worst-case behavior of the involved traffic agents, or by purely local proofs, involving only a single traffic agent. A companion paper will show how such local proof obligations can be discharged automatically. }
}
R. Meyer, Model Checking Using TestingGITO, 2006.
@incollection{Meyer2006,
author = {R. Meyer},
title = {Model Checking Using Testing},
booktitle = {Dependability Engineering},
pages = {147--171},
publisher = {GITO},
year = {2006},
editor = {W. Hasselbring and S. Giesecke},
volume = {2},
series = {Trustworthy Software Systems},
publists = {rmeyer}
}
J. Faber und R. Meyer, "Model Checking Data-Dependent Real-Time Properties of the European Train Control System" in Proc. Formal Methods in Computer Aided Design, 2006. FMCAD '06, 2006.
@inproceedings{FR06,
author = {J. Faber and R. Meyer},
title = {Model Checking Data-Dependent Real-Time Properties of the European Train Control System},
booktitle = {Formal Methods in Computer Aided Design, 2006. FMCAD '06},
year = {2006},
month = nov, pages = {76--77},
publisher = {IEEE Computer Society Press},
note = {This publication is available free of charge at \url{http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.21} {IEEE Digital Library}},
publists = {rmeyer},
abstract = { The behavior of embedded hardware and software systems is determined by at least three dimensions: control flow, data aspects, and real-time requirements. To specify the different dimensions of a system with the best-suited techniques, the formal language CSP-OZ-DC integrates Communicating Sequential Processes (CSP), Object-Z (OZ), and Duration Calculus (DC) into a declarative formalism equipped with a unified and compositional semantics. In this paper, we provide evidence that CSP-OZ-DC is a convenient language for modeling systems of industrial relevance. To this end, we examine the emergency message handling in the European Train Control System (ETCS) as a case study with uninterpreted constants and infinite data domains. We automatically verify that our model ensures real-time safety properties, which crucially depend on the system?s data handling. }
}
T. Strazny und C. Stehno, "Ein Simulator für mehrfach erweiterte höhere Petrinetze" in Proc. 19. Symposium Simulationstechnik (ASIM 2006), 2006.
@inproceedings{SS06,
author = {Tim Strazny and Christian Stehno},
title = {{E}in {S}imulator {f}\"{u}r {m}ehrfach {e}rweiterte {h}\"{o}here {P}etrinetze},
booktitle = {19. Symposium Simulationstechnik (ASIM 2006)},
editor = {Matthias Becker and Helena Szczerbicka},
year = {2006},
month = sep, pages = {171--176},
publisher = {SCS Publishing House e.V.},
publists = {strazny},
abstract = {Petrinetze mit ihrer eindeutigen Semantik und dem zugrunde liegenden mathematischen Modell bew\"{a}hren sich vermehrt bei Entwurf, Analyse und Steuerung komplexer, asynchroner und verteilter Systeme. Insbesondere zeitbehaftete stochastische gef\"{a}rbte Petrinetze bieten M\"{o}glichkeiten komplizierte Sachverhalte strukturiert und kompakt auszudr\"{u}cken, jedoch ist die Simulation solcher h\"{o}heren Petrinetze um ein Vielfaches aufw\"{a}ndiger. Mit Geschwindigkeit und Vielf\"{a}ltigkeit als Hauptziel wurde mit P-UMLaut/Sim ein Simulator f\"{u}r solche mehrfach erweiterten Petrinetze entwickelt.}
}
I. Brückner, B. Metzler, und H. Wehrheim, "Optimizing Slicing of Formal Specifications by Deductive Verification" Nordic Journal of Computing, vol. 13, iss. 1--2, 2006.
@article{BMW06,
author = {I. Br\"uckner and B. Metzler and H. Wehrheim},
title = {Optimizing Slicing of Formal Specifications by Deductive Verification},
journal = {Nordic Journal of Computing},
year = {2006},
volume = {13},
number = {1--2},
month = {August},
pages = {22--45},
publists = {brueckner,wehrheim},
abstract = { Slicing is a technique for extracting parts of programs or specifications with respect to certain criteria of interest. The extraction is carried out in such a way that properties as described by the slicing criterion are preserved, i.e., they hold in the complete program if and only if they hold in the sliced program. During verification, slicing is often employed to reduce the state space of specifications to a size tractable by a model checker. The computation of specification slices relies on the construction of dependence graphs, reflecting (at least) control and data dependencies in specifications. The more dependencies the graph has, the less removal of parts is possible. In this paper we present a technique for optimizing the construction of the dependence graph by using deductive verification techniques. More precisely, we propose a technique for showing that certain control dependencies in the graph can be eliminated. The technique employs small {\em deductive} proofs of the enabledness of certain transitions. Thereby we obtain dependence graphs with less control dependencies and as a consequence smaller specification slices which are an easier target for model checking. },
url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib06njc.pdf}
}
P. E. Sevinç, D. Basin, und E. -R. Olderog, "Controlling Access to Documents: A Formal Access Control Model" in Proc. ETRICS 2006, 2006.
@inproceedings{SBO06,
author = {P. E. Sevin\c{c} and D. Basin and E.-R. Olderog},
booktitle = {ETRICS 2006},
editor = {G\"unter M\"uller},
month = {June},
pages = {352--367},
publisher = {Springer-Verlag},
series = {LNCS},
title = {Controlling Access to Documents: A Formal Access Control Model},
volume = 3995, year = 2006, abstract = { Current access-control systems for documents suffer from one or more of the following limitations: they are coarse-grained, limited to XML documents, ot unable to maintain control over copies of documents once they are released by the system. We present a formal model of a system that overcomes all of these restrictions. It is very fine-grained, supporst a general class of documents, and provides a foundation for usage control. }
}
R. Meyer, J. Faber, und A. Rybalchenko, "Model Checking Duration Calculus: A Practical Approach" in Proc. Theoretical Aspects of Computing - ICTAC 2006, 2006.
@inproceedings{MFR2006,
author = {R. Meyer and J. Faber and A. Rybalchenko},
title = {Model Checking Duration Calculus: A Practical Approach},
booktitle = {Theoretical Aspects of Computing - ICTAC 2006},
year = {2006},
editor = {K. Barkaoui and A. Cavalcanti and A. Cerone},
series = {LNCS},
volume = {4281},
pages = {332--346},
pdf = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/MeyerFaberRybalchenko2006.pdf},
note = {This publication is available at \url{ http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11921240_23 } {SpringerLink}},
publists = {rmeyer,pea},
abstract = { Model checking of real-time systems with respect to Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. This task is difficult to automate. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to real world applications. Our algorithm significantly extends the subset of DC that can be handled. It decomposes DC specifications into sub-properties that can be verified independently. The decomposition bases on a novel distributive law for DC. We implemented the algorithm as part of our tool chain for the automated verification of systems comprising data, communication, and real-time aspects. Our translation facilitated a successful application of the tool chain on an industrial case study from the European Train Control System (ETCS). }
}
B. Beckert und A. Platzer, "Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program Verification" in
Proc. Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, 2006.
doi:
10.1007/11814771_23@inproceedings{DBLP:conf/cade/BeckertP06,
author = {Bernhard Beckert and Andr{\'e} Platzer},
title = {Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program Verification},
booktitle = {Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
year = {2006},
editor = {U. Furbach and N. Shankar},
volume = {4130},
series = {LNCS},
subseries = {LNAI},
pages = {266--280},
doi = {10.1007/11814771_23},
issn = {0302-9743},
isbn = {3-540-37187-7},
publisher = {Springer-Verlag},
keywords = {dynamic logic, sequent calculus, program logic, software verification, logical foundations of programming languages, object-orientation},
note = {\url{http://dx.doi.org/10.1007/11814771_23}{(c) Springer-Verlag}},
url = {http://symbolaris.com/pub/odl.pdf},
abstract = { We introduce a dynamic logic that is enriched by non-rigid functions, i.e., functions that may change their value from state to state (during program execution), and we present a (relatively) complete sequent calculus for this logic. In conjunction with dynamically typed object enumerators, non-rigid functions allow to embed notions of object-orientation in dynamic logic, thereby forming a basis for verification of object-oriented programs. A semantical generalisation of substitutions, called state update, which we add to the logic, constitutes the central technical device for dealing with object aliasing during function modification. With these few extensions, our dynamic logic captures the essential aspects of the complex verification system KeY and, hence, constitutes a foundation for object-oriented verification with the principles of reasoning that underly the successful KeY case studies. }
}
Dokument aufrufenB. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory" in Proc. 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), 2022.