abstract: We report on a case study in synthetic biology,
demonstrating the model-driven design of a self-powering
electrochemical biosensor. An essential result of the design process is
a general template of a biosensor, which can be instantiated to be
adapted to specific pollutants. This template represents a gene
expression network extended by metabolic activity. We illustrate the
model-based analysis of this template using qualitative, stochastic and
continuous Petri nets and related analysis techniques, contributing to
a reliable and robust design.
abstract: We give a description of a Petri net-based
framework for modelling and analysing biochemical pathways, which
unifies the qualitative, stochastic and continuous paradigms.
Each perspective adds its contribution to the understanding of the
system, thus the three approaches do not compete, but complement each
other. We illustrate our approach by applying it to an extended model
of the three stage cascade, which forms the core of the ERK signal
transduction pathway. Consequently our focus is on transient behaviour
analysis.
We demonstrate how qualitative descriptions are abstractions over
stochastic or continuous descriptions, and show that the stochastic and
continuous models approximate each other.
Although our framework is based on Petri nets, it can be applied more
widely to other formalisms which are used to model and analyse
biochemical networks.
abstract: Quantitative models of biochemical networks (signal
transduction cascades, metabolic pathways, gene regulatory circuits)
are a central component of modern systems biology. Building and
managing these complex models is a major challenge that can benefit
from the application of formal methods adopted from theoretical
computing science. Here we provide a general introduction to the field
of formal modelling, which emphasizes the intuitive biochemical basis
of the modelling process, but is also accessible for an audience with a
background in computing science and/or model engineering.
We show how signal transduction cascades can be modelled in a modular
fashion, using both a qualitative approach -- Qualitative Petri nets,
and quantitative approaches -- Continuous Petri Nets and Ordinary
Differential Equations. We review the major elementary building
blocks of a cellular signalling model, discuss which critical design
decisions have to be made during model building, and present a number
of novel computational tools that can help to explore alternative
modular models in an easy and intuitive manner. These tools, which are
based on Petri net theory, offer convenient ways of composing
hierarchical ODE models, and permit a qualitative analysis of their
behaviour.
We illustrate the central concepts using signal transduction as our
main example. The ultimate aim is to introduce a general approach that
provides the foundations for a structured formal engineering of
large-scale models of biochemical networks.
abstract: We sketch the fundamental properties and
features of Snoopy, a tool to model and execute (animate, simulate)
hierarchical graph-based system descriptions.
The tool comes along with several pre-fabricated graph classes,
especially some kind of Petri nets and other related graphs, and
facilitates a comfortable integration of further graph classes due to
its generic design.
To support an aspect-oriented model engineering, different graph
classes may be used simultaneously. Snoopy provides some features
(hierarchical nodes, logical nodes), which are particularly useful for
larger models, or models with an higher connectivity degree. There are
several Petri net classes available, among them the purely qualitative
place/transition nets in its standard definition and in a version
enhanced by four special arcs as well as two quantitative extensions of
it - stochastic Petri nets and continuous Petri nets. Each of these
classes enjoys dedicated animation or simulation features.
Our tool runs on Windows and Linux operating systems, and it is
available free of charge for non-commercial use.
abstract: We give a description
of a Petri net-based
framework for modelling and analysing biochemical pathways, which
unifies the qualitative, stochastic and continuous worlds. Each
perspective adds its contribution to the understanding of the system,
thus the three approaches do not compete, but complement each other. We
illustrate our approach by applying it to an extended model of the
three stage cascade, which forms the core of the ERK signal
transduction pathway. Consequently our focus is on transient behaviour
analysis. We demonstrate how qualitative descriptions are abstractions
over stochastic or continuous descriptions, and show that the
stochastic and continuous models approximate each other. A key
contribution of the paper consists in a precise definition of
biochemically interpreted stochastic Petri nets. Although our framework
is based on Petri nets, it can be applied more widely to other
formalisms which are used to model and analyse biochemical networks.
abstract: We apply Petri net theory to model and analyse
signal transduction pathways first qualitatively before continuing with
quantitative analyses. This paper demonstrates how to build
systematically a discrete model, which reflects provably the
qualitative biological behaviour without any knowledge of kinetic
parameters. The mating pheromone response pathway in Saccharomyces
cerevisiae serves as case study. Results: We propose an approach for
model validation of signal transduction pathways, based on the network
structure only. For this purpose, we introduce the new notion of
feasible t-invariants, which represent minimal self-contained subnets
being active under a given input situation. Each of these subnets
stands for a signal flow in the system. We define maximal common
transition sets (MCT-sets), which can be used for t-invariant
examination and net decomposition into smallest biologically meaningful
functional units.
abstract: We report on the results of an investigation into the integration of Petri nets and ordinary differential equations (ODEs) for the modelling and analysis of biochemical networks, and the application of our approach to the model of the influence of the Raf Kinase Inhibitor Protein (RKIP) on the Extracellular signal Regulated Kinase (ERK) signalling pathway. We show that analysis based on a discrete Petri net model of the system can be used to derive the sets of initial concentrations required by the corresponding continuous ordinary differential equation model, and no other initial concentrations produce meaningful steady states. Altogether, this paper represents a tutorial in step-wise modelling and analysis of larger models as well as in structured design of ODEs.
abstract:Biochemical networks are modelled at different abstraction levels. Basically, qualitative and quantitative models can be distinguished, which are typically treated as separate ones. In this paper, we bridge the gap between qualitative and quantitative models and apply time Petri nets for modelling and analysis of molecular biological systems. We demonstrate how to develop quantitative models of biochemical networks in a systematic manner, starting from the underlying qualitative ones. For this purpose we exploit the well-established structural Petri net analysis technique of transition invariants, which may be interpreted as a characterisation of the system’s steady state behaviour. For the analysis of the derived quantitative model, given as time Petri net, we present structural techniques to decide the time-dependent realisability of a transition sequence and to calculate its shortest and longest time length. All steps of the demonstrated approach consider systems of integer linear inequalities. The crucial point is the total avoidance of any state space construction. Therefore, the presented technology may be applied also to infinite systems, i.e. unbounded Petri nets.
Koch, I.; Junker, B. H.; Heiner, M.:abstract: Because of the complexity of metabolic networks and their regulation, formal modelling is a useful method to improve the understanding of these systems. An essential step in network modelling is to validate the network model. Petri net theory provides algorithms and methods, which can be applied directly to metabolic network modelling and analysis in order to validate the model. The metabolism between sucrose and starch in the potato tuber is of great research interest. Even if the metabolism is one of the best studied in sink organs, it is not yet fully understood. We provide an approach for model validation of metabolic networks using Petri net theory, which we demonstrate for the sucrose breakdown pathway in the potato tuber. We start with hierarchical modelling of the metabolic network as a Petri net and continue with the analysis of qualitative properties of the network. The results characterise the net structure and give insights into the complex net behaviour.
abstract: To understand biochemical processes caused by, e. g., mutations or deletions in the genome, the knowledge of possible alternative paths between two arbitrary chemical compounds is of increasing interest for biotechnology, pharmacology, medicine, and drug design. With the steadily increasing amount of data from high-throughput experiments new biochemical networks can be constructed and existing ones can be extended, which results in many large metabolic, signal transduction, and gene regulatory networks. The search for alternative paths within these complex and large networks can provide a huge amount of solutions, which can not be handled manually. Moreover, not all of the alternative paths are generally of interest. Therefore, we have developed and implemented a method, which allows us to define constraints to reduce the set of all structurally possible paths to the truly interesting path set. The paper describes the search algorithm and the constraints definition language. We give examples for path searches using this dedicated special language for a Petri net model of the sucrose-to-starch breakdown in the potato tuber.
Runge, T.:abstract: Computer aided analysis is necessary to improve the understanding of the complex biochemical processes. The often used kinetic models in biochemistry are based on differential equations. The results of such a kinetic model are often non-reliable on account of unreliable data or of inconsistencies in the used model. Therefore, other supplementary methods are indispensable. A detailed qualitative analysis should be done, before a quantitative (kinetic) analysis is made. This paper extends and refines the construction strategy of a coloured Petri net model of a metabolic network at a steady state, previously introduced in [11]. In a steady state the internal compounds’ concentrations are constant and therefore bounded. Each chemical reaction is typically active at steady state. Therefore, its naturally to demand a bounded and live model. A systematic procedure, exploiting the place transition nets’ T-invariants to construct an behavioural equivalent bounded and live coloured net, is presented. The application of P-invariant or model checking analysis techniques of such a model results in usable information, which are helpful for model validation.
Koch, I.; Heiner, M.:abstract: This paper describes
the thriving application
of Petri net theory for model validation of different types of
molecular biological systems. After a short introduction into systems
biology we demonstrate how to develop and validate qualitative models
of biological pathways in a systematic manner using the
well-established Petri net analysis technique of place and transition
invariants. We discuss special properties, which are characteristic
ones for biological pathways, and give three representative case
studies, which we model and analyse in more detail. The examples used
in this paper cover signal transduction pathways as well as metabolic
pathways.
abstract: This paper demonstrates the first steps of a new integrating methodology to develop and analyse models of biological pathways in a systematic manner using well established Petri net technologies. The whole approach comprises stepwise modelling, animation, model validation as well as qualitative and quantitative analysis for behaviour prediction. In this paper, the first phase is addressed - how to develop and validate a qualitative model, which might be extended afterwards to a quantitative model. The example used in this paper is devoted to apoptosis, the genetically programmed cell death. Apoptosis is an essential part of normal physiology for most metazoan species. Disturbances in the apoptotic process could lead to several diseases. The signal transduction pathway of apoptosis includes highly complex mechanisms to control and execute programmed cell death. This paper explains how to model and validate this pathway using qualitative Petri nets. The results provide a mathematically unique and valid model enabling the confirmation of known properties as well as new insights in this pathway.
abstract: Computer assisted analysis and simulation of biochemical pathways can improve the understanding of the structure and the dynamics of cell processes considerably. The construction and quantitative analysis of kinetic models is often impeded by the lack of reliable data. However, as the topological structure of biochemical systems can be regarded to remain constant in time, a qualitative analysis of a pathway model was shown to be quite promising as it can render a lot of useful knowledge, e.g., about its structural invariants. The topic of this paper are pathways whose substances have reached a dynamic concentration equilibrium (steady state). It is argued that appreciated tools from biochemistry and also low-level Petri nets can yield only part of the desired results, whereas executable high-level net models lead to a number of valuable additional insights by combining symbolic analysis and simulation.
Heiner, M.; Koch, I.; Will, J.:abstract: This bibliography
provides 74 entries
in biochemistry, 1 entry for
chemistry, 58 entries for medicine, and 14 entries for ecology and
environment.
abstract: There is an increasing demand to certify the security of systems according to the Common Criteria (CC). The CC distinguish several evaluation assurance levels (EALs), level EAL7 being the highest and requiring the application of formal techniques. We present a method for requirements engineering and (semi-formal and formal) modeling of systems to be certified according to the higher evaluation assurance levels of the CC. The method is problem oriented, i.e. it is driven by the environment in which the system will operate and by a mission statement. We illustrate our approach by an industrial case study, namely an electronic purse card (EPC) to be implemented on a Java Smart Card. As a novelty, we treat the mutual asymmetric authentication of the card and the terminal into which the card is inserted.
abstract: At WODES ’98, we
introduced an approach to
modelling and analysis of PLC systems using ordinary Petri nets. This
paper supplements the former one by presenting detailed contributions
to a systematic model design of the application program’s surroundings.
For that purpose, design aspects of the environment model as well as
three different kinds of models for the system program are discussed.
As a side effect, an obvious principle of timer modelling turns out.
abstract: We show how to combine the specification notation Z with Petri nets for modeling safety-critical systems. The combination preserves the strengths of the two formalisms, while ameliorating their drawbacks. We illustrate our approach by modeling a part of a production cell and validating that model with respect to safety-related properties.
Heiner, M.; Menzel, T.:abstract: In diesem Bericht
beschreiben wir eine
Möglichkeit zur Modellierung und Analyse von SPS- Systemen. Dazu
stellen wir zunächst kurz eine Petri-Netz-Semantik für die
SPS-Anwenderprogram miersprache Anweisungsliste (AWL) vor, welche in
der IEC 1131-3 [DIN EN 61131-3] definiert wurde. Anschließend
diskutieren wir wesentliche Punkte einer Methodik zur Erstellung eines
Systemmodells, wobei sowohl der Entwurf des notwendigen
Umgebungsmodelles als auch drei verschiedene Mögli chkeiten
für das Systemprogramm angesprochen werden. Zum Abschluß
wird die Generierung des Petri-Netz-Modelles aus einem gegebenen
SPS-System anhand eines Beispiels praktisch illustriert.
abstract: The application of
Petri
nets is one of the
well-know approaches for developing provably error-free control
software for manufacturing systems. To evaluate the practicability of
available methods and tools for at least medium-sized systems, a case
study has been performed to develop modularized control software of a
production cell with hierarchical Petri nets, supporting reuse as well
as stepwise validation.
abstract: In this paper we combine structural analysis of Petri nets with the symbolic representation of state spaces by Binary Decision Diagrams (BDDs). The size of a BDD is determined by the number of its variables and by their order. We suggest two methods based on structural properties (precisely one- token-P-invariants) which improve the encoding of states. One method attempts to derive a good variable order. The other tries to reduce the needed number of variables by compacting the encoding of states.
Deussen, P.:abstract: Partial order semantics of Petri nets have a long history. In this paper, we describe a formalism which combines partial order semantics with the usual notion of markings of a Petri net. We call this formalism concurrent automata. We present a generation algorithm for concurrent automata. We show that our algorithm is correct in the sense of semi language equivalence: The generated automaton recognizes essentially the same set of semiwords as the associated Petri net.
Heiner, M.:abstract: The development of provably error-free concurrent systems is still a challenge of practical system engineering. Modeling and analysis of concurrent systems by means of Petri nets is one of the well-known approaches using formal methods. Among those Petri net analysis techniques suitable for strong verification purposes there is an increasing amount of promising methods avoiding the construction of the complete interleaving state space, and by this way the well-known state explosion problem. These alternative approaches are summarized and compared with each other: structural analysis, integer programming, compressed and composite state space representations, lazy state space constructions, and partial order representations. It is demonstrated by means of case studies that the available methods and tools are actually applicable successfully to at least medium-sized systems. For that purpose, the step-wise validation of various qualitative system properties (consistency, safety, progress) of the concurrent control software of reactive systems is exemplified. If possible, different analysis techniques are applied and compared with each other concerning their pros and cons. The main lesson learned is that the different methods do not compete, but complement each other. Finally, objectives of an open integrated tool box to support Petri net based dependability engineering are outlined.
Heiner, M; Menzel, T.:abstract: In this paper we describe a Petri net semantics of the PLC language Instruction List (IL) defined in IEC 1131-3 [DIN EN 61131-3]. This is a necessary prerequisite to be able to analyze functional and especially safety requirements of IL programs. We introduce a subset of IL (IL0) and give formal definitions as reference semantics for this subset. After this, the reference semantics is transformed into a Petri net model.
Heiner, M; Menzel, T.:abstract: In order to adapt a Petri net based verification framework to programmable logic controllers, a Petri net semantics is introduced formally for a subset of the standardized Instruction List language [IEC 1131-3]. For that purpose, the subset's syntax as well as static and operational semantics are specified strictly. Having that, the operational reference semantics is substituted by an equivalent Petri net semantics. Due to this prudent practice, the equivalence proof of the substitution step is obvious.
abstract: In the development of provably error-free control software for manufacturing systems the application of Petri nets is a well-known approach. One of the main advantages of Petri nets are their sound mathematical background which makes it possible to analyse and validate the qualitative and quantitative behavior of a Petri net system by formal methods. The gap between the validated Petri net model and the needed control software can be closed by directly synthesizing the control software form a Petri net specification. One way to achieve this, is to assign control code to the transitions and use a Petri net simulator to simulate the tokenflow of a Petri net. We have realized a parallel Petri net simulator (FUNlite), especially designed for fast execution speed, low memory consumption and low communication overhead. When simulating a Petri net system, the speed of the transition enabling test plays an important role. In FUNlite the enabling test is highly simplified by a method characterizing the enabling of a transition at a given marking by a simple number comparison.
König, H.; Ulrich, A.; Heiner, M.:abstract:It is well-known in Petri net theory that there is generally no strong relation between the properties of qualitative and quantitative Petri net models due to the influence of time constraints on the general net behaviour. That holds for any type of time-dependent Petri net. Therefore, in order to integrate qualitative as well as quantitative analysis on a common intermediate system representation, an important feature of a related methodology is the ability of controlled maintenance of any analysis results gained during qualitative validation steps. For that purpose, this paper summarizes and explains available results on the influence of interval time on qualitative properties of Petri nets, boundedness as well as liveness
Heiner, M.:abstract:The development of provably error-free and efficient concurrent manufacturing systems is still a challenge of practical system engineering. Modelling and analysis of concurrent systems by means of Petri nets is one of the well-known approaches using formal methods. Among those Petri net analysis techniques suitable for strong verification purposes there is an increasing amount of promising methods avoiding the construction of the complete interleaving state space, and by this way the well-known state explosion problem. This paper demonstrates that available methods and tools are actually applicable successfully to at least medium-sized manufacturing systems. For that purpose, step-wise validation of various system properties (consistency, safety, progress) and optimization of the concurrent controller software of a discrete event system is performed. If possible, different analysis techniques are applied and compared with each other concerning their efforts.
Popova-Zeugmann, L.; Heiner, M.:[ improved version: ] Humboldt-Universität zu Berlin, Informatik-Bericht Nr. 83, May 1997, 18 p.
abstract: This paper deals with computing the minimal and maximal execution durations in a given concurrent control system in order to support dependability engineering by assuring the meeting of prescribed deadlines. For that purpose, a new type of time-dependent Petri nets - the Duration Interval Petri net - is introduced, and a dedicated reachability graph is defined in a discrete way. Using this reach ability graph, shortest and largest time paths between two arbitrary states of the control system, and by this way minimal and maximal execution times, can be computed.
Heiner, M.:abstract: The development of provably error-free concurrent systems is still a challenge of practical system engineering. Modelling and analysis of concurrent systems by means of Petri nets is one of the well-known approaches using formal methods. Among those Petri net analysis techniques suitable for strong verification purposes there is an increasing amount of promising methods avoiding the construction of the complete interleaving state space, and by this way the well-known state explosion problem. This paper claims to demonstrate that the available methods and tools are actually applicable successfully to at least medium-sized systems. For that purpose, the step-wise validation of various system properties (consistency, safety, progress) of the concurrent control software of a reactive system is performed. If possible, different analysis techniques are applied and compared with each other concerning its efforts.
abstract: The application of Petri nets is one of the well-known approaches to develop provably error-free control software of manufacturing systems. To evaluate the reached practicability degree of available methods and tools to at least medium-sized systems, a case study has been performed to develop modularized control software of a production cell with hierarchical Petri nets, supporting reuse as well as step-wise validation.
Lindner, G.; Heiner, M.; Kobienia, T.:abstract: In this paper we apply the methods proposed in [mh92], [mh94] for detecting anomalies in existing executable INMOS C code for a parallel program using static and dynamic analyses of Petri nets. Our target architecture on which the application program is running is a transputer network. The algorithmic translation of the INMOS C program into hierarchical place/transition nets which preserves both control and message flow is performed by a Petri net generator. Every implemented process is converted into an equivalent net. After this, the net parts generated are visualized and linked, and supplements are added, using a powerful graphical Petri net editor. Hierarchical methods are furnished, e.g. function calls are levelled down to subnets, and communication interface objects are highlighted. Every net object in the graphical representation is referenced with its counterpart in the source code so that error localization is possible. In the next processing step, the output capabilities of the Petri net editor are used to produce several input files for analyzing tools. Finally, the process nets investigated separately are brought together by merging the communication interfaces into one whole top level net. Here, a renewed analysis is performed.
Heiner, M.; Deussen, P.:abstract: The development of provably error-free concurrent systems is still a challenge of system engineering. Modelling and analysis of concurrent systems by means of Petri nets is one of the well- known approaches using formal methods. To evaluate the reached practicability degree of available methods and tools to at least medium-sized systems, the authors demonstrate the step-wise devel opment and validation of the control software of a reactive system [13]. Strong emphasis has been laid on automation of the analyses to be done. This paper provides a brief outline of the authors' work, stressing especially analysis experience.
Heiner, M.; Deussen, P.:abstract: The development of provably error-free concurrent systems is still a challenge of system engineering. Modelling and analysis of concurrent systems by means of Petri nets is one of the well- known approaches using formal methods. To evaluate the reached practicability degree of available methods and tools to at least medium-sized systems, we demonstrate the step-wise development and validation of the control software of a reactive system. The validation of qualitative properties comprises two steps. At first, context checking of general semantic properties is done by a suitable combination of static and dynamic analysis techniques of Petri net theory. Afterwards, verification of well-defined special semantic properties, especially safety properties, given by a separate specification of the required functionality, is performed by model checking. Strong emphasis has been laid on automation of the analyses to be done.
abstract:1. Dependability terminology; 2. Petri net approach; 3. Modelling with Petri nets: Control structure model (CSM) as place/transition net, Control flow model (CFM) as coloured net, Interacting concurrent processes (ICP); 4. Qualitative analyzing with Petri nets: Context checking with Petri net theory, Verification with temporal logics; 5. Quantitative analyzing with Petri nets: Worst-case evaluation with duration interval nets, performance prediction with stochastic nets, reliability prediction with stochastic nets; 6. Conclusions; 7. References; 8. Appendix: Case study;
Heiner, M.:abstract: Methods of software dependability engineering can be divided into two groups - methods to improve the software dependability and methods to predict the reached degree of software dependability. Among those methods, which aim at the improvement of software dependability, the Petri net based validation techniques to avoid faults during the development phase have attract a lot of attention in the last years. Within this framework, Petri net models play the role of a common intermediate software representation, from which different validation techniques are able to start - qualitative as well as quanti tative ones. Based on this experience, the approach to integrate different methods on a common repre sentation is extended by a formal method to derive Petri net models suitable for a structure-oriented reliability prediction.
abstract: An innovative net-based methodology to integrate qualitative and quantitative analysis of distributed software systems is outlined, and an on-going prototype implementation of a related graphic- oriented tool kit is sketched. The proposed method combines qualitative analysis, monitoring and testing as well as quantitative analysis on the basis of a net-based intermediate representation of the distributed software system under consideration. All transformations (from the distributed software system into a first Petri net model, and between the different kinds of net models) can be done formally, and therefore automated to a high degree. The evaluation of quantitative properties is based on so-called object nets which are obtained by a property-preserving structural compression and quantitative expansion of the qualitative model. Hereby, the frequency and delay attributes necessary to generate quantitative models are provided by the monitoring and testing component.
