@phdthesis{RianoPachon2008, author = {Ria{\~n}o-Pach{\´o}n, Diego Mauricio}, title = {Identification of transcription factor genes in plants}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-27009}, school = {Universit{\"a}t Potsdam}, year = {2008}, abstract = {In order to function properly, organisms have a complex control mechanism, in which a given gene is expressed at a particular time and place. One way to achieve this control is to regulate the initiation of transcription. This step requires the assembly of several components, i.e., a basal/general machinery common to all expressed genes, and a specific/regulatory machinery, which differs among genes and is the responsible for proper gene expression in response to environmental or developmental signals. This specific machinery is composed of transcription factors (TFs), which can be grouped into evolutionarily related gene families that possess characteristic protein domains. In this work we have exploited the presence of protein domains to create rules that serve for the identification and classification of TFs. We have modelled such rules as a bipartite graph, where families and protein domains are represented as nodes. Connections between nodes represent that a protein domain should (required rule) or should not (forbidden rule) be present in a protein to be assigned into a TF family. Following this approach we have identified putative complete sets of TFs in plant species, whose genome is completely sequenced: Cyanidioschyzon merolae (red algae), Chlamydomonas reinhardtii (green alga), Ostreococcus tauri (green alga), Physcomitrella patens (moss), Arabidopsis thaliana (thale cress), Populus trichocarpa (black cottonwood) and Oryza sativa (rice). The identification of the complete sets of TFs in the above-mentioned species, as well as additional information and reference literature are available at http://plntfdb.bio.uni-potsdam.de/. The availability of such sets allowed us performing detailed evolutionary studies at different levels, from a single family to all TF families in different organisms in a comparative genomics context. Notably, we uncovered preferential expansions in different lineages, paving the way to discover the specific biological roles of these proteins under different conditions. For the basic leucine zipper (bZIP) family of TFs we were able to infer that in the most recent common ancestor (MRCA) of all green plants there were at least four bZIP genes functionally involved in oxidative stress and unfolded protein responses that are bZIP-mediated processes in all eukaryotes, but also in light-dependent regulations. The four founder genes amplified and diverged significantly, generating traits that benefited the colonization of new environments. Currently, following the approach described above, up to 57 TF and 11 TR families can be identified, which are among the most numerous transcription regulatory families in plants. Three families of putative TFs predate the split between rhodophyta (red algae) and chlorophyta (green algae), i.e., G2-like, PLATZ, and RWPRK, and may have been of particular importance for the evolution of eukaryotic photosynthetic organisms. Nine additional families, i.e., ABI3/VP1, AP2-EREBP, ARR-B, C2C2-CO-like, C2C2-Dof, PBF-2-like/Whirly, Pseudo ARR-B, SBP, and WRKY, predate the split between green algae and streptophytes. The identification of putative complete list of TFs has also allowed the delineation of lineage-specific regulatory families. The families SBP, bHLH, SNF2, MADS, WRKY, HMG, AP2-EREBP and FHA significantly differ in size between algae and land plants. The SBP family of TFs is significantly larger in C. reinhardtii, compared to land plants, and appears to have been lost in the prasinophyte O. tauri. The families bHLH, SNF2, MADS, WRKY, HMG, AP2-EREBP and FHA preferentially expanded with the colonisation of land, and might have played an important role in this great moment in evolution. Later, after the split of bryophytes and tracheophytes, the families MADS, AP2-EREBP, NAC, AUX/IAA, PHD and HRT have significantly larger numbers in the lineage leading to seed plants. We identified 23 families that are restricted to land plants and that might have played an important role in the colonization of this new habitat. Based on the list of TFs in different species we have started to develop high-throughput experimental platforms (in rice and C. reinhardtii) to monitor gene expression changes of TF genes under different genetic, developmental or environmental conditions. In this work we present the monitoring of Arabidopsis thaliana TFs during the onset of senescence, a process that leads to cell and tissue disintegration in order to redistribute nutrients (e.g. nitrogen) from leaves to reproductive organs. We show that the expression of 185 TF genes changes when leaves develop from half to fully expanded leaves and finally enter partial senescence. 76\% of these TFs are down-regulated during senescence, the remaining are up-regulated. The identification of TFs in plants in a comparative genomics setup has proven fruitful for the understanding of evolutionary processes and contributes to the elucidation of complex developmental programs.}, language = {en} } @phdthesis{GuedesCorrea2009, author = {Guedes Corr{\^e}a, Luiz Gustavo}, title = {Evolutionary and functional analysis of transcription factors controlling leaf development}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-40038}, school = {Universit{\"a}t Potsdam}, year = {2009}, abstract = {Leaves are the main photosynthetic organs of vascular plants, and leaf development is dependent on a proper control of gene expression. Transcription factors (TFs) are global regulators of gene expression that play essential roles in almost all biological processes among eukaryotes. This PhD project focused on the characterization of the sink-to-source transition of Arabidopsis leaves and on the analysis of TFs that play a role in early leaf development. The sink-to-source transition occurs when the young emerging leaves (net carbon importers) acquire a positive photosynthetic balance and start exporting photoassimilates. We have established molecular and physiological markers (i.e., CAB1 and CAB2 expression levels, AtSUC2 and AtCHoR expression patterns, chlorophyll and starch levels, and photosynthetic electron transport rates) to identify the starting point of the transition, especially because the sink-to-source is not accompanied by a visual phenotype in contrast to other developmental transitions, such as the mature-to-senescent transition of leaves. The sink-to-source transition can be divided into two different processes: one light dependent, related to photosynthesis and light responses; and one light independent or impaired, related to the changes in the vascular tissue that occur when leaves change from an import to an export mode. Furthermore, starch, but not sucrose, has been identified as one of the potential signalling molecules for this transition. The expression level of 1880 TFs during early leaf development was assessed by qRTPCR, and 153 TFs were found to exhibit differential expression levels of at least 5-fold. GRF, MYB and SRS are TF families, which are overrepresented among the differentially expressed TFs. Additionally, processes like cell identity acquisition, formation of the epidermis and leaf development are overrepresented among the differentially expressed TFs, which helps to validate the results obtained. Two of these TFs were further characterized. bZIP21 is a gene up-regulated during the sink-to-source and mature-to-senescent transitions. Its expression pattern in leaves overlaps with the one observed for AtCHoR, therefore it constitutes a good marker for the sink-to-source transition. Homozygous null mutants of bZIP21 could not be obtained, indicating that the total absence of bZIP21 function may be lethal to the plant. Phylogenetic analyses indicate that bZIP21 is an orthologue of Liguleless2 from maize. In these analyses, we identified that the whole set of bZIPs in plants originated from four founder genes, and that all bZIPs from angiosperms can be classified into 13 groups of homologues and 34 Possible Groups of Orthologues (PoGOs). bHLH64 is a gene highly expressed in early sink leaves, its expression is downregulated during the mature-to-senescent transition. Null mutants of bHLH64 are characterized by delayed bolting when compared to the wild-type; this indicates a possible delay in the sink-to-source transition or the retention of a juvenile identity. A third TF, Dof4, was also characterized. Dof4 is neither differentially expressed during the sink-to-source nor during the senescent-to-mature transition, but a null mutant of Dof4 develops bigger leaves than the wild-type and forms a greater number of siliques. The Dof4 null mutant has proven to be a good background for biomass accumulation analysis. Though not overrepresented during the sink-to-source transition, NAC transcription factors seem to contribute significantly to the mature-to-senescent transition. Twenty two NACs from Arabidopsis and 44 from rice are differentially expressed during late stages of leaf development. Phylogenetic analyses revealed that most of these NACs cluster into three big groups of homologues, indicating functional conservation between eudicots and monocots. To prove functional conservation of orthologues, the expression of ten NAC genes of barley was analysed. Eight of the ten NAC genes were found to be differentially expressed during senescence. The use of evolutionary approaches combined with functional studies is thus expected to support the transfer of current knowledge of gene control gained in model species to crops.}, language = {en} } @phdthesis{Schuette2011, author = {Sch{\"u}tte, Moritz}, title = {Evolutionary fingerprints in genome-scale networks}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-57483}, school = {Universit{\"a}t Potsdam}, year = {2011}, abstract = {Mathematical modeling of biological phenomena has experienced increasing interest since new high-throughput technologies give access to growing amounts of molecular data. These modeling approaches are especially able to test hypotheses which are not yet experimentally accessible or guide an experimental setup. One particular attempt investigates the evolutionary dynamics responsible for today's composition of organisms. Computer simulations either propose an evolutionary mechanism and thus reproduce a recent finding or rebuild an evolutionary process in order to learn about its mechanism. The quest for evolutionary fingerprints in metabolic and gene-coexpression networks is the central topic of this cumulative thesis based on four published articles. An understanding of the actual origin of life will probably remain an insoluble problem. However, one can argue that after a first simple metabolism has evolved, the further evolution of metabolism occurred in parallel with the evolution of the sequences of the catalyzing enzymes. Indications of such a coevolution can be found when correlating the change in sequence between two enzymes with their distance on the metabolic network which is obtained from the KEGG database. We observe that there exists a small but significant correlation primarily on nearest neighbors. This indicates that enzymes catalyzing subsequent reactions tend to be descended from the same precursor. Since this correlation is relatively small one can at least assume that, if new enzymes are no "genetic children" of the previous enzymes, they certainly be descended from any of the already existing ones. Following this hypothesis, we introduce a model of enzyme-pathway coevolution. By iteratively adding enzymes, this model explores the metabolic network in a manner similar to diffusion. With implementation of an Gillespie-like algorithm we are able to introduce a tunable parameter that controls the weight of sequence similarity when choosing a new enzyme. Furthermore, this method also defines a time difference between successive evolutionary innovations in terms of a new enzyme. Overall, these simulations generate putative time-courses of the evolutionary walk on the metabolic network. By a time-series analysis, we find that the acquisition of new enzymes appears in bursts which are pronounced when the influence of the sequence similarity is higher. This behavior strongly resembles punctuated equilibrium which denotes the observation that new species tend to appear in bursts as well rather than in a gradual manner. Thus, our model helps to establish a better understanding of punctuated equilibrium giving a potential description at molecular level. From the time-courses we also extract a tentative order of new enzymes, metabolites, and even organisms. The consistence of this order with previous findings provides evidence for the validity of our approach. While the sequence of a gene is actually subject to mutations, its expression profile might also indirectly change through the evolutionary events in the cellular interplay. Gene coexpression data is simply accessible by microarray experiments and commonly illustrated using coexpression networks where genes are nodes and get linked once they show a significant coexpression. Since the large number of genes makes an illustration of the entire coexpression network difficult, clustering helps to show the network on a metalevel. Various clustering techniques already exist. However, we introduce a novel one which maintains control of the cluster sizes and thus assures proper visual inspection. An application of the method on Arabidopsis thaliana reveals that genes causing a severe phenotype often show a functional uniqueness in their network vicinity. This leads to 20 genes of so far unknown phenotype which are however suggested to be essential for plant growth. Of these, six indeed provoke such a severe phenotype, shown by mutant analysis. By an inspection of the degree distribution of the A.thaliana coexpression network, we identified two characteristics. The distribution deviates from the frequently observed power-law by a sharp truncation which follows after an over-representation of highly connected nodes. For a better understanding, we developed an evolutionary model which mimics the growth of a coexpression network by gene duplication which underlies a strong selection criterion, and slight mutational changes in the expression profile. Despite the simplicity of our assumption, we can reproduce the observed properties in A.thaliana as well as in E.coli and S.cerevisiae. The over-representation of high-degree nodes could be identified with mutually well connected genes of similar functional families: zinc fingers (PF00096), flagella, and ribosomes respectively. In conclusion, these four manuscripts demonstrate the usefulness of mathematical models and statistical tools as a source of new biological insight. While the clustering approach of gene coexpression data leads to the phenotypic characterization of so far unknown genes and thus supports genome annotation, our model approaches offer explanations for observed properties of the coexpression network and furthermore substantiate punctuated equilibrium as an evolutionary process by a deeper understanding of an underlying molecular mechanism.}, language = {en} } @phdthesis{CastroPrieto2011, author = {Castro Prieto, Aines del Carmen}, title = {Immunogenetics of free-ranging felids on Namibian farmlands}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-55505}, school = {Universit{\"a}t Potsdam}, year = {2011}, abstract = {Genetic variation is crucial for the long-term survival of the species as it provides the potential for adaptive responses to environmental changes such as emerging diseases. The Major Histocompatibility Complex (MHC) is a gene family that plays a central role in the vertebrate's immune system by triggering the adaptive immune response after exposure to pathogens. MHC genes have become highly suitable molecular markers of adaptive significance. They synthesize two primary cell surface molecules namely MHC class I and class II that recognize short fragments of proteins derived respectively from intracellular (e.g. viruses) and extracellular (e.g. bacteria, protozoa, arthropods) origins and present them to immune cells. High levels of MHC polymorphism frequently observed in natural populations are interpreted as an adaptation to detect and present a wide array of rapidly evolving pathogens. This variation appears to be largely maintained by positive selection driven mainly by pathogenic selective pressures. For my doctoral research I focused on MHC I and II variation in free-ranging cheetahs (Acinonyx jubatus) and leopards (Panthera pardus) on Namibian farmlands. Both felid species are sympatric thus subject to similar pathogenic pressures but differ in their evolutionary and demographic histories. The main aims were to investigate 1) the extent and patterns of MHC variation at the population level in both felids, 2) the association between levels of MHC variation and disease resistance in free-ranging cheetahs, and 3) the role of selection at different time scales in shaping MHC variation in both felids. Cheetahs and leopards represent the largest free-ranging carnivores in Namibia. They concentrate in unprotected areas on privately owned farmlands where domestic and other wild animals also occur and the risk of pathogen transmission is increased. Thus, knowledge on adaptive genetic variation involved in disease resistance may be pertinent to both felid species' conservation. The cheetah has been used as a classic example in conservation genetics textbooks due to overall low levels of genetic variation. Reduced variation at MHC genes has been associated with high susceptibility to infectious diseases in cheetahs. However, increased disease susceptibility has only been observed in captive cheetahs whereas recent studies in free-ranging Namibian cheetahs revealed a good health status. This raised the question whether the diversity at MHC I and II genes in free-ranging cheetahs is higher than previously reported. In this study, a total of 10 MHC I alleles and four MHC II alleles were observed in 149 individuals throughout Namibia. All alleles but one likely belong to functional MHC genes as their expression was confirmed. The observed alleles belong to four MHC I and three MHC II genes in the species as revealed by phylogenetic analyses. Signatures of historical positive selection acting on specific sites that interact directly with pathogen-derived proteins were detected in both MHC classes. Furthermore, a high genetic differentiation at MHC I was observed between Namibian cheetahs from east-central and north-central regions known to differ substantially in exposure to feline-specific viral pathogens. This suggests that the patterns of MHC I variation in the current population mirrors different pathogenic selective pressure imposed by viruses. Cheetahs showed low levels of MHC diversity compared with other mammalian species including felids, but this does not seem to influence the current immunocompetence of free-ranging cheetahs in Namibia and contradicts the previous conclusion that the cheetah is a paradigm species of disease susceptibility. However, it cannot be ruled out that the low MHC variation might limit a prosperous immunocompetence in the case of an emerging disease scenario because none of the remaining alleles might be able to recognize a novel pathogen. In contrast to cheetahs, leopards occur in most parts of Africa being perhaps the most abundant big cat in the continent. Leopards seem to have escaped from large-scale declines due to epizootics in the past in contrast to some free-ranging large carnivore populations in Africa that have been afflicted by epizootics. Currently, no information about the MHC sequence variation and constitution in African leopards exists. In this study, I characterized genetic variation at MHC I and MHC II genes in free-ranging leopards from Namibia. A total of six MHC I and six MHC II sequences were detected in 25 individuals from the east-central region. The maximum number of sequences observed per individual suggests that they likely correspond to at least three MHC I and three MHC II genes. Hallmarks of MHC evolution were confirmed such as historical positive selection, recombination and trans-species polymorphism. The low MHC variation detected in Namibian leopards is not conclusive and further research is required to assess the extent of MHC variation in different areas of its geographic range. Results from this thesis will contribute to better understanding the evolutionary significance of MHC and conservation implications in free-ranging felids. Translocation of wildlife is an increasingly used management tool for conservation purposes that should be conducted carefully as it may affect the ability of the translocated animals to cope with different pathogenic selective pressures.}, language = {en} } @misc{SicardLenhard2011, author = {Sicard, Adrien and Lenhard, Michael}, title = {The selfing syndrome a model for studying the genetic and evolutionary basis of morphological adaptation in plants}, series = {Annals of botany}, volume = {107}, journal = {Annals of botany}, number = {9}, publisher = {Oxford Univ. Press}, address = {Oxford}, issn = {0305-7364}, doi = {10.1093/aob/mcr023}, pages = {1433 -- 1443}, year = {2011}, abstract = {Background In angiosperm evolution, autogamously selfing lineages have been derived from outbreeding ancestors multiple times, and this transition is regarded as one of the most common evolutionary tendencies in flowering plants. In most cases, it is accompanied by a characteristic set of morphological and functional changes to the flowers, together termed the selfing syndrome. Two major areas that have changed during evolution of the selfing syndrome are sex allocation to male vs. female function and flower morphology, in particular flower (mainly petal) size and the distance between anthers and stigma. Scope A rich body of theoretical, taxonomic, ecological and genetic studies have addressed the evolutionary modification of these two trait complexes during or after the transition to selfing. Here, we review our current knowledge about the genetics and evolution of the selfing syndrome. Conclusions We argue that because of its frequent parallel evolution, the selfing syndrome represents an ideal model for addressing basic questions about morphological evolution and adaptation in flowering plants, but that realizing this potential will require the molecular identification of more of the causal genes underlying relevant trait variation.}, language = {en} } @misc{SchippersNguyenLuetal.2012, author = {Schippers, Jos H. M. and Nguyen, Hung M. and Lu, Dandan and Schmidt, Romy and M{\"u}ller-R{\"o}ber, Bernd}, title = {ROS homeostasis during development: an evolutionary conserved strategy}, series = {Cellular and molecular life sciences}, volume = {69}, journal = {Cellular and molecular life sciences}, number = {19}, publisher = {Springer}, address = {Basel}, issn = {1420-682X}, doi = {10.1007/s00018-012-1092-4}, pages = {3245 -- 3257}, year = {2012}, abstract = {The balance between cellular proliferation and differentiation is a key aspect of development in multicellular organisms. Recent studies on Arabidopsis roots revealed distinct roles for different reactive oxygen species (ROS) in these processes. Modulation of the balance between ROS in proliferating cells and elongating cells is controlled at least in part at the transcriptional level. The effect of ROS on proliferation and differentiation is not specific for plants but appears to be conserved between prokaryotic and eukaryotic life forms. The ways in which ROS is received and how it affects cellular functioning is discussed from an evolutionary point of view. The different redox-sensing mechanisms that evolved ultimately result in the activation of gene regulatory networks that control cellular fate and decision-making. This review highlights the potential common origin of ROS sensing, indicating that organisms evolved similar strategies for utilizing ROS during development, and discusses ROS as an ancient universal developmental regulator.}, language = {en} } @phdthesis{Becker2013, author = {Becker, Basil}, title = {Architectural modelling and verification of open service-oriented systems of systems}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-70158}, school = {Universit{\"a}t Potsdam}, year = {2013}, abstract = {Systems of Systems (SoS) have received a lot of attention recently. In this thesis we will focus on SoS that are built atop the techniques of Service-Oriented Architectures and thus combine the benefits and challenges of both paradigms. For this thesis we will understand SoS as ensembles of single autonomous systems that are integrated to a larger system, the SoS. The interesting fact about these systems is that the previously isolated systems are still maintained, improved and developed on their own. Structural dynamics is an issue in SoS, as at every point in time systems can join and leave the ensemble. This and the fact that the cooperation among the constituent systems is not necessarily observable means that we will consider these systems as open systems. Of course, the system has a clear boundary at each point in time, but this can only be identified by halting the complete SoS. However, halting a system of that size is practically impossible. Often SoS are combinations of software systems and physical systems. Hence a failure in the software system can have a serious physical impact what makes an SoS of this kind easily a safety-critical system. The contribution of this thesis is a modelling approach that extends OMG's SoaML and basically relies on collaborations and roles as an abstraction layer above the components. This will allow us to describe SoS at an architectural level. We will also give a formal semantics for our modelling approach which employs hybrid graph-transformation systems. The modelling approach is accompanied by a modular verification scheme that will be able to cope with the complexity constraints implied by the SoS' structural dynamics and size. Building such autonomous systems as SoS without evolution at the architectural level --- i. e. adding and removing of components and services --- is inadequate. Therefore our approach directly supports the modelling and verification of evolution.}, language = {en} } @article{HillLeowBleidornetal.2013, author = {Hill, Natascha and Leow, Alexander and Bleidorn, Christoph and Groth, Detlef and Tiedemann, Ralph and Selbig, Joachim and Hartmann, Stefanie}, title = {Analysis of phylogenetic signal in protostomial intron patterns using Mutual Information}, series = {Theory in biosciences}, volume = {132}, journal = {Theory in biosciences}, number = {2}, publisher = {Springer}, address = {New York}, issn = {1431-7613}, doi = {10.1007/s12064-012-0173-0}, pages = {93 -- 104}, year = {2013}, abstract = {Many deep evolutionary divergences still remain unresolved, such as those among major taxa of the Lophotrochozoa. As alternative phylogenetic markers, the intron-exon structure of eukaryotic genomes and the patterns of absence and presence of spliceosomal introns appear to be promising. However, given the potential homoplasy of intron presence, the phylogenetic analysis of this data using standard evolutionary approaches has remained a challenge. Here, we used Mutual Information (MI) to estimate the phylogeny of Protostomia using gene structure data, and we compared these results with those obtained with Dollo Parsimony. Using full genome sequences from nine Metazoa, we identified 447 groups of orthologous sequences with 21,732 introns in 4,870 unique intron positions. We determined the shared absence and presence of introns in the corresponding sequence alignments and have made this data available in "IntronBase", a web-accessible and downloadable SQLite database. Our results obtained using Dollo Parsimony are obviously misled through systematic errors that arise from multiple intron loss events, but extensive filtering of data improved the quality of the estimated phylogenies. Mutual Information, in contrast, performs better with larger datasets, but at the same time it requires a complete data set, which is difficult to obtain for orthologs from a large number of taxa. Nevertheless, Mutual Information-based distances proved to be useful in analyzing this kind of data, also because the estimation of MI-based distances is independent of evolutionary models and therefore no pre-definitions of ancestral and derived character states are necessary.}, language = {en} } @article{SteinertCassouHirschfeld2013, author = {Steinert, Bastian and Cassou, Damien and Hirschfeld, Robert}, title = {CoExist overcoming aversion to change preserving immediate access to source code and run-time information of previous development states}, series = {ACM SIGPLAN notices}, volume = {48}, journal = {ACM SIGPLAN notices}, number = {2}, publisher = {Association for Computing Machinery}, address = {New York}, issn = {0362-1340}, doi = {10.1145/2480360.2384591}, pages = {107 -- 117}, year = {2013}, abstract = {Programmers make many changes to the program to eventually find a good solution for a given task. In this course of change, every intermediate development state can of value, when, for example, a promising ideas suddenly turn out inappropriate or the interplay of objects turns out more complex than initially expected before making changes. Programmers would benefit from tool support that provides immediate access to source code and run-time of previous development states of interest. We present IDE extensions, implemented for Squeak/Smalltalk, to preserve, retrieve, and work with this information. With such tool support, programmers can work without worries because they can rely on tools that help them with whatever their explorations will reveal. They no longer have to follow certain best practices only to avoid undesired consequences of changing code.}, language = {en} } @book{GieseBecker2013, author = {Giese, Holger and Becker, Basil}, title = {Modeling and verifying dynamic evolving service-oriented architectures}, publisher = {Universit{\"a}tsverlag Potsdam}, address = {Potsdam}, isbn = {978-3-86956-246-9}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-65112}, publisher = {Universit{\"a}t Potsdam}, pages = {97}, year = {2013}, abstract = {The service-oriented architecture supports the dynamic assembly and runtime reconfiguration of complex open IT landscapes by means of runtime binding of service contracts, launching of new components and termination of outdated ones. Furthermore, the evolution of these IT landscapes is not restricted to exchanging components with other ones using the same service contracts, as new services contracts can be added as well. However, current approaches for modeling and verification of service-oriented architectures do not support these important capabilities to their full extend.In this report we present an extension of the current OMG proposal for service modeling with UML - SoaML - which overcomes these limitations. It permits modeling services and their service contracts at different levels of abstraction, provides a formal semantics for all modeling concepts, and enables verifying critical properties. Our compositional and incremental verification approach allows for complex properties including communication parameters and time and covers besides the dynamic binding of service contracts and the replacement of components also the evolution of the systems by means of new service contracts. The modeling as well as verification capabilities of the presented approach are demonstrated by means of a supply chain example and the verification results of a first prototype are shown.}, language = {en} }