Simulation and Verification of Dynamic Systems

Summary

Simulation is widely used for modeling engineering artifacts and natural phenomena to gain insight into the operation of those systems. Simulation, using a simulator or otherwise experimenting with fictitious situation can show the eventual real effects of some possible conditions. In contrast, formal verification is concerned with proving or disproving the correctness of a system with respect to a certain property, using mathematical and logical methods. Verification techniques include explicit-state enumeration, symbolic simulation, model checking, static program analysis, and theorem proving techniques.

Despite of these different objectives, the fields of simulation and verification address similar research challenges. In particular, the need for identifying and defining suitable models of the dynamic system under study unifies both research fields. Modeling methods have a significant impact on how easily certain phenomena can be described, they influence the acceptance in the application community and the possibilities to be analyzed and simulated. They formed one focus of discussion and the basis for a working group exploring the potentials and limitations of different modeling approaches. Although there are disparate approaches in the fields of simulation and verification for validating timed, probabilistic, and hybrid systems, both fields address component-based and abstraction-based validation techniques. Refinement and abstraction plays a crucial role, both in simulation and verification, but even more so if both approaches are combined. The role of refinement and abstractions has been a second focus of general discussion intensified in a dedicated working group. In application areas like embedded systems and systems biology, researchers of simulation and verifi- cation are coming together to see a lot of common problems and interesting solutions that help propelling research in the respective areas. During the seminar, the application area of Systems Biology moved quickly into the focus of interest, which resulted in a working group addressing the question whether the application area of systems biology requires specific modeling, simulation, and verification tools, and how biological systems differ from engineered ones.

The dialog between the simulation and verification community about the abovementioned issues most notably started with the Computational Methods in Systems Biology Workshop series, the first of which took place in Trento in 2003. The Dagstuhl Seminar continued and intensified this dialog between both communities working on simulating and verifying dynamic systems.

Seminar

Dagstuhl is dedicated to working groups. In contrast to traditional conference settings, the schedule offered plenty of time for working groups, discussions, and spontaneous activities. To give an overview about the different areas, state-of-the-art plenary talks were given in the beginning of the seminar. Short presentations provided the opportunity for each participant to present and discuss his or her own work during the morning session. The afternoons were dedicated to working groups. The themes of the working groups formed during the first days of the seminar. In the evening, the results of the working groups were presented in plenary sessions.

Intertwining working groups and plenary sessions helped to work on concrete questions in the different groups and to support a cross fertilization among them. The seminar was a truly interdisciplinary event and all participants played an active role in driving the progress and content of the seminar and the individual working groups. Their results took shape in three documents that formed the basis of the included working groups’ report The challenge of combining simulation and verification. As always, Schloss Dagstuhl and its ambiance, its unusual blend of the old with the new, the organization, and the very helpful staff contributed largely to the success of the seminar.