Workshop Program


Dr. Daniel Ratiu, Siemens AG, Germany
Title: Enabling Software Verification for Practicing Engineers with Domain Specific Languages
Abstract: Despite the maturity of current verification techniques, formal verification tools have not found their way in the daily practice yet. The main reason for the low adoption is related to pragmatic aspects such as usability or the cost of applying formal verification (e.g. specifying properties, running the analyses, interpreting the results). For a large majority of developers, formal verification techniques are seen rather as expert tools and not as engineering tools that can be used on a daily basis. This is mostly the case in the context of main stream systems (e.g. automotive, medical, industrial automation) where pragmatics (e.g. personnel skills, cost structures, deadlines, existent processes) plays a major role. I will present our approach and experience to tackle some of these challenges with the help of domain specific languages in the mbeddr project ( and its extensions at Siemens.

Bio: Daniel Ratiu works as researcher, coach and software engineer for Siemens Corporate Technology in Munich. His focus is on robust software development in context of dependable systems with the help of domain specific languages and formal verification Before joining Siemens, Daniel was research group lead at fortiss Research Institute in Munich. In 2009 he obtained a PhD degree from the Technische Universität München.

Dr. Michael Sedlmair, University of Vienna, Austria
Title: Human-centered Methods in Visualization Research
Abstract: Visualization systems provide a unique way for people to interact, explore, and better understand their data. Visualization systems might, for instance, help medical doctors to base tricky medication decisions on historic patient data; journalists to get a quick overview over large sets of documents; or economists to better understand stock trends.
As visualization systems target human users, closely involving them into design and research processes is crucial. While this importance has been acknowledged many times, realizing such a human-centered focus in day-to-day research practices is challenging.
This talk will shed some light into existing human-centered methods that are used in visualization research, as well as the challenges that come with them. To illustrate these aspects, I will present case studies from several visualization research projects, such as my own 3.5-year collaboration with automotive engineers at BMW. The ultimate goal of the talk would be to help building a bridge between the human-centered challenges faced in visualization research and those in formal methods.

Bio: Michael Sedlmair is an assistant professor at the University of Vienna, where he works at the intersection of human-computer interaction, visualization, and data analysis. His specific research interests focus on studying visual data analysis techniques, tools, and users in real-world settings, and innovating and refining human-centered research methods and methodologies for the area of data analysis. Previously, he worked at the University of British Columbia, University of Munich, and the BMW Group Research and Technology.


9:30 – 10:30: Session 1

  • 9:30 Welcome
  • 9:50 Keynote: Michael Sedlmair, University of Vienna, Austria
    Human-centered Methods in Visualization Research

Coffee Break

11:00 – 13:00: Session 2

  • 11:00 Paolo Arcaini, Silvia Bonfanti, Angelo Gargantini and Elvinia Riccobene
    Visual notation and patterns for Abstract State Machines.
  • 11:30 Ulyana Tikhonova, Maarten Manders and R.C. Boudewijns
    Visualization of Formal Specifications for Understanding and Debugging an Industrial DSL
  • 12:00 Khanh-Hoang Doan, Martin Gogolla and Frank HilkenTowards a Developer-Oriented Process for Verifying Behavioral Properties in UML and OCL Models
  • 12:30 Phan Vo, Maria Spichkova
    Model-based generation of natural language specifications

Lunch Break (13:00 – 14:00)

14:00 – 15:30: Session 3

  • 14:00 Keynote:  Daniel Ratiu, Siemens AG, Germany
    Enabling Software Verification for Practicing Engineers with Domain Specific Languages
  • 14:40 Antonio Cerone
    Human-Oriented Formal Modelling of Human-Computer Interaction: Practitioners’ and Students’ Perspectives
  • 15:10 Maria Spichkova
    “Boring formal methods” or “Sherlock Holmes deduction methods”? 

Coffee Break

16:00 – 17:30: Session 4

  • 16:00 Peter Herrmann and Jan Olaf Blech
    Formal Model-based Development in Industrial Automation with Reactive Blocks
  • 16:30 Nasser Alzahrani, Maria Spichkova and Jan Olaf Blech
    Spatio-temporal model for property based testing
  • 17:00 Group discussion and Plans for the next steps