Service-oriented systems (SOS) have recently emerged as context-independent component-based systems. In contrast to components, services can be created, invoked, composed and destroyed at run-time. Services are assumed to be platform independent and available for use within heterogeneous applications. One of the main assets in SOS is service composability. It allows the development of composite services with the main goal of reusable functionality provided by existing services in a low cost and rapid development process at run-time. However, in such distributed systems it becomes difficult to guarantee the quality of services (QoS), both in isolation, as well as of the newly created service compositions. Means of checking correctness of service composition can enable optimization w.r.t. the function and resource-usage of composed services, as well as provide a higher degree of QoS assurance of a service composition. To accomplish such goals, we employ model-checking technique for both single and composed services. The verification eventually provides necessaryinformation about QoS, already at early development stage.This thesis presents the research that we have been carrying out, on developing of methods and tools for specification, modeling, and formal analysis of services and service compositions in SOS. In this work, we first show how to formally check QoS in terms of performance and reliability for formallyspecified component-based systems (CBS). Next, we outline the commonalities and differences between SOS and CBS. Third, we develop constructs for the formal description of services using the resource-aware timed behavioral language called REMES, including development of language to support service compositions. At last, we show how to check service and service composition(functional, timing and resource-wise) correctness by employing the strongest post condition semantics. For less complex services and service compositions we choose to prove correctness using Hoare triples and the guarded command language. In case of complex services described as priced timed automata(PTA), we prove correctness via algorithmic computation of strongest post-condition of PTA. / Q-ImPreSS

Although service oriented architecture has reached a particular maturity level especially in the technological dimension, there is a lack of common and acceptable approach to design a software system through composition and integration of web services. In this thesis, a service oriented system design approach for Service Oriented Architecture based software development is introduced to fill this gap. This new methodology basically offers a procedural top-down decomposition of a given software system allowing several abstraction levels. At the higher levels of the decomposition, the system is divided into abstract nodes that correspond to process models in the decomposition tree. Any node is a process and keeps the sequence and the state information for the possible sub-processes in this decomposition tree. Nodes which are defined as process models may include some sub-nodes to present details for the intermediate levels of the model. Eventually at the leaf level, process models are decomposed into existing web services as the atomic units of system execution. All processes constructing the system decomposition tree are modeled with BPEL (Business Process Execution Language) to expose the algorithmic details of the design. This modeling technique is also supported with a graphical modeling language referred to as SOSEML (Service Oriented Software Engineering Modeling Language) that is also newly introduced in this thesis.

In this thesis, a static analysis approach is introduced in order to develop correct business processes according to the Web Service Business Process Execution Language (WS-BPEL) specification. The modeling of the business processes are conducted with Business Process Execution Language (BPEL) which is a popular orchestrator of Service Oriented Architectures (SOA) based system through the description of workflow. This approach is also integrated to the Service Oriented Software Engineering (SOSE) design technique. The integration of this approach aims the development of complex business processes more robust and implementation of them more accurate and low error prone. Moreover, this approach will also decrease the development cost of the system and rework in the implementation phase. The implementation of the approach is also conducted and it is integrated to the existing service oriented architecture based tool named Service Oriented Software Engineering Tool (SOSECASE). This integration forwards the SOSECASE a step forward to an all-in-one service oriented architecure software development tool.

In this thesis, a service oriented decomposition approach: Use case Driven Service Oriented Architecture (UDSOA), is introduced to close the gap between business requirements and SOA (Service Oriented Architecture) design by including business use cases and system use cases into decomposition process. The approach is constructed upon Service Oriented Software Engineering (SOSE) modeling technique and aims to fill the deficits of it at the decomposition phase. Further, it aims to involve both business vision and Information Technologies concerns in the decomposition process. This approach starts with functional top-down decomposition of the domain. Then, business use cases are used for further decomposition because of their high-level view. This connects the business requirements and our SOA design. Also it raises the level of abstraction which allows us to focus on business services. Second step of the SOA approach uses system use cases to continue decomposition. System use cases help discovering technical web services and allocating them on the decomposition tree. Service oriented analysis also helps separating business and technical services in tightly coupled architecture conditions. Those two steps together bring quality in to both problem and solution domains.