Abstract
The coordination of time-dependent simulation models is an important problem in environmental systems engineering. We propose a solution based on a rigorous formal modelling of the participating processes. Methodologically, our approach is driven by property processes which are used for the formal specification of the coordination problem. Property processes are supported by the CSP-like language FSP of Magee and Kramer which will be used throughout this paper for modelling the system requirements and the system design. The heart of our design model is a global time controller which coordinates distributed simulation models according to their local time scales. We will show with model checking techniques that all safety and liveness requirements are guaranteed by the timecontroller design.
The strong practical relevance of the approach is ensured by the fact that our strategy is used to produce a formally verified design for the kernel of the integrative simulation system DANUBIA developed within the GLOWA-Danube project.
This work is partially supported by the GLOWA-Danube project (07GWK04) sponsored by the German Federal Ministry of Education and Research.
Chapter PDF
References
Barth, M., Hennicker, R., Kraus, A., Ludwig, M.: DANUBIA: An Integrative Simulation System for Global Research in the Upper Danube Basin. Cybernetics and Systems 35(7-8), 639–666 (2004)
Barth, M., Knapp, A.: A Coordination Architecture for Time-Dependent Components. In: Proc. 22nd Int. Multi-Conf. Applied Informatics. Software Engineering (IASTED SE’04), pp. 6–11 (2004)
EESD (last visited 2005/03/17), http://www.cordis.lu/eesd
GLOWA (last visited 2005/03/17), http://www.glowa.org
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Holzmann, G.: The SPIN Model Checker – Primer and Reference Manual. Addison Wesley, Reading (2004)
LTSA (last visited 2005/03/17), http://www-dse.doc.ic.ac.uk/concurrency/
Ludwig, R., Mauser, W., Niemeyer, S., Colgan, A., Stolz, R., Escher-Vetter, H., Kuhn, M., Reichstein, M., Tenhunen, J., Kraus, A., Ludwig, M., Barth, M., Hennicker, R.: Web-based Modeling of Water, Energy and Matter Fluxes to Support Decision Making in Mesoscale Catchments - the Integrative Perspective of GLOWA-Danube. Physics and Chemistry of the Earth 28, 621–634 (2003)
Magee, J., Kramer, J.: Concurrency – State Models and Java Programs. John Wiley & Sons, Chichester (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 IFIP International Federation for Information Processing
About this paper
Cite this paper
Hennicker, R., Ludwig, M. (2005). Property-Driven Development of a Coordination Model for Distributed Simulations. In: Steffen, M., Zavattaro, G. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2005. Lecture Notes in Computer Science, vol 3535. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11494881_19
Download citation
DOI: https://doi.org/10.1007/11494881_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26181-0
Online ISBN: 978-3-540-31556-8
eBook Packages: Computer ScienceComputer Science (R0)