Specification of design and verification of service-oriented systems

Robert Marzeta

AbstractAs 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’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.
TypeMaster's thesis [Academic thesis]
Year2007
PublisherInformatics and Mathematical Modelling, Technical University of Denmark, DTU
AddressRichard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby
SeriesIMM-Thesis-2007-103
NoteSupervised by Professor Hanne Riis Nielson, IMM, DTU.
Electronic version(s)[pdf]
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering