S. Gerwinn, E. Möhlmann, and A. Sieper, "Statistical Model Checking for Scenario-based verification of ADAS" , Waschl, H., Kolmanovsky, I., and Willems, F. Eds., Cham: Springer International Publishing.
doi: 10.1007/978-3-319-91569-2_4
@Inbook{GerwinnMS2019,
author = {Sebastian Gerwinn and Eike Möhlmann and Anja Sieper},
title = {Statistical Model Checking for Scenario-based verification of ADAS},
booktitle = {Control Strategies for Advanced Driver Assistance Systems and Autonomous Driving Functions : Development, Testing and Verification},
editor = {Waschl, Harald and Kolmanovsky, Ilya and Willems, Frank},
year = {2019},
publisher = {Springer International Publishing},
address = {Cham},
pages = {67--87},
abstract = {The increasing complexity of advanced driver assistant systems requires a thorough investigation of a high-dimensional input space. To alleviate this problem, simulation-based approaches have recently been proposed. An overall safety assessment, however, requires the simulation results to relate to the safety of such systems in real-world scenes. To this end, we propose a rigorous method of specifying requirements for these systems depending on the environmental situation and generating statistical evidence for the safety of the system in the specified environmental situations. We demonstrate this process in an exemplary highway scenario involving decision and perception uncertainty.},
isbn = {978-3-319-91569-2},
doi = {10.1007/978-3-319-91569-2_4},
url = {https://doi.org/10.1007/978-3-319-91569-2_4}
}
E. Möhlmann, "Automatic Stability Verification via Lyapunov Functions: Representations, Transformations, and Practical Issues" PhD Thesis , 2018.
@phdthesis{Moehlmann2018,
author = {M{\"{o}}hlmann, Eike},
title = {Automatic Stability Verification via Lyapunov Functions: Representations, Transformations, and Practical Issues},
school = {Carl von Ossietzky University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
year = {2018},
url = {https://oops.uni-oldenburg.de/id/eprint/4217},
W. Damm, S. Kemper, E. Möhlmann, T. Peikenkamp, and A. Rakow, "Using Traffic Sequence Charts for the Development of HAVs" in Proc. ERTS 2018, Toulouse, France, 2018.
@inproceedings{hal-01714060/DammKMPR2018, TITLE = {{Using Traffic Sequence Charts for the Development of HAVs}},
AUTHOR = {Damm, W and Kemper, S and M{\"o}hlmann, E and Peikenkamp, T and Rakow, A},
URL = {https://hal.archives-ouvertes.fr/hal-01714060},
BOOKTITLE = {{ERTS 2018}},
ADDRESS = {Toulouse, France},
SERIES = {9th European Congress on Embedded Real Time Software and Systems (ERTS 2018)},
YEAR = {2018},
MONTH = Jan, KEYWORDS = {highly autonomous driving ; formal specification languages ; testing ; type acceptance},
PDF = {https://hal.archives-ouvertes.fr/hal-01714060/file/ERTS_2018_paper_17.pdf},
HAL_ID = {hal-01714060},
HAL_VERSION = {v1},
}
W. Damm, E. Möhlmann, T. Peikenkamp, and A. Rakow, "A Formal Semantics for Traffic Sequence Charts" in Proc. Principles of Modeling - Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday, 2018.
doi: 10.1007/978-3-319-95246-8_11
@inproceedings{DBLP:conf/birthday/DammMPR18,
author = {Werner Damm and Eike M{\"{o}}hlmann and Thomas Peikenkamp and Astrid Rakow},
title = {A Formal Semantics for Traffic Sequence Charts},
booktitle = {Principles of Modeling - Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday},
editor = {Marten Lohstroh and Patricia Derler and Marjan Sirjani},
series = {Lecture Notes in Computer Science},
volume = {10760},
publisher = {Springer},
isbn = {978-3-319-95245-1},
pages = {182--205},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-95246-8\_11},
doi = {10.1007/978-3-319-95246-8\_11},
timestamp = {Fri, 20 Jul 2018 10:53:40 +0200},
biburl = {https://dblp.org/rec/bib/conf/birthday/DammMPR18},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
W. Damm, S. Kemper, E. Möhlmann, T. Peikenkamp, and A. Rakow, "Traffic Sequence Charts - From Visualization to Semantics" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 117, 2017.
@techreport{ATR/DKMPR2017,
author = {Werner Damm and Stephanie Kemper and Eike M{\"o}hlmann and Thomas Peikenkamp and Astrid Rakow},
title = {{Traffic Sequence Charts - From Visualization to Semantics}},
institution= {SFB/TR 14 AVACS},
month = {10},
year = {2017},
type = {Reports of SFB/TR 14 AVACS},
note = {http://www.avacs.org},
number = {117},
access = {open},
bibtex = {atr117.bib},
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},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_117.pdf},
pdf = {avacs_technical_report_117.pdf},
}
E. Möhlmann, W. Hagemann, and A. Rakow, "Verifying a PI Controller using SoapBox and Stabhyli" in Proc. ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria, 2016.
@inproceedings{workshop/arch/MohlmannHR16,
author = {Eike M{\"{o}}hlmann and Willem Hagemann and Astrid Rakow},
title = {Verifying a {PI} Controller using SoapBox and Stabhyli},
booktitle = {ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria},
editor = {Goran Frehse and Matthias Althoff},
series = {EPiC Series in Computing},
volume = {43},
pages = {115-125},
year = {2016},
publisher = {EasyChair},
url = {http://www.easychair.org/publications/paper/Verifying_a_PI_Controller_using_SoapBox_and_Stabhyli},
abstract = {We describe practical experiences on verifying a steering controller specification. The hybrid automaton implements a PI control rule and considers the vehicle's velocity as input from the environment. By combining the tools Stabhyli and SoapBox, we establish several safety and liveness properties for the steering controller, including convergence towards an equilibrium.},
note = {originally submitted and accepted for ARCH14},
issn = {2398-7340}
}
W. Damm, E. Möhlmann, and A. Rakow, "A Design Framework for Concurrent Hybrid System Controllers with Safety and Stability Annotations" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 105, 2016.
@techreport{report/ATR/DammMR2016,
author = {Werner Damm and Eike M{\"o}hlmann and Astrid Rakow},
title = {A Design Framework for Concurrent Hybrid System Controllers with Safety and Stability Annotations},
institution= {SFB/TR 14 AVACS},
year = {2016},
type = {Reports of SFB/TR 14 AVACS},
number = {105},
month = {April},
note = {http://www.avacs.org},
abstract = {We present an assume guarantee framework for hybrid systems which implements design principles tailored for loosely coupled controllers of safety critical applications. To bridge the gap between design and implementation level, the framework takes into account signal latencies and potential loss of coordination messages between controllers on a common plant. Safety as well as stability properties of a controller can be derived compositionally from its subcomponents. Industrial applications usually require safety and stability properties.},
access = {open},
bibtex = {atr105.bib},
pdf = {avacs_technical_report_105.pdf},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_105.pdf},
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,H4}
}
W. Hagemann and E. Möhlmann, "Inscribing H-Polyhedra in Quadrics using a Projective Generalization of Closed Sets" in Proc. Proceedings of the 27th Canadian Conference on Computational Geometry, CCCG 2015, 2015.
@inproceedings{conf/cccg/HagemannM2015a,
author = {Willem Hagemann and Eike M{\"o}hlmann},
title = {Inscribing H-Polyhedra in Quadrics using a Projective Generalization of Closed Sets},
booktitle = {Proceedings of the 27th Canadian Conference on Computational Geometry, {CCCG} 2015},
location = {Kingston, Ontario, Canada},
month = {August},
year = {2015},
url = {http://research.cs.queensu.ca/cccg2015/CCCG15-papers/07.pdf},
bookurl = {http://research.cs.queensu.ca/cccg2015/CCCG.pdf},
publisher = {Queen's University, Ontario, Canada},
subproject = {H3,H4},
abstract = {We present a projective generalization of closed sets, called complete projective embeddings, which allows us to inscribe H-polyhedra in quadrics efficiently. Essentially, the complete projective embedding of a closed convex set $P \subseteq K^d$ is a double cone in $K^{d+1}$. We show that complete projective embeddings of polyhedral sets are of particular interest and already occurred in the theory of linear fractional programming. Our approach works as follows: By projective principal axis transformation the quadric is converted to a hyperboloid and then approximated by an inner (right) spherical cylinder. Now, given an inscribed H-polytope of the spherical cross section, cylindrification of the polyhedron yields an inscribed H-polyhedron of the spherical cylinder and, hence, of the hyperboloid. After application of the inverse base transformation this approach finally yields an inscribed set of the quadric. The crucial task of this procedure is to find an appropriate generalization of closed sets, which is closed under the involved projective transformations and allows us to recover the non-projective equivalents to the inscribed sets obtained by our approach. It turns out that complete projective embeddings are the requested generalizations.},
}
E. Möhlmann, W. Hagemann, and O. E. Theel, "Hybrid Tools for Hybrid Systems - Proving Stability and Safety at Once" in Proc. Formal Modeling and Analysis of Timed Systems - 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings, 2015.
doi: 10.1007/978-3-319-22975-1_15
@inproceedings{conf/formats/MohlmannHT15,
author = {Eike M{\"{o}}hlmann and Willem Hagemann and Oliver E. Theel},
title = {Hybrid Tools for Hybrid Systems - Proving Stability and Safety at Once},
booktitle = {Formal Modeling and Analysis of Timed Systems - 13th International Conference, {FORMATS} 2015, Madrid, Spain, September 2-4, 2015, Proceedings},
pages = {222--239},
year = {2015},
month = {September},
url = {http://dx.doi.org/10.1007/978-3-319-22975-1_15},
doi = {10.1007/978-3-319-22975-1_15},
series = {Lecture Notes in Computer Science},
volume = {9268},
publisher = {Springer},
isbn = {978-3-319-22974-4},
subproject = {H3,H4},
abstract = {Industrial applications usually require safety and stability properties. The safety property guarantees that "something bad" never happens, and the stability property guarantees that "something good" eventually happens. The analyses of both properties are usually performed in isolation. In this work, we consider analyzing both properties by a single automatic approach for hybrid systems. We basically merge analyses of both properties to exploit the knowledge gained from the analysis of each of them in the analysis of the other. We show how both analyses can be divided into multiple steps and interlocked such that both benefit from each other. In fact, we compute single-mode Lyapunov functions, unroll the hybrid system’s automaton via repeated reachability queries, and, finally, compute a global Lyapunov function. Each reachability query is simplified by exploiting the knowledge gained from the single-mode Lyapunov functions. The final computation of the global Lyapunov function is simplified by a precise characterization of the reachable states and reuses the single-mode Lyapunov functions. We provide automated tools necessary to link the analyses and report on promising experiments we performed using our new prototype tool.},
}
E. Möhlmann and O. E. Theel, "Breaking Dense Structures: Proving Stability of Densely Structured Hybrid Systems" in Proc. Proceedings of the 4th International Workshop on Engineering Safety and Security Systems, ESSS 2015, Oslo, Norway, June 22, 2015., 2015.
doi: 10.4204/EPTCS.184.4
@inproceedings{conf/corr/MohlmannT15,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {Breaking Dense Structures: Proving Stability of Densely Structured Hybrid Systems},
booktitle = {Proceedings of the 4th International Workshop on Engineering Safety and Security Systems, {ESSS} 2015, Oslo, Norway, June 22, 2015.},
editor = {Pang, Jun and Liu, Yang and Mauw, Sjouke},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {184},
year = {2015},
publisher = {Open Publishing Association},
pages = {49--63},
doi = {10.4204/EPTCS.184.4},
ISSN = {2075-2180},
month = {June},
url = {http://dx.doi.org/10.4204/EPTCS.184.4},
subproject= {H4},
abstract = {Abstraction and refinement is widely used in software development. Such techniques are valuable since they allow to handle even more complex systems. One key point is the ability to decompose a large system into subsystems, analyze those subsystems and deduce properties of the larger system. As cyber-physical systems tend to become more and more complex, such techniques become more appealing. In 2009, Oehlerking and Theel presented a (de-)composition technique for hybrid systems. This technique is graph-based and constructs a Lyapunov function for hybrid systems having a complex discrete state space. The technique consists of (1) decomposing the underlying graph of the hybrid system into subgraphs, (2) computing multiple local Lyapunov functions for the subgraphs, and finally (3) composing the local Lyapunov functions into a piecewise Lyapunov function. A Lyapunov function can serve multiple purposes, e.g., it certifies stability or termination of a system or allows to construct invariant sets, which in turn may be used to certify safety and security. In this paper, we propose an improvement to the decomposing technique, which relaxes the graph structure before applying the decomposition technique. Our relaxation significantly reduces the connectivity of the graph by exploiting super-dense switching. The relaxation makes the decomposition technique more efficient on one hand and on the other allows to decompose a wider range of graph structures.},
}
W. Hagemann, E. Möhlmann, and O. E. Theel, "Hybrid Tools for Hybrid System: Proving Safety and Stability at once (Extended Version)" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 108, 2015.
@techreport{report/ATR/HagemannMT2015b,
author = {Willem Hagemann and Eike M{\"o}hlmann and Oliver E. Theel},
title = {Hybrid Tools for Hybrid System: Proving Safety and Stability at once (Extended Version)},
month = {September},
year = {2015},
institution= {SFB/TR 14 AVACS},
type = {Reports of SFB/TR 14 AVACS},
note = {http://www.avacs.org},
number = {108},
access = {open},
bibtex = {atr108.bib},
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},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_108.pdf},
pdf = {avacs_technical_report_108.pdf},
subproject = {H3,H4},
abstract = {Industrial applications usually require safety and stability properties. The safety property guarantees that "something bad" never happens, and the stability property guarantees that "something good" eventually happens. The analyses of both properties are usually performed in isolation. In this work, we consider analyzing both properties by a single automatic approach for hybrid systems. We basically merge analyses of both properties to exploit the knowledge gained from the analysis of each of them in the analysis of the other. We show how both analyses can be divided into multiple steps and interlocked such that both benefit from each other. In fact, we compute single-mode Lyapunov functions, unroll the hybrid system's automaton via repeated reachability queries, and, finally, compute a global Lyapunov function. Each reachability query is simplified by exploiting the knowledge gained from the single-mode Lyapunov functions. The final computation of the global Lyapunov function is simplified by a precise characterization of the reachable states and reuses the single-mode Lyapunov functions. We provide automated tools necessary to link the analyses and report on promising experiments we performed using our new prototype tool.},
}
O. Jubran, E. Möhlmann, and O. E. Theel, "Verifying Recurrence Properties in Self-Stabilization by Checking the Absence of Finite Counterexamples" in Proc. Stabilization, Safety, and Security of Distributed Systems - 17th International Symposium, SSS 2015, 2015.
doi: 10.1007/978-3-319-21741-3_9
@inproceedings{conf/sss/JubranMT15,
author = {Oday Jubran and Eike M{\"{o}}hlmann and Oliver E. Theel},
title = {Verifying Recurrence Properties in Self-Stabilization by Checking the Absence of Finite Counterexamples},
booktitle = {Stabilization, Safety, and Security of Distributed Systems - 17th International Symposium, {SSS} 2015},
editor = {Andrzej Pelc and Alexander A. Schwarzmann},
location = {Edmonton, AB, Canada},
month = {August},
year = {2015},
pages = {124--138},
url = {http://dx.doi.org/10.1007/978-3-319-21741-3_9},
doi = {10.1007/978-3-319-21741-3_9},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/sss/JubranMT15},
bibsource = {dblp computer science bibliography, http://dblp.org},
series = {Lecture Notes in Computer Science (LNCS)},
volume = {9212},
publisher = {Springer-Verlag},
bookurl = {http://dx.doi.org/10.1007/978-3-319-21741-3},
isbn = {978-3-319-21740-6},
subproject= {H4,S3},
abstract = {A performance-related property of a system can be defined as the ratio of states satisfying some condition in each execution of the system, which we signify as the recurrence of the condition in the execution. In this work, we concern self-stabilization with respect to this property: the convergence to an execution that guarantees a minimum recurrence of a condition. For a system exhibiting infinite executions, it may not be straightforward to verify that the system satisfies the property, while considering the convergence as well. Towards simplifying such a verification, we show that for each system violating the property, there exists a finite execution prefix that is a counterexample with a reasonably short length. Furthermore, we exploit model checking to verify the absence of such counterexamples, to conclude that a system satisfies its property. We apply this approach by using the nuXmv model checker to analyze the service time of a self-stabilizing mutual exclusion algorithm having a finite state space, and running over many topologies.},
}
E. Möhlmann and O. E. Theel, "Towards Counterexample-Guided Computation of Validated Stability Certificates for Hybrid Systems" in Proc. Proceedings of the 2nd Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2014, 2014.
@inproceedings{conf/CoNaIISI/MohlmannT14,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {{Towards Counterexample-Guided Computation of Validated Stability Certificates for Hybrid Systems}},
year = {2014},
month = {November},
issn = {2346-9927},
editor = {Marcelo M. Marciszack and Roberto M. Mu{\~{n}}oz and Mario A. Groppo},
booktitle = {Proceedings of the 2nd Congreso Nacional de Ingeniería Inform{\'{a}}tica / Aplicaciones Inform{\'{a}}ticas y de Sistemas de Informaci{\'{o}}n, CoNaIISI 2014},
location = {San Luis, Argentina},
publisher = {Red de Carreras de Ingenier{\'{i}}a Inform{\'{a}}tica / Sistemas de Informati{\'{o}}n (RIISIC)},
volume = {2},
issn = {2346-9927},
url = {http://www.informatik.uni-oldenburg.de/~eikemoe/pubs/CoNaIISI_123.pdf},
abstract = {We propose a method to obtain trustable Lyapunov-based certificates of stability for hybrid systems. A hybrid system is a system exhibiting discrete-time as well as continuous-time behaviors, e.g. embedded systems within a physical environment. Stability is a property which ensures that a system starting in any possible state will reach a desired state and remain there. Such systems are particularly useful when a certain autonomous operation is required, e.g. keeping a certain temperature or speed of a chemical reaction or steering a vehicle over a predefined track. Stable hybrid systems are extremely valuable because if an error disturbs their normal operation, they automatically "steer back" to normal operation. Stability can be certified by finding a so-called Lyapunov function. The search for this kind of functions usually involves solving systems of constraints. The state-of-the-art in Lyapunov-based stability verification is to use numerical methods to solve systems of inequalities, which if solvable indicate stability. We propose to use Satisfiability-Modulo-Theory (SMT) methods to (a) validate the results of a numerical solver and (b) use counterexamples to guide the numerical solver towards a valid solution.},
}
W. Damm, W. Hagemann, E. Möhlmann, and A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 95, 2014.
@techreport{report/ATR/DammHMR14,
author = {Werner Damm and Willem Hagemann and Eike M{\"o}hlmann and Astrid Rakow},
title = {Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling},
institution= {SFB/TR 14 AVACS},
month = {February},
year = {2014},
type = {Reports of SFB/TR 14 AVACS},
note = {http://www.avacs.org},
number = {95},
access = {open},
bibtex = {atr095.bib},
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},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_095.pdf},
pdf = {avacs_technical_report_095.pdf},
subproject = {H3,H4},
abstract = {In the search of design principles that allow compositional reasoning about safety and stability properties of hybrid controllers we examine a case study on a simplified driver assistance system for lane keeping and velocity control. We thereby target loosely coupled systems: the composed system has to accomplish a task that may depend on several of its subcomponents while little coordination between them is necessary. Our assistance system has to accomplish a comfortable centrifugal force, lane keeping and velocity control. This leads to an architecture composed of a velocity controller and a steering controller, where each controller has its local objectives and together they maintain a global objective. The steering controller makes time bounded promises about its steering, which the velocity controller uses for optimization. For this system, we deductively prove from the components' properties that the objectives of the composed system are accomplished.},
}
W. Damm, E. Möhlmann, and A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling" in Proc. Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14, 2014.
doi: 10.1145/2562059.2562120
@inproceedings{conf/hybrid/DammMR14,
author = {Werner Damm and Eike M{\"o}hlmann and Astrid Rakow},
title = {Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling},
editor = {Martin Fr{\"a}nzle and John Lygeros},
booktitle = {Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14},
location = {Berlin, Berlin, Germany},
month = {April},
year = {2014},
pages = {145-150},
numpages = {6},
ee = {http://doi.acm.org/10.1145/2562059.2562120},
crossref = {DBLP:conf/hybrid/2014},
publisher = {ACM},
isbn = {978-1-4503-2732-9},
acmid = {2562120},
url = {http://doi.acm.org/10.1145/2562059.2562120},
doi = {10.1145/2562059.2562120},
keywords = {Hybrid Systems, Automatic Verification, Stability, Safety, Composition, Interfaces, Specifications, Assume-Guarantee, Computer-Aided Design},
abstract = {In the search of design principles that allow compositional reasoning about safety and stability properties of hybrid controllers we examine a case study on a simplified driver assistance system for lane keeping and velocity control. We thereby target loosely coupled systems: the composed system has to accomplish a task that may depend on several of its subcomponents while little coordination between them is necessary. Our assistance system has to accomplish a comfortable centrifugal force, lane keeping and velocity control. This leads to an architecture composed of a velocity controller and a steering controller, where each controller has its local objectives and together they maintain a global objective. The steering controller makes time bounded promises about its steering, which the velocity controller uses for optimization. For this system, we deductively prove from the components' properties that the objectives of the composed system are accomplished.},
}
E. Möhlmann and O. E. Theel, "Towards Automatic Detection of Implicit Equality Constraints in Stability Verification of Hybrid Systems" in Proc. Proceedings of the 1th Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2013, 2013.
@inproceedings{conf/CoNaIISI/MohlmannT13,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {{Towards Automatic Detection of Implicit Equality Constraints in Stability Verification of Hybrid Systems}},
booktitle = {Proceedings of the 1th Congreso Nacional de Ingeniería Inform{\'{a}}tica / Aplicaciones Inform{\'{a}}ticas y de Sistemas de Informaci{\'{o}}n, CoNaIISI 2013},
year = {2013},
url = {http://conaiisi.frc.utn.edu.ar/PDFsParaPublicar/1/schedConfs/1/104-504-1-DR.pdf},
location = {C{\'{o}}rdoba, C{\'{o}}rdoba, Argentina},
keywords = {Hybrid Systems; Automatic Verification; Stability; Lyapunov Theory; Optimization; Sums-of-Squares},
editor = {Marcelo M. Marciszack and Roberto M. Mu{\~{n}}oz and Mario A. Groppo},
publisher = {Red de Carreras de Ingenier{\'{i}}a Inform{\'{a}}tica / Sistemas de Informati{\'{o}}n (RIISIC)},
issn = {2346-9927},
abstract = {We present a powerful heuristic that detects implicit equality constraints that may occur in the specification of systems of constraints in order to find Lyapunov-based certificates of stability for hybrid systems. A hybrid system is a fusion of systems exhibiting discrete-time as well as continuous-time behavior, e.g.\ embedded systems within a physical environment. Stability is a property which ensures that a system starting in any possible state will reach a desired state and remain there. Such systems are particularly useful where a certain autonomous operation is required, e.g.\ keeping a certain temperature or speed of a chemical reaction or steering a vehicle over a predefined track. Stable hybrid systems are extremely valuable because after an error has disturbed their normal operation, they automatically \enquote{steer back} to normal operation. Stability can be certified by finding a so-called Lyapunov function. The search for this kind of function usually involves solving systems of inequality constraints. We have identified and implemented a heuristic that detects implicitly specified equality constraints and tries to resolve them by substitution.},
}
E. Möhlmann and O. E. Theel, "Stabhyli: A Tool for Automatic Stability Verification of Non-Linear Hybrid Systems" in Proc. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'13, 2013.
@inproceedings{conf/hybrid/MohlmannT13,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {Stabhyli: {A} {T}ool for {A}utomatic {S}tability {V}erification of {N}on-{L}inear {H}ybrid {S}ystems},
booktitle = {Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'13},
year = {2013},
pages = {107-112},
url = {http://doi.acm.org/10.1145/2461328.2461347},
crossref = {DBLP:conf/hybrid/2013},
location = {Philadelphia, Pennsylvania, USA},
acmid = {2461347},
keywords = {LMIS, automatic verification, computer-aided design, hybrid systems, lyapunov theory, stability, sums-of-squares},
abstract = {We present Stabhyli, a tool that automatically proves stability of non-linear hybrid systems. Hybrid systems are systems that exhibit discrete as well as continuous behavior. The stability property basically ensures that a system exposed to a faulty environment (e.g. suffering from disturbances) will be able to regain a "good" operation mode as long as errors occur not too frequently. Stabilizing Hybrid systems are omnipresent, for instance in control applications where a discrete controller is controlling a time-continuous process such as a car's movement or a particular chemical reaction. We have implemented a tool to automatically derive a certificate of stability for non-linear hybrid systems. Certificates are obtained by Lyapunov theory combined with decomposition and composition techniques.},
editor = {Calin Belta and Franjo Ivancic},
publisher = {ACM},
isbn = {978-1-4503-1567-8},
}
A. Bouajjani, R. Meyer, and E. Möhlmann, "Deciding Robustness against Total Store Ordering" in Proc. Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, 2011.
doi: 10.1007/978-3-642-22012-8_34
@inproceedings{conf/icalp/BouajjaniMM2011,
author = {Ahmed Bouajjani and Roland Meyer and Eike M{\"{o}}hlmann},
title = {Deciding Robustness against Total Store Ordering},
booktitle = {Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II},
year = {2011},
pages = {428-440},
url = {http://dx.doi.org/10.1007/978-3-642-22012-8_34},
doi = {10.1007/978-3-642-22012-8_34},
bibsource = {DBLP, http://dblp.uni-trier.de},
isbn = {978-3-642-22011-1},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Ji{\v{r}\'{i}}},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
volume = {6756},
abstract = {We address the problem of deciding robustness of a program against the total store ordering (TSO) relaxed memory model, i.e., of checking whether the behaviour under TSO coincides with the expected sequential consistency (SC) semantics. We prove that this problem is PSpace-complete. The key insight is that violations to robustness can be detected on pairs of SC computations.}
}
W. Damm, E. Möhlmann, and A. Rakow, Traffic Sequence Charts for the ENABLE-S3 Test ArchitectureSpringer Nature Switzerland AG year = 2019: Springer International Publishing.
doi: 10.1007/978-3-030-14628-3
@incollection{DammRM2019a,
author = {Werner Damm and Eike M{\"{o}}hlmann and Astrid Rakow},
title = {Traffic Sequence Charts for the ENABLE-S3 Test Architecture},
editor = {Leitner, Andrea and Watzenig, Daniel and Ibanez-Guzman, Javier} booktitle = {Validation and Verification of Automated Systems},
publisher = {Springer International Publishing},
address = {Springer Nature Switzerland AG} year = 2019, pages = "45--60", chapter = 6, isbn = {978-3-030-14628-3},
url = {https://doi.org/10.1007/978-3-030-14628-3},
doi = {10.1007/978-3-030-14628-3},
}
W. Damm, E. Möhlmann, and A. Rakow, Scenario Discovery Process Based on Traffic Sequence ChartsSpringer Nature Switzerland AG year = 2019: Springer International Publishing.
doi: 10.1007/978-3-030-14628-3_7
@incollection{DammRM2019b,
author = {Werner Damm and Eike M{\"{o}}hlmann and Astrid Rakow},
title = {Scenario Discovery Process Based on Traffic Sequence Charts},
editor = {Leitner, Andrea and Watzenig, Daniel and Ibanez-Guzman, Javier} booktitle = {Validation and Verification of Automated Systems},
publisher = {Springer International Publishing},
address = {Springer Nature Switzerland AG} year = 2019, pages = "61--73", chapter = 7, isbn = {978-3-030-14628-3},
url = {https://doi.org/10.1007/978-3-030-14628-3_7},
doi = {10.1007/978-3-030-14628-3_7},
}
H. Esen, M. Kneissl, A. Molin, S. vom Dorff, B. Böddeker, E. Möhlmann, U. Brockmeyer, T. Teige, G. Garcia Padilla, and S. Kalisvaart, Validation of Automated Valet ParkingSpringer Nature Switzerland AG year = 2019: Springer International Publishing.
doi: 10.1007/978-3-030-14628-3_16
@incollection{EsenKMDBMBTPK2019b,
author = {Esen, Hasan and Kneissl, Maximilian and Molin, Adam and vom Dorff, Sebastian and B{\"{o}}ddeker, Bert and M{\"{o}}hlmann, Eike and Brockmeyer, Udo and Teige, Tino and Garcia Padilla, Gustavo and Kalisvaart, Sytze},
title = {Validation of Automated Valet Parking},
editor = {Leitner, Andrea and Watzenig, Daniel and Ibanez-Guzman, Javier} booktitle = {Validation and Verification of Automated Systems},
publisher = {Springer International Publishing},
address = {Springer Nature Switzerland AG} year = 2019, pages = "207--220", chapter = 16, isbn = {978-3-030-14628-3},
url = {https://doi.org/10.1007/978-3-030-14628-3_16},
doi = {10.1007/978-3-030-14628-3_16},
}
E. Möhlmann, "Hiding Relaxed Semantics from a User - Design and Implementation of Fence Insertion Algorithms for Concurrent Programs" Master's Thesis (Diplomarbeit) , 2010.
@thesis{Moehlmann2010,
author = {Eike M{\"o}hlmann},
title = {Hiding Relaxed Semantics from a User - Design and Implementation of Fence Insertion Algorithms for Concurrent Programs},
type = {Master's Thesis ({Diplomarbeit})},
year = {2010},
school = {LIAFA and University of Oldenburg},
supervisor = {Ahmed Bouajjani and Ernst Rüdiger Olderog and Roland Meyer},
E. Möhlmann and J. Timmermann, "iPosix - Ein objektorientierter Kernel in C++" Bachelor's Thesis (Studienarbeit, Individuelles Project) , 2009.
@thesis{Moehlmann2009,
author = {Eike M{\"o}hlmann and Janko Timmermann},
title = {{iPosix - Ein objektorientierter Kernel in C++}},
type = {Bachelor's Thesis ({Studienarbeit, Individuelles Project})},
year = {2009},
month = SEP, school = {University of Oldenburg},
url = {http://www.svs.informatik.uni-oldenburg.de/download/thesis/IP-20090914-moehlmann_timmermann-iPosix.pdf},
supervisor = {Oliver Theel and Christian Strom},
}
B. Hullmann, "Entwurf und Implementierung einer kamerabasierten, augengesteuerten Eingabemöglichkeit für graphische Benutzeroberflächen" Bachelor's Thesis , University of Oldenburg, 2014.
@thesis{Hullmann2014,
author = {Bjoern Hullmann},
title = {Entwurf und Implementierung einer kamerabasierten, augengesteuerten Eingabemöglichkeit für graphische Benutzeroberflächen},
type = {Bachelor's Thesis},
year = {2014},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {https://www.uni-oldenburg.de/informatik/svs/lehre/abschlussarbeiten/2014/augengesteuerte-bedienung/},
key = EM, }
M. Luebke, "Konstruktion und Aufbau eines fehlertoleranten, autonomen Rasenmähroboters" Master's Thesis (Diplomarbeit) , University of Oldenburg, 2014.
@thesis{Luebke2014,
author = {Michael Luebke},
title = {Konstruktion und Aufbau eines fehlertoleranten, autonomen Rasenm{\"a}hroboters},
type = {Master's Thesis ({Diplomarbeit})},
year = {2014},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.uni-oldenburg.de/informatik/svs/lehre/abschlussarbeiten/2014/konstruktion-und-aufbau-eines-autonomen-fehlertoleranten-rasenmaehroboters/},
key = EM, }
S. Reichel, "Running a standard Linux distribution on a smartphone" Master's Thesis , University of Oldenburg, 2015.
@thesis{Reichel2014,
author = {Sebastian Reichel},
title = {Running a standard Linux distribution on a smartphone},
type = {Master's Thesis},
year = {2015},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {https://www.uni-oldenburg.de/informatik/svs/lehre/abschlussarbeiten/2015/running-a-standard-linux-distribution-on-a-smartphone/},
key = EM, }
S. Jakubowski, "Entwurf und Implementierung eines prototypischen Web-Shops zur Erfassung und Abwicklung von Steckperlenbilderbestellungen" Master's Thesis , University of Oldenburg, 2015.
@thesis{Jakubowski2015,
author = {Simon Jakubowski},
title = {Entwurf und Implementierung eines prototypischen Web-Shops zur Erfassung und Abwicklung von Steckperlenbilderbestellungen},
type = {Master's Thesis},
year = {2015},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.uni-oldenburg.de/informatik/svs/lehre/abschlussarbeiten/2015/web-shop-fuer-steckperlenbilder/},
key = EM, }
P. Zschoche, "Automatisierte Erkennung und Eliminierung impliziter Äquivalenzen in quantifizierten nicht-linearen Ungleichungssystemen zur Stabilitätsverifikation hybrider Systeme mittels Lyapunov-Theorie" Bachelor's Thesis , University of Oldenburg, 2015.
@thesis{Zschoche2015,
author = {Philipp Zschoche},
title = {Automatisierte Erkennung und Eliminierung impliziter {\"A}quivalenzen in quantifizierten nicht-linearen Ungleichungssystemen zur Stabilit{\"a}tsverifikation hybrider Systeme mittels Lyapunov-Theorie},
year = {2015},
type = {Bachelor's Thesis},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {https://www.uni-oldenburg.de/informatik/svs/lehre/abschlussarbeiten/2015/automatisierte-erkennung-und-eliminierung-impliziter-aquivalenzen-in-quantifizierten-nicht-linearen-ungleichungssystemen-zur-stabilitatsverifikation-hybrider-systeme-mittels-lyapunov-theorie/},
key = EM,
