Dr. Kai Lampka

"Analysis of systems with quantifiable constraints: Fighting abstraction loss and state space explosion"

State-based modeling methods such as UML state charts, methods known formprocess calculi, Petri nets and all their numerous extensions are expressive enough for capturing most important aspects of system behaviors. Thus state-based modeling methods provide a well accepted basis for analyzing complex systems. However, when it comes to the actual analysismany high-level modeling methods require their entities to be expanded intostate transition systems which explicitly cover all possible evolutions of the system under analysis. This transformation suffers from the well knownstate-space explosion, as the number of systems states can be exponentialwith respect to the number of concurrent components of the system model. The past decades have seen intensive research efforts for tackling therestriction in size and complexity of analyzable models. The developed approaches ranges from analytic methodologies, which provide closed-form solution for answering system-relevant questions of interest, over symbolic techniques which are robust w. r. t. the number of system states, up to partial-order reduction methods which exploit system inherent symmetries. Targeting the limitations of state-based analysis of quantifiable systems, this talk elaborates on the following strategies:
1. Heterogeneous analysis: Coupling Timed Automata and Real Time Calculus
2. Testing formal models against time-series of measurements
3. BDD-based techniques for quantitative analyses: are we done yet?