MoVeS Modeling, Verification and Control of complex Systems: From Foundations to Power Network Appliances

Goal

Several phenomena in the context of power systems, like continuous dynamics, evolution of voltages, frequencies, discrete dynamics changes in network topology, and the uncertainty about power demand and supply require models and analyses of stochastic hybrid systems. None of the methods currently available are powerful enough to deal with real life large scale applications. A key reason for this is that the methods have been developed by different communities in relative isolation, motivated by different applications. 

In the MoVeS project synergies between the methods are systematically explored, in particular by establishing links between model checking, theorem proving, optimal control and randomized methods. 

Persons

Scientific Director

Publications
Measurability and Safety Verification for Stochastic Hybrid Systems

Fränzle, Martin and Hahn, Ernst Moritz Hahn and Hermanns, Holgers and Wolovick, Nicolas and Zhang, Lijun; Hybrid Systems: Computation and Control, 13th International Conference, HSCC 2011, Chicago, USA, Proceedings; 001 / 2011

Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems

Teige, Tino and Fränzle, Martin; Proceedings of the Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems; 001 / 2011

Combining Decomposition and Reduction for State Space Analysis of a Self-Stabilizing System - Best Paper Award

Müllner, Nils and Theel, Oliver and Fränzle, Martin; Advanced Information Networking and Applications, International Conference on; 003 / 2012

Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems

Fränzle, Martin and Gerwinn, Sebastian and Kröger, Paul and Abate, Alessandro and Katoen, Joost-Pieter; Formal Modeling and Analysis of Timed Systems; 2015

Confidence Bounds for Statistical Model Checking of Probabilistic Hybrid Systems

Ellen, Christian and Gerwinn, Sebastian and Fränzle, Martin; Formal Modeling and Analysis of Timed Systems - 10th International Conference, FORMATS 2012, London, UK; 009 / 2012

Modeling TCL via DTMC

Ellen, Christian and Fränzle, Martin and Gerwinn, Sebastian and Müllner, Nils; 009 / 2012

Combining Decomposition and Reduction for the State Space Analysis of Self-Stabilizing Systems

Müllner, Nils and Theel, Oliver and Fränzle, Martin; Journal of Computer and System Sciences (JCSS); 001 / 2013

Modeling Options for Demand Side Participation of Thermostatically Controlled Loads

Kamgarpour, Maryam and Ellen, Christian and Esmaeil Zadeh Soudjani, Sadegh and Gerwinn, Sebastian and Mathieu, Johanna L. and Müllner, Nils and Abate, Alessandro and Callaway, Duncan S. and Fränzle, Martin and Lygeros, John; Bulk Power System Dynamics and Control - IX Optimization, Security and Control of the Emerging Power Grid (IREP), 2013 IREP Symposium; 08 / 2013

Formal Synthesis and Validation of Inhomogeneous Thermostatically Controlled Loads

Esmaeil Zadeh Soudjani, Sadegh and Gerwinn, Sebastian and Ellen, Christian and Fränzle, Martin and Abate, Alessandro; Quantitative Evaluation of Systems; 2014

Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains

Ellen, Christian and Gerwinn, Sebastian and Fränzle, Martin; International Journal on Software Tools for Technology Transfer; 2014

Partners
Carl von Ossietzky Universität Oldenburg
www.uni-oldenburg.de
ETH Zürich
www.ethz.ch
Rheinisch-Westfälische Technische Hochschule Aachen (RWTH)
www.rwth-aachen.de/go/id/hi
TU Delft
Politecnico di Milano
www.elet.polimi.it/index.jsp
Honeywell spol. s.r.o.
www.honeywell.com

Duration

Start: 30.09.2010
End: 29.09.2013

Website of project