S. Linker, Diagrammatic Specification of Mobile Real-Time SystemsSpringer Berlin / Heidelberg.
@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}
G. v. Bochmann, M. Hilscher, S. Linker, and E. -R. Olderog, "Synthesizing and Verifying Controllers for Multi-lane Traffic Maneuvers" Formal Aspects of Computing, vol. 29, iss. 4.
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}
}
S. Linker and M. Hilscher, "Proof Theory of a Multi-Lane Spatial Logic" Logical Methods in Computer Science, vol. 11, iss. 3.
@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}
}
G. v. Bochmann, M. Hilscher, S. Linker, and 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}
}
S. Linker and 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}
}
M. Hilscher, S. Linker, and 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. 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.}
}
J. Faber, S. Linker, E. Olderog, and J. Quesel, "Syspect - Modelling, Specifying, and Verifying Real-Time Systems with Rich Data" International Journal of Software and Informatics, vol. 5, iss. 1-2.
@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}
}
M. Hilscher, S. Linker, E. -R. Olderog, and 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. }
}
