13th International Conference on integrated Formal Methods (iFM 2017)

Main Conference

Jane Hillston (University of Edinburgh, UK)

Integrating Inference with Stochastic Process Algebra Models
André Platzer (CMU, USA)

Logic & Proofs for Cyber-Physical Systems with KeYmaera X
Martin Vechev (ETH Zurich, Switzerland)

Machine Learning for Programming

PhD Symposium

Mike Nicolai (Siemens, Belgium)

Dr. Mike Nicolai is a Research Manager and group leader at Siemens Industry Software N.V. His team works on Model-based Systems Engineering (MBSE) and Systems-driven Product Development (SDPD). He holds a PhD in Mechanical Engineering from RWTH Aachen University and a degree in Electrical Engineering from Technical University Braunschweig. His current main interests are engineering design, systems engineering, simulation, optimization and high performance computing. Before starting at Siemens Industry Software he worked for both academia and industry, with assignments in various engineering domains - reaching from oilfield sector over medical devices up to autonomous driving and others. Most projects had some aspects of CAE prototype tool development.

Automatic Reasoning for Novel Engineering Designs

A novel design of a complex engineering system depends on creativity, intuition and a deep technical understanding of its designer - which often is also secured by a patent. Such systems have in most cases a multi-physical nature and are rarely understood by one single engineer. An example for such a design problem is the design of hybrid automotive drivetrain. The dependency of each component on each other is hard to grasp intuitively or analytically in simple mathematical models. The only remedy is a systems-driven product development process, were design decisions are based on behavior simulations, multiple domain-experts and were also alternative designs are taken into account. Especially the alternative solutions for one specific engineering problem often decide on the success of a product.
In the presentation design examples from automotive, aerospace and marine engineering will be shown to illustrate the domain independence of the problem and how an architecture description can be used to describe one specific design solution. Starting from such an architecture description a method will be presented which allows generating such architectures from a declarative design model. This declarative model captures the designer's intent and it must be formal such that the method can translate it into a constraint problem to generate complying solutions. Having such process various challenges arises, e.g. symmetry breaking, problem encoding, solver limitations and others. Some of them will be highlighted in presentation. The presentation will be concluded with the display of realistic examples where novel designs were created. These designs are novel in the sense that they perform better as known patented solutions.