Research Overview: My research is about robust software engineering using domain specific languages and formal verification. I enable practicing engineers to benefit from these technologies in their daily work. Together with other colleagues, I deploy domain specific model driven engineering and automated formal verification to achieve 5-10x improvement of productivity and quality and enable completely new use-cases. I work with people from various business domains -- healthcare, industrial software, power generation or mobility.
DSLs eliminate accidental complexity of development artefacts by using adequate and domain appropriate constructs. This increases productivity via higher automation and allows easier definition of tooling. Furthermore, the quality can be ensured in a constructive manner since many categories of errors and inconsistencies can be simply avoided up front. To efficiently build and evolve DSLs and associated tooling I am using JetBrain's Meta Programming System (MPS).
Formal verification is a key technology to reach high assurance of the dependability of software intensive systems. I am especially interested in enabling practicing engineers to use automated formal verification techniques in their daily work -- I develop methods and tooling for deploying formal methods for a broader audience of practitioners in software/systems engineering or various business domains. I strongly believe that DSLs and formal verification used in a synnergetic manner have a huge potential.
I continuously publish about my research in peer-reviewed international venues. Below is an overview over my recent papers:
DSLs: Experiences and lessons learnt from building and deploying industrial eco-systems of DSLs in are presented in ASE'13, SoSyM'17, Modellierung'18, DevOps@MODELS'19 and MPS Book Chapter about Experiences from Siemens'21. Testing of DSLs implementations is a cornerstone to the wide adoption of DSLs - our work is presented in AST'16 and SQJ'17. Using DSLs for in for engineering dependability engineering ASSURE'15, RAMS'17. Modelling of requirements in RE'13, ACES@MODELS'13, MBT'12. Deeply integrated MDE environment is presented in Proc. of IEEE'11. Experiences with teaching language engineering to software engineering practitioners in MODELS'17.
Formal verification: DSLs and MDE enable usable formal verification as described in FormSERA'12, MoDeVVa'12, NFM'13, ASE'14, STTT'19, FormaliSE'19. The papers describe approaches, methods and tooling concepts which proved to be successful for bringing formal approached closer to practitioners. Characterizing completeness degree of incomplete verification is essential for getting credit about formal verification results for certification - as presented in Verisure'15 and ASSURE'16. I am one of the organizers of the AFFORD series of workshops about bringing formal methods to practicing engineers.
Assurance: Using DSLs for modeling and automation of dependability assurance is presented in ASSURE'15, RAMS'17, SafeComp'20, MPS Book Chapter about FASTEN'21.
During my PhD, my research was about program comprehension and reverse engineering - an overview is here.