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}
}
S. Kemper, "SAT-based verification for timed component connectors" Science of Computer Programming, vol. 77, iss. 7–8.
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}
}
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}
}
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. }
S. Kemper, "Modelling and Analysis of Real-Time Coordination Patterns" PhD Thesis , 2011.
@PHDTHESIS{Kem11phd,
author = {Stephanie Kemper},
title = {Modelling and Analysis of Real-Time Coordination Patterns},
school = {{Leiden Institute of Advanced Computer Science (LIACS)}},
year = {2011},
adress = {Leiden, The Netherlands},
isbn = {978-90-8891-360-0},
pages = {165}
