@MASTERSTHESIS\{IMM2007-05560,
    author       = "R. Marzeta",
    title        = "Specification of design and verification of service-oriented systems",
    year         = "2007",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Professor Hanne Riis Nielson, {IMM,} {DTU}.",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5560-full.html",
    abstract     = "As a next step of software development evolution, Service Oriented Architecture is already a widely accepted standard to modern software systems. However, it seems that there are not enough tools and techniques that could allow efficient and precise modeling and verification of {SOA}. This thesis is an attempt to analyze and address some of those issues.

Firstly, some of {SOA'}s mechanisms are described in the example of a hypothetical test scenario to show how the new approach can be effectively pursued to solve real problems. A number of known technologies and standards are reviewed ({UML,} Petri Nets, {MDA}) with respect to {SOA} applicability. Next, {SOA'}s verification possibilities are assessed followed by the extraction of scenario specific properties.

Secondly, using an application {CPN} Tools, two design methodologies are followed to create a model realizing the test scenario. Results are compared in terms of clarity, scalability and complexity, which also influences verification suitability. Next, in order to complete partial verification provided by {CPN} Tools, Uppaal application is introduced. After showing two simple usage examples of modeling components and protocols, both Uppaal\&\#146;s strengths and weaknesses (towards {SOA}) are described.

Furthermore, an experimental algorithm is presented to transform a {CPN} Tools Petri net(s) to a state machine(s) compatible with Uppaal. The mapping takes under consideration various Petri net structures and produces significantly extensive models (more than 50 templates and 400 locations). Lastly, algorithm constraints are presented together with a discussion on other
possible transformations."
}