Post-Doc Researcher in the CONVECS group at INRIA Rhône-Alpes in Grenoble
I studied Applied Computer Sciences and Mathematics at the University of Augsburg. In 2005 I finished my diploma thesis in cooperation with KUKA SysTec (now part of KUKA AG). From 2005 to 2009 worked as a researcher at the University of Augsburg. From 2009 to 2011 I worked as a researcher at the Otto-von-Guericke University of Magdeburg, where I finished my PhD in safety analysis.
Besides research, I taught university courses in industrial robot programming, Java smartcards programming, cryptographic protocols and mathematical logics. In several seminars and university courses we used the SCADE suite as academic partner of Esterel Technologies. I also supervised several Bachelor, Master and Diploma theses, both directly at the university and in cooperation with companies like KUKA AG or Infineon Technologies.
My main research interest is to use formal methods and mathematics to provide correct and efficient solutions for real-world problems, in particular for safety critical systems.
Currently I am working on the formal verification of choreography specifications (e.g. BPMN 2.0) which are implemented via distributed systems with asynchronous communication. For this I use the CADP toolbox, which is developed in the CONVECS (formerly VASY) group at INRIA Rhône-Alpes. I work on encoding choreographies in LOTOS NT, analyze them for properties like realizability and, if necessary, interpret CADP counterexamples. This identifies all problematic messages in a choreography, and using additional synchronization messages, proposes a solution which enforces realizability. I have implemented the approach in Python to automatize is completely.
For my PhD thesis I developed a method for a combined quantitative and qualitative model-based safety analysis, using model-checking tools like PRISM, MRMC and NuSMV. I implemented an appropriate modeling language using the ANTlr toolkit and the necessary model transformations in Common Lisp. I also worked on the integration of model-based safety analysis into the SCADE suite. My work on resulted in more than 16 publications, most notably at SAFECOMP (2007 and 2011), PRDC (2011) and HASE (2012 and 2010). My work is also the basis for the DFG-founded research project Probabilistic Models for Safety Analysis (ProMoSA), and is continued at Magdeburg by two PhD students.
In my diploma thesis I applied mathematical optimization to tune mixed palletizing algorithms for industrial robots to produce a minimal number of maximally stable pallets from a set of goods. The implementation was done in C# and comprised highly optimized mathematical algorithms, in particular for estimation techniques to reduce the number of (very costly) objective function calls. The simulation environment which I developed was in internal use at KUKA SysTec for several years afterwards.
Choreography Monitor (choreomon): This software analyzes specifications of choreographies with the CADP toolbox. It decides whether a choreography is realizable. If this is not the case, the counterexamples provided by CADP are exploited to add synchronization messages to the choreography. It is realized in Python, the approach is described in our ATVA12 paper.
Verification of Choreographies (verchor): This software provides a generic format for different choreography specifications (e.g., BPMN 2.0, conversation protocols) based on XML. Models are validated using XSD and are transformed to Lotos NT specifications for analysis with the CADP toolbox.
Safety Analysis and Modeling Language (SAML): This language is an extension of the PRISM modeling language. It allows to model Markov Decision Processes and is especially suited for modeling safety critical systems. SAML models are transformed for different model checkers, e.g., PRISM, MRMC, NuSMV or Cadence SMV, depending on the nature of the properties to verify. The transformations are proven to preserve the semantics of the models. The toolchain is realized using ANTlr, Java and Common Lisp.
Genetic Optimization with Kriging and Evolutionary Learning (GOKEL): This software provides a generic interface for multi-objective optimization algorithms. I implemented the algorithms NSGA-2, ParEGO and OEGADO to optimize automated palletizing algorithms for stability of pallets, packing density and pallet numbers. It is realized in C#, provides a GUI, an objective function interface and allows to specify the allowed time for optimization.
A short list of talks I gave in addition to the presentations of my articles at conferences:
Verification of Interaction Based Systems presented in Grenoble at Schneider Electric with whom we collaborate on that topic, May 2012
Quantitative and Qualitative Model-Based Safety Analysis presented in Toulouse at ONERA for the Model-Based Safety Assessment Workshop, March 2011
Multi-Objective Optimization of Formal Specifications Simon Struck, Matthias Güdemann, Michael Lipaczewski & Frank Ortmeier, Proceedings of the 14th High Assurance System Engineering Symposium (HASE 2012) IEEE, to appear October 2012
Counterexample Guided Synthesis of Monitors for Realizability Enforcement Matthias Güdemann, Gwen Salaün, Meriem Ouderni, Proceedings of Automated Technology for Verification and Analyis (ATVA 2012), to appear October 2012
Trajectory Description Conception for Industrial Robots Sergey Alatartsev, Matthias Güdemann, Frank Ortmeier, Proceedings of the 7th German Conference on Robotics (ROBOTIK), 2012
The ForMoSA Approach to Qualitative and Quantitative Model-Based Safety Analysis Axel Habermaier, Matthias Güdemann, Frank Ortmeier, Wolfgang Reif & Gerhard Schellhorn, in Railway Safety, Reliability and Security: Technologies and System Engineering, IGI Global, 2012
Unifying Probabilistic and Traditional Formal Model-Based Analysis Matthias Güdemann, Michael Lipaczewski, Simon Struck & Frank Ortmeier, Proceedings of 8. Dagstuhl-Workshop on Model-Based Development of Embedded Systems (MBEES), 2012
Qualitative and Quantitative Formal Model-Based Safety Analysis Matthias Güdemann PhD Thesis, 2011
Model-Based Multi-Objective Safety Optimization Matthias Güdemann & Frank Ortmeier, Proceedings of the 30th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2011) Springer LNCS, 2011
Towards Model-driven Safety Analysis Matthias Güdemann & Frank Ortmeier, Proceedings of the 3rd international Workshop on Dependable Control of Discrete Systems (DCDS 11) IEEE, 2011
Tool Supported Model-Based Safety Analysis and Optimization Matthias Güdemann, Michael Lipaczewski & Frank Ortmeier, Proceedings of the 17th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC 2011), 2011
Towards Making Dependability Visual - Combining Model-Based Design and Virtual Realities Frank Ortmeier, Matthias Güdemann, Michael Lipaczewski, Marco Schumann & Robert Eschbach, Proceedings of the 17th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC 2011), 2011
Practical Experiences in Model-Based Safety Analysis Frank Ortmeier, Michael Lipaczewski & Matthias Güdemann, Proceedings of the 2nd International Workshop on Digital Engineering (IWDE), 2011
A Framework for Qualitative and Quantitative Model-Based Safety Analysis Matthias Güdemann & Frank Ortmeier, Proceedings of the 12th High Assurance System Engineering Symposium (HASE 2010) IEEE, 2010
Probabilistic Model-Based Safety Analysis Matthias Güdemann & Frank Ortmeier, Proceedings of the 8th Workshop on Quantitative Aspects of Programming Languages (QAPL 2010) ENTCS, 2010
Quantitative Model-Based Safety Analysis: A Case Study Matthias Güdemann & Frank Ortmeier, Proceedings of 5th conference for Sicherheit, Schutz und Zuverlaessigkeit (SICHERHEIT 10) Lecture Notes in Informatics (LNI), 2010
SysML in Digital Engineering Matthias Güdemann, Stefan Kegel, Frank Ortmeier, Olaf Poenicke & Klaus Richter, Proceedings of 1st International Workshop on Digital Engineering (IWDE) ACM, 2010
ProMoSA - Probabilistic Models for Safety Analysis Frank Ortmeier & Matthias Güdemann, Proceedings of 6th Dagstuhl-Workshop MBEES 2010: Model-Based Development of Embedded Systems, 2010
A specification and construction paradigm for Organic Computing systems Matthias Güdemann, Florian Nafz, Frank Ortmeier, Hella Seebach & Wolfgang Reif, Proceedings of the 2nd IEEE International Conference on Self-Adaptive and Self-Organizing Systems pages 233-242 IEEE, 2010
Computing Ordered Minimal Critical Sets Matthias Güdemann, Frank Ortmeier & Wolfgang Reif, Proceedings of the 7th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 08), 2008
Developing Safety-critical Mechatronical Systems Matthias Güdemann, Frank Ortmeier & Wolfgang Reif, Self-optimizing Mechatronic Systems: Design the Future HNI-Verlagsschriftenreihe, 2008
Modeling of self-adaptive systems with SCADE Matthias Güdemann, Andreas Angerer, Frank Ortmeier & Wolfgang Reif, Proceedings of the 40th IEEE International Symposium on Circuits and Systems (ISCAS) IEEE, 2007
Using Deductive Cause Consequence Analysis (DCCA) with SCADE Matthias Güdemann, Frank Ortmeier & Wolfgang Reif, Proceedings of SAFECOMP 2007 Springer LNCS, 2007
Formal Failure Models Frank Ortmeier, Matthias Güdemann & Wolfgang Reif, Proceedings of the 1st IFAC Workshop on Dependable Control of Discrete Systems (DCDS 07) Elsevier, 2007
Towards Safe and Secure Organic Computing Applications Matthias Güdemann, Florian Nafz, Wolfgang Reif & Hella Seebach, INFORMATIK 2006 – Informatik für Menschen pages 153-160 Bonn, Germany : Köllen Verlag, 2006
Formal Modeling and Verification of Systems with Self-x Properties Matthias Güdemann, Frank Ortmeier & Wolfgang Reif, Proceedings of the 3rd International Conference on Autonomic and Trusted Computing (ATC-06) Springer, 2006
Safety and Dependability Analysis of Self-Adaptive Systems Matthias Güdemann, Frank Ortmeier & Wolfgang Reif, Proceedings of the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 06) IEEE, 2006