19 Search Results for "Priami, Corrado"

Document
DOI: 10.4230/DagRep.1.4.41
Formal Methods in Molecular Biology (Dagstuhl Seminar 11151)

Authors: Rainer Breitling, Adelinde M. Uhrmacher, Frank J. Bruggeman, and Corrado Priami

Published in: Dagstuhl Reports, Volume 1, Issue 4 (2011)

Abstract
This report documents the program and the outcomes of the Seminar 11151 `Formal Methods in Molecular Biology' that took place in Dagstuhl, Germany, on 10--15 Apr 2011. The most recent advances in Systems Biology were discussed, as well as and the contribution of computational formalisms to the modeling of biological systems, with the focus on stochasticity. About 30 talks were given. The participants formed 5 teams that worked on selected case studies. Two teams were awarded prizes, for their efforts in analyzing and further elucidating published biological models.
Cite as

Rainer Breitling, Adelinde M. Uhrmacher, Frank J. Bruggeman, and Corrado Priami. Formal Methods in Molecular Biology (Dagstuhl Seminar 11151). In Dagstuhl Reports, Volume 1, Issue 4, pp. 41-64, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{breitling_et_al:DagRep.1.4.41,
  author =	{Breitling, Rainer and Uhrmacher, Adelinde M. and Bruggeman, Frank J. and Priami, Corrado},
  title =	{{Formal Methods in Molecular Biology (Dagstuhl Seminar 11151)}},
  pages =	{41--64},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2011},
  volume =	{1},
  number =	{4},
  editor =	{Breitling, Rainer and Uhrmacher, Adelinde M. and Bruggeman, Frank J. and Priami, Corrado},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.4.41},
  URN =		{urn:nbn:de:0030-drops-31975},
  doi =		{10.4230/DagRep.1.4.41},
  annote =	{Keywords: Bioinformatics, systems biology, formal modeling, computational biology, stochastic, model, simulation, checking, verification, abstraction, petri nets, process algebra}
}
Document
DOI: 10.4230/DagSemProc.09091.1
09091 Abstracts Collection – Formal Methods in Molecular Biology

Authors: Rainer Breitling, David Roger Gilbert, Monika Heiner, and Corrado Priami

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)

Abstract
From 23. February to 27. February 2009, the Dagstuhl Seminar 09091 ``Formal Methods in Molecular Biology '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. 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

Rainer Breitling, David Roger Gilbert, Monika Heiner, and Corrado Priami. 09091 Abstracts Collection – Formal Methods in Molecular Biology. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, pp. 1-24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{breitling_et_al:DagSemProc.09091.1,
  author =	{Breitling, Rainer and Gilbert, David Roger and Heiner, Monika and Priami, Corrado},
  title =	{{09091 Abstracts Collection – Formal Methods in Molecular Biology }},
  booktitle =	{Formal Methods in Molecular Biology},
  pages =	{1--24},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.1},
  URN =		{urn:nbn:de:0030-drops-19972},
  doi =		{10.4230/DagSemProc.09091.1},
  annote =	{Keywords: Formal models, systems biology, biological processes}
}
Document
DOI: 10.4230/DagSemProc.09091.2
09091 Executive Summary – Formal Methods in Molecular Biology

Authors: Rainer Breitling, David Roger Gilbert, Monika Heiner, and Corrado Priami

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)

Abstract
Formal logical models play an increasing role in the newly emerging field of Systems Biology. Compared to the classical, well-established approach of modeling biological processes using continuous and stochastic differential equations, formal logical models offer a number of important advantages. Many different formal modeling paradigms have been applied to molecular biology, each with its own community, formalisms and tools. In this seminar we brought together modelers from various backgrounds to stimulate closer interaction within the field and to create a common platform for discussion. A central feature of the seminar was a modeling competition (with a highly collaborative flavor) of various modeling paradigms.
Cite as

Rainer Breitling, David Roger Gilbert, Monika Heiner, and Corrado Priami. 09091 Executive Summary – Formal Methods in Molecular Biology. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{breitling_et_al:DagSemProc.09091.2,
  author =	{Breitling, Rainer and Gilbert, David Roger and Heiner, Monika and Priami, Corrado},
  title =	{{09091 Executive Summary – Formal Methods in Molecular Biology}},
  booktitle =	{Formal Methods in Molecular Biology},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.2},
  URN =		{urn:nbn:de:0030-drops-19964},
  doi =		{10.4230/DagSemProc.09091.2},
  annote =	{Keywords: Formal models, systems biology, biological processes.}
}
Document
DOI: 10.4230/DagSemProc.09091.3
Analyzing various models of Circadian Clock and Cell Cycle coupling

Authors: Attila Csikász-Nagy, Adrien Faure, Roberto Larcher, Paola Lecca, Ivan Mura, Ferenc Jordan, Alida Palmisano, Alessandro Romanel, Sean Sedwards, Heike Siebert, Sylvain Soliman, Denis Thieffry, Judit Zámborszky, Tommaso Mazza, and Paolo Ballarini

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)

Abstract
The daily rhythm can influence the proliferation rate of many cell types. In the mammalian system the transcription of the cell cycle regulatory protein Wee1 is controlled by the circadian clock. Zamborszky et al. (2007) present a computational model coupling the cell cycle and circadian rhythm, showing that this coupling can lead to multimodal cell cycle time distributions. Biological data points to additional couplings, including a link back from the cell cycle to the circadian clock. Proper modelling of this coupling requires a more detailed description of both parts of the model. Hence, we aim at further extending and analysing earlier models using a combination of modelling techniques and computer software, including CoSBI lab, BIOCHAM, and GINsim.
Cite as

Attila Csikász-Nagy, Adrien Faure, Roberto Larcher, Paola Lecca, Ivan Mura, Ferenc Jordan, Alida Palmisano, Alessandro Romanel, Sean Sedwards, Heike Siebert, Sylvain Soliman, Denis Thieffry, Judit Zámborszky, Tommaso Mazza, and Paolo Ballarini. Analyzing various models of Circadian Clock and Cell Cycle coupling. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, pp. 1-6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{csikasznagy_et_al:DagSemProc.09091.3,
  author =	{Csik\'{a}sz-Nagy, Attila and Faure, Adrien and Larcher, Roberto and Lecca, Paola and Mura, Ivan and Jordan, Ferenc and Palmisano, Alida and Romanel, Alessandro and Sedwards, Sean and Siebert, Heike and Soliman, Sylvain and Thieffry, Denis and Z\'{a}mborszky, Judit and Mazza, Tommaso and Ballarini, Paolo},
  title =	{{Analyzing various models of Circadian Clock and Cell Cycle coupling}},
  booktitle =	{Formal Methods in Molecular Biology},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.3},
  URN =		{urn:nbn:de:0030-drops-19944},
  doi =		{10.4230/DagSemProc.09091.3},
  annote =	{Keywords: Cell cycle, circadian clock, computational modelling}
}
Document
DOI: 10.4230/DagSemProc.09091.4
BioModel Engineering: Its role in Systems Biology and Synthetic Biology

Authors: David Roger Gilbert, Rainer Breitling, and Monika Heiner

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)

Abstract
BioModel Engineering takes place at the interface of computing science, mathematics, engineering and biology, and provides a systematic approach for designing, constructing and analyzing computational models of biological systems. Some of its central concepts are inspired by efficient software engineering strategies. BioModel Engineering does not aim at engineering biological systems per se, but rather aims at describing their structure and behavior, in particular at the level of intracellular molecular processes, using computational tools and techniques in a principled way. The two major application areas of BioModel Engineering are systems biology and synthetic biology. In the former, the aim is the design and construction of models of existing biological systems, which explain observed properties and predict the response to experimental interventions; in the latter, BioModel Engineering is used as part of a general strategy for designing and constructing synthetic biological systems with novel functionalities. The overall steps in building computational models in a BioModel Engineering framework are: Problem Identification, Model Construction, Static and Dynamic Analysis, Simulation, and Model management and development. A major theme in BioModel Engineering is that of constructing a (qualitative) model means (1) finding the structure, (2) obtaining an initial state and (3) parameter fitting. In an approach that we have taken, the structure is obtained by piecewise construction of models from modular parts, the initial state which describes concentrations of species or numbers of molecules is obtained by analysis of the structure, and parameter fitting comprises determining the rate parameters of the kinetic equations by reference to trusted data. Model checking can play a key role in BioModel Engineering – for example in recent work we have shown how parameter estimation can be achieved by characterising the desired behaviour of a model with a temporal logic property and altering the model to make it conform to the property as determined through model checking.
Cite as

David Roger Gilbert, Rainer Breitling, and Monika Heiner. BioModel Engineering: Its role in Systems Biology and Synthetic Biology. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, pp. 1-2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{gilbert_et_al:DagSemProc.09091.4,
  author =	{Gilbert, David Roger and Breitling, Rainer and Heiner, Monika},
  title =	{{BioModel Engineering: Its role in Systems Biology and Synthetic Biology}},
  booktitle =	{Formal Methods in Molecular Biology},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.4},
  URN =		{urn:nbn:de:0030-drops-19929},
  doi =		{10.4230/DagSemProc.09091.4},
  annote =	{Keywords: Biochemical systems, models, design, construction, systems biology, synthetic biology, model checking.}
}
Document
DOI: 10.4230/DagSemProc.09091.5
Modelling and analysis of the NF-$kappa$B pathway in Bio-PEPA

Authors: Federica Ciocchetta, Andrea Degasperi, John Heath, and Jane Hillston

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)

Abstract
In this work we present a Bio-PEPA model describing the Nuclear Factor $kappa$B (NF-$kappa$B) signalling pathway. In particular our model focuses on the dynamic response of NF-$kappa$B to an external stimulus. Each biochemical species in the pathway is represented by a specific Bio-PEPA component and the external stimulus is abstracted by Bio-PEPA events. The Bio-PEPA model is a formal intermediate representation of the pathway on which various kinds of analysis can be performed. Both stochastic and deterministic simulations are carried out to validate our model against the experimental data in the literature and to verify some properties, such as the impact of the stimulus duration and of the NF-$kappa$B initial amount on the behaviour of some species. Finally, sensitivity analysis is considered to investigate the most influential parameters of the model.
Cite as

Federica Ciocchetta, Andrea Degasperi, John Heath, and Jane Hillston. Modelling and analysis of the NF-$kappa$B pathway in Bio-PEPA. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, pp. 1-18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{ciocchetta_et_al:DagSemProc.09091.5,
  author =	{Ciocchetta, Federica and Degasperi, Andrea and Heath, John and Hillston, Jane},
  title =	{{Modelling and analysis of the NF-\$kappa\$B pathway in Bio-PEPA}},
  booktitle =	{Formal Methods in Molecular Biology},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.5},
  URN =		{urn:nbn:de:0030-drops-19911},
  doi =		{10.4230/DagSemProc.09091.5},
  annote =	{Keywords: Process algebras, NF-\$kappa\$B pathway, modelling, analysis}
}
Document
DOI: 10.4230/DagSemProc.09091.6
Rule-based Modeling of Transcriptional Attenuation at the Tryptophan Operon

Authors: Céline Kuttler, Cédric Lhoussaine, and Mirabelle Nebut

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)

Abstract
Transcriptional attenuation at E.coli's tryptophan operon is a prime example of RNA-mediated gene regulation. In this paper, we present a discrete stochastic model for this phenomenon based on chemical reactions. Our model is compact and intelligible, due to n-ary reactions (which preclude object-centric approaches) and to rule schemas that define finite sets of chemical reactions. Stochastic simulations with our model confirm results that were previously obtained by master equations or differential equations. In addition, our approach permits to reflect mutation experiments by simple model modifications, and to re-use model components for transcriptional attenuation in other genes and organisms.
Cite as

Céline Kuttler, Cédric Lhoussaine, and Mirabelle Nebut. Rule-based Modeling of Transcriptional Attenuation at the Tryptophan Operon. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, pp. 1-22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{kuttler_et_al:DagSemProc.09091.6,
  author =	{Kuttler, C\'{e}line and Lhoussaine, C\'{e}dric and Nebut, Mirabelle},
  title =	{{Rule-based Modeling of Transcriptional Attenuation at the Tryptophan Operon}},
  booktitle =	{Formal Methods in Molecular Biology},
  pages =	{1--22},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.6},
  URN =		{urn:nbn:de:0030-drops-19938},
  doi =		{10.4230/DagSemProc.09091.6},
  annote =	{Keywords: Systems biology, rule-based modeling languages, stochastic simulation, kappa.}
}
Document
DOI: 10.4230/DagSemProc.09091.7
Stochastic modelling of cellular growth and division by means of the pi@ calculus

Authors: Cristian Versari

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)

Abstract
The application of Concurrency Theory to Systems Biology is in its earliest stage of progress. The metaphor of cells as computing systems by Regev and Shapiro opened the employment of concurrent languages for the modelling of biological systems. Their peculiar characteristics led to the design of many bio-inspired formalisms which achieve higher faithfulness and specificity. In this paper we discuss the application to the biological modelling of pi@, a core calculus for the representation of biological systems. The pi@ language represents a keystone in this respect, thanks to its expressiveness capabilities which allow the modelling of a wide variety of phenomena (e.g. simple chemical reactions, but also formation of molecular or protein complexes, organisation of complex system in dynamical compartment hierarchies) despite of its simplicity and conservativeness. Here we analyse a biological case study involving cellular growth and division, modelled in the stochastic variant of pi@: the case study is formalised and stochastically simulated according to a multi-compartment extension of Gillespie's stochastic simulation algorithm. The results underline the usefulness of the modelling approach adopted in pi@ for the correct handling of systems with variable volume.
Cite as

Cristian Versari. Stochastic modelling of cellular growth and division by means of the pi@ calculus. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, pp. 1-15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{versari:DagSemProc.09091.7,
  author =	{Versari, Cristian},
  title =	{{Stochastic modelling of cellular growth and division by means of the pi@ calculus}},
  booktitle =	{Formal Methods in Molecular Biology},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.7},
  URN =		{urn:nbn:de:0030-drops-19907},
  doi =		{10.4230/DagSemProc.09091.7},
  annote =	{Keywords: Process algebra, pi-calculus, simulation, stochastic}
}
Document
DOI: 10.4230/DagSemProc.09091.8
Symbolic Steady States and Dynamically Essential Subnetworks of Discrete Regulatory Networks

Authors: Heike Siebert

Published in: Dagstuhl Seminar Proceedings, Volume 9091, Formal Methods in Molecular Biology (2009)

Abstract
Analyzing complex networks is a difficult task, regardless of the chosen modeling framework. For a discrete regulatory network, even if the number of components is in some sense manageable, we have to deal with the problem of analyzing the dynamics in an exponentially large state space. A well known idea to approach this difficulty is to identify smaller building blocks of the system the study of which in isolation still renders information on the dynamics of the whole network. In this talk, we introduce the notion of symbolic steady state which allows us to identify such building blocks. We state explicit rules how to derive attractors of the network from subnetwork attractors valid for synchronous as well as asynchronous dynamics. Illustrating those rules, we derive general conditions for circuits embedded in the network to transfer their behavioral characteristics pertaining number and size of attractors observed in isolation to the complex network.
Cite as

Heike Siebert. Symbolic Steady States and Dynamically Essential Subnetworks of Discrete Regulatory Networks. In Formal Methods in Molecular Biology. Dagstuhl Seminar Proceedings, Volume 9091, pp. 1-3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{siebert:DagSemProc.09091.8,
  author =	{Siebert, Heike},
  title =	{{Symbolic Steady  States and Dynamically Essential Subnetworks of Discrete Regulatory Networks}},
  booktitle =	{Formal Methods in Molecular Biology},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9091},
  editor =	{Rainer Breitling and David Roger Gilbert and Monika Heiner and Corrado Priami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09091.8},
  URN =		{urn:nbn:de:0030-drops-19957},
  doi =		{10.4230/DagSemProc.09091.8},
  annote =	{Keywords: Discrete networks, logical analysis, symbolic steady states}
}
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

Published in: Dagstuhl Seminar Proceedings, Volume 6161, Simulation and Verification of Dynamic Systems (2006)

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.6
Context Dependent Analysis of BioAmbients

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

Published in: Dagstuhl Seminar Proceedings, Volume 6161, Simulation and Verification of Dynamic Systems (2006)

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.2
06161 Executive Summary – Simulation and Verification of Dynamic Systems

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

Published in: Dagstuhl Seminar Proceedings, Volume 6161, Simulation and Verification of Dynamic Systems (2006)

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

Published in: Dagstuhl Seminar Proceedings, Volume 6161, Simulation and Verification of Dynamic Systems (2006)

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

Published in: Dagstuhl Seminar Proceedings, Volume 6161, Simulation and Verification of Dynamic Systems (2006)

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

Published in: Dagstuhl Seminar Proceedings, Volume 6161, Simulation and Verification of Dynamic Systems (2006)

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}
}
  • Refine by Author
  • 5 Priami, Corrado
  • 4 Breitling, Rainer
  • 4 Riis-Nielson, Hanne
  • 4 Uhrmacher, Adelinde M.
  • 3 Gilbert, David Roger
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 4 systems biology
  • 3 Simulation
  • 3 Systemsbiology
  • 3 Verification
  • 3 simulation
  • Show More...

  • Refine by Type
  • 19 document

  • Refine by Publication Year
  • 10 2006
  • 8 2009
  • 1 2011

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact