Volume

Dagstuhl Seminar Proceedings, Volume 6161

Publication Details

  • published at: 2006-09-07
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Access Numbers

Documents

No documents found matching your filter selection.
Document
DOI: 10.4230/DagSemProc.06161.1
06161 Abstracts Collection – Simulation and Verification of Dynamic Systems

Authors: David M. Nicol, Corrado Priami, Hanne Riis-Nielson, and Adelinde M. Uhrmacher

Abstract
From 17.04.06 to 22.04.06, the Dagstuhl Seminar 06161 ``Simulation and Verification of Dynamic Systems'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

David M. Nicol, Corrado Priami, Hanne Riis-Nielson, and Adelinde M. Uhrmacher. 06161 Abstracts Collection – Simulation and Verification of Dynamic Systems. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{nicol_et_al:DagSemProc.06161.1,
  author =	{Nicol, David M. and Priami, Corrado and Riis-Nielson, Hanne and Uhrmacher, Adelinde M.},
  title =	{{06161 Abstracts Collection – Simulation and Verification of Dynamic Systems}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.1},
  URN =		{urn:nbn:de:0030-drops-7102},
  doi =		{10.4230/DagSemProc.06161.1},
  annote =	{Keywords: Modeling, Simulation, Verification, Dynamic Systems, Systemsbiology}
}
Document
DOI: 10.4230/DagSemProc.06161.2
06161 Executive Summary – Simulation and Verification of Dynamic Systems

Authors: Hanne Riis-Nielson, David M. Nicol, Corrado Priami, and Adelinde M. Uhrmacher

Abstract
Simulation is widely used for modeling engineering artifacts and natural phenomena to gain insight into the operation of those systems. Formal verification is concerned with proving or disproving the correctness of a system with respect to a certain property. Despite of these different objectives, the fields of simulation and verification address similar research challenges. Particularly, in the application area systems biology simulation and verification are moving together. The Dagstuhl Seminar was dedicated to intensifying this dialogue, and stimulating the exchange of ideas. Three working groups discussed questions: Why are biological systems difficult to model?, What role does refinement and abstraction play in combining simulation and verification?, What is the role of communication and composition in simulating and analysing dynamic systems? The results of the working groups can be found in the working groups' report.
Cite as

Hanne Riis-Nielson, David M. Nicol, Corrado Priami, and Adelinde M. Uhrmacher. 06161 Executive Summary – Simulation and Verification of Dynamic Systems. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{riisnielson_et_al:DagSemProc.06161.2,
  author =	{Riis-Nielson, Hanne and Nicol, David M. and Priami, Corrado and Uhrmacher, Adelinde M.},
  title =	{{06161 Executive Summary – Simulation and Verification of Dynamic Systems}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.2},
  URN =		{urn:nbn:de:0030-drops-7028},
  doi =		{10.4230/DagSemProc.06161.2},
  annote =	{Keywords: Modelling, Simulation, Verification, Systemsbiology}
}
Document
DOI: 10.4230/DagSemProc.06161.3
06161 Working Groups' Report: The Challlenge of Combining Simulation and Verification

Authors: Gregory Batt, Jeremy T. Bradley, Roland Ewald, François Fages, Holger Hermans, Jane Hillston, Peter Kemper, Alke Martens, Pieter Mosterman, Flemming Nielson, Oleg Sokolsky, and Adelinde M. Uhrmacher

Abstract
Simulation has found widespread use for experimentation and exploration of the possible impacts of a variety of conditions on a system. 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.
Cite as

Gregory Batt, Jeremy T. Bradley, Roland Ewald, François Fages, Holger Hermans, Jane Hillston, Peter Kemper, Alke Martens, Pieter Mosterman, Flemming Nielson, Oleg Sokolsky, and Adelinde M. Uhrmacher. 06161 Working Groups' Report: The Challlenge of Combining Simulation and Verification. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{batt_et_al:DagSemProc.06161.3,
  author =	{Batt, Gregory and Bradley, Jeremy T. and Ewald, Roland and Fages, Fran\c{c}ois and Hermans, Holger and Hillston, Jane and Kemper, Peter and Martens, Alke and Mosterman, Pieter and Nielson, Flemming and Sokolsky, Oleg and Uhrmacher, Adelinde M.},
  title =	{{06161 Working Groups' Report: The Challlenge of Combining Simulation and Verification}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--21},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.3},
  URN =		{urn:nbn:de:0030-drops-7249},
  doi =		{10.4230/DagSemProc.06161.3},
  annote =	{Keywords: Modelling, Simulation, Verification, Systemsbiology}
}
Document
DOI: 10.4230/DagSemProc.06161.4
A Petri Net Approach to Verify and Debug Simulation Models

Authors: Peter Kemper and Carsten Tepper

Abstract
Verification and Simulation share many issues, one is that simulation models require validation and verification. In the context of simulation, verification is understood as the task to ensure that an executable simulation model matches its conceptual counterpart while validation is the task to ensure that a simulation model represents the system under study well enough with respect to the goals of the simulation study. Both, validation and verification, are treated in the literature at a rather high level and seem to be more an art than engineering. This paper considers discrete event simulation of stochastic models that are formulated in a process-oriented language. The ProC/B paradigm is used as a particular example of a class of simulation languages which follow the common process interaction approach and show common concepts used in performance modeling, namely a) layered systems of virtual machines that contain resources and provide services and b) concurrent processes that interact by message passing and shared memory. We describe how Petri net analysis techniques help to verify and debug a large and detailed simulation model of airport logistics. We automatically derive a Petri net that models the control flow of a Proc/B model and we make use of invariant analysis and modelchecking to shed light on the allocation of resources, constraints among entities and causes for deadlocks.
Cite as

Peter Kemper and Carsten Tepper. A Petri Net Approach to Verify and Debug Simulation Models. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kemper_et_al:DagSemProc.06161.4,
  author =	{Kemper, Peter and Tepper, Carsten},
  title =	{{A Petri Net Approach to Verify and Debug Simulation Models}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.4},
  URN =		{urn:nbn:de:0030-drops-7084},
  doi =		{10.4230/DagSemProc.06161.4},
  annote =	{Keywords: Discrete event simulation, verification, debugging, process interaction, Petri net analysis}
}
Document
DOI: 10.4230/DagSemProc.06161.5
Abstract Interpretation of Graph Transformation

Authors: Jörg Bauer and Reinhard Wilhelm

Abstract
The semantics of many dynamic systems can be described by evolving graphs. Graph transformation systems (GTS) are a natural, intuitive, and formally defined method to specify systems of evolving graphs, whereas verification techniques for GTS are scarce. We present an abstract interpretation based approach for GTS verification. Single graphs are abstracted in two steps. First similar nodes within a connected component, then similar abstracted connected components are summarized. Transformation rules are applied directly to abstract graphs yielding a bounded set of abstract graphs of bounded size that over-approximates the concrete GTS and can be used for further verification. Since our abstraction is homomorphic, existential positive properties are preserved under abstraction. Furthermore, we identify automatically checkable completeness criteria for the abstraction. The technique is implemented and successfully tested on the platoon case study.
Cite as

Jörg Bauer and Reinhard Wilhelm. Abstract Interpretation of Graph Transformation. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:DagSemProc.06161.5,
  author =	{Bauer, J\"{o}rg and Wilhelm, Reinhard},
  title =	{{Abstract Interpretation of Graph Transformation}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.5},
  URN =		{urn:nbn:de:0030-drops-7039},
  doi =		{10.4230/DagSemProc.06161.5},
  annote =	{Keywords: Abstract Interpretation, Graph Transformation}
}
Document
DOI: 10.4230/DagSemProc.06161.6
Context Dependent Analysis of BioAmbients

Authors: Henrik Pilegaard, Hanne Riis-Nielson, and Flemming Nielson

Abstract
BioAmbients is a derivative of mobile ambients that has shown promise of describing interesting features of the behaviour of biological systems. The technical contribution of this paper is to extend the Flow Logic approach to static analysis with a couple of new techniques in order to give precise information about the behaviour of systems written in BioAmbients. Applying the development to a simple model of a cell releasing nutrients from food compunds we illustrate how the proposed analysis does indeed improve on previous efforts.
Cite as

Henrik Pilegaard, Hanne Riis-Nielson, and Flemming Nielson. Context Dependent Analysis of BioAmbients. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{pilegaard_et_al:DagSemProc.06161.6,
  author =	{Pilegaard, Henrik and Riis-Nielson, Hanne and Nielson, Flemming},
  title =	{{Context Dependent Analysis of BioAmbients}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.6},
  URN =		{urn:nbn:de:0030-drops-7093},
  doi =		{10.4230/DagSemProc.06161.6},
  annote =	{Keywords: Static analysis, abstract interpretation, BioAmbients}
}
Document
DOI: 10.4230/DagSemProc.06161.7
Modeling and Simulating Biological Processes with Stochastic Multiset Rewriting

Authors: Matteo Cavaliere and Sean Sedwards

Abstract
Membrane systems were originally introduced as models of computation inspired by the structure and the functioning of living cells. More recently, membrane systems have been shown to be suitable also to model cellular processes. Inspired by brane calculi, a new model of membrane system with peripheral proteins has been recently introduced. Such model has compartments (enclosed by membranes), floating objects, and objects attached to the internal and external surfaces of the membranes. The objects can be processed/transported inside/across the compartments and the transport is regulated by opportune objects attached to the membranes surfaces. We present a stochastic simulator of this model, with a style of syntax based on chemical reactions. We show that the simulator can be particularly useful in modelling biological processes that involve compartments, surface and integral membrane proteins, transport and processing of chemical substances. As examples we present the simulation of circadian clock and the G-protein cycle in yeast.
Cite as

Matteo Cavaliere and Sean Sedwards. Modeling and Simulating Biological Processes with Stochastic Multiset Rewriting. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{cavaliere_et_al:DagSemProc.06161.7,
  author =	{Cavaliere, Matteo and Sedwards, Sean},
  title =	{{Modeling and Simulating Biological Processes with Stochastic Multiset Rewriting}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.7},
  URN =		{urn:nbn:de:0030-drops-7061},
  doi =		{10.4230/DagSemProc.06161.7},
  annote =	{Keywords: Systems biology, membrane systems, formal language, simulation}
}
Document
DOI: 10.4230/DagSemProc.06161.8
Population models from PEPA descriptions

Authors: Jane Hillston

Abstract
Stochastic process algebras such as PEPA have enjoyed considerable success as CTMC-based system description languages for performance evaluation of computer and communication systems. However they have not been able to escape the problem of state space explosion, and this problem is exacerbated when other domains such as systems biology are considered. Therefore we have been investigating alternative semantics for PEPA models which give rise to a population view of the system, in terms of a set of nonlinear ordinary differential equations. This extended abstract gives an overview of this mapping.
Cite as

Jane Hillston. Population models from PEPA descriptions. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{hillston:DagSemProc.06161.8,
  author =	{Hillston, Jane},
  title =	{{Population models from PEPA descriptions}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.8},
  URN =		{urn:nbn:de:0030-drops-7071},
  doi =		{10.4230/DagSemProc.06161.8},
  annote =	{Keywords: Stochastic Process Algebra, Fluid Approximation, Discrete vs Continuous models}
}
Document
DOI: 10.4230/DagSemProc.06161.9
Static Analysis of a Model of the LDL Degradation Pathway

Authors: Henrik Pilegaard, Hanne Riis-Nielson, and Flemming Nielson

Abstract
BioAmbients is a derivative of mobile ambients that has shown promise of describing interesting features of the behaviour of biological systems. As for other ambient calculi static program analysis can be used to compute safe approximations of the behaviour of system models. We use these tools to model and analyse the production of cholesterol in living cells and show that we are able to pinpoint the difference in behaviour between models of healthy systems and models of mutated systems giving rise to known diseases.
Cite as

Henrik Pilegaard, Hanne Riis-Nielson, and Flemming Nielson. Static Analysis of a Model of the LDL Degradation Pathway. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{pilegaard_et_al:DagSemProc.06161.9,
  author =	{Pilegaard, Henrik and Riis-Nielson, Hanne and Nielson, Flemming},
  title =	{{Static Analysis of a Model of the LDL Degradation Pathway}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.9},
  URN =		{urn:nbn:de:0030-drops-7230},
  doi =		{10.4230/DagSemProc.06161.9},
  annote =	{Keywords: Static analysis, Systems Biology, BioAmbients, LDL Degradation Pathway}
}
Document
DOI: 10.4230/DagSemProc.06161.10
Stochastic Process Algebra Models of a Circadian Clock

Authors: Jeremy T. Bradley and Thomas Thorne

Abstract
We present stochastic process algebra models of a Circadian clock mechanism used in many biological organisms to regulate time-based behaviour. We compare modelling techniques from different modelling paradigms, PEPA and stochastic $pi$-calculus.
Cite as

Jeremy T. Bradley and Thomas Thorne. Stochastic Process Algebra Models of a Circadian Clock. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bradley_et_al:DagSemProc.06161.10,
  author =	{Bradley, Jeremy T. and Thorne, Thomas},
  title =	{{Stochastic Process Algebra Models of a Circadian Clock}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.10},
  URN =		{urn:nbn:de:0030-drops-7050},
  doi =		{10.4230/DagSemProc.06161.10},
  annote =	{Keywords: Stochastic process algebras, ODEs, Circadian clock}
}

Filters

  • Authors
  • B
  • Batt, Gregory
  • Bauer, Jörg
  • Bradley, Jeremy T.
  • C
  • Cavaliere, Matteo
  • E
  • Ewald, Roland
  • F
  • Fages, François
  • H
  • Hermans, Holger
  • Hillston, Jane
  • K
  • Kemper, Peter
  • M
  • Martens, Alke
  • Mosterman, Pieter
  • N
  • Nicol, David M.
  • Nielson, Flemming
  • P
  • Pilegaard, Henrik
  • Priami, Corrado
  • R
  • Riis-Nielson, Hanne
  • S
  • Sedwards, Sean
  • Sokolsky, Oleg
  • T
  • Tepper, Carsten
  • Thorne, Thomas
  • U
  • Uhrmacher, Adelinde M.
  • W
  • Wilhelm, Reinhard

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact