City Research Online

Abstract

With the growing popularity of web services the demand of highly reliable service based systems (SBS) is increasing. Formal verification and testing are performed to ensure the correctness of a system before it is deployed in a real environment. But the high complexity of complete fielded systems puts their effectiveness into questions. Runtime monitoring is the potential technique to cover the area not covered by formal verification and testing. This technique aims to assure the correctness of the current execution of a system. Substantial amount of research has been carried out in runtime monitoring to ensure the reliability of autonomous legacy software. However in service based system some significant complications arises as they focus on systems with no autonomous components, that make the approaches applied to monitor legacy software inadequate for service based system. In this thesis we present a framework for runtime monitoring of service based systems. We establish the necessity of introducing new types of inconsistencies beyond the classical inconsistencies that may occur during the execution of service based systems and develop reasoning mechanism to detect them at run time.

In the proposed framework, the properties to be monitored include: (i) behavioural properties of the co-ordination process of the service based system, (ii) functional properties that express functional requirements for the individual services of a service based system or groups of such services, (ii) assumptions regarding the behaviour of the service based system and its constituent services and their effects on the state of the system and (iii) Quality-of- Service (QOS) properties for the service based systems and its constituent services. All types of properties are expressed in a property specification language which is based on event- calculus [Sha99]. The behavioural properties to be monitored at run-time are extracted automatically from the specification of the co-ordination process of a service-based system in BPEL [Bpe03] while the other types of properties to be monitored must be specified by the providers of the system. These properties must be specified in terms of: (i) events that can be observed at run-time and correspond to either operation invocation and response messages or the assignment of values to global variables used by the co-ordination process of the system, and (ii) conditions over the state of the co-ordination process of the system and/or the individual services deployed by it. These restrictions ensure that property monitoring can be based solely on events which are generated by virtue of the normal operation of the system without the need for instrumenting the individual services deployed by it. The property specification language that is used by this framework is a first-order logic language that incorporates special predicates to signify assertions about time and, to this end, it provides a very expressive framework for specifying properties of service based system, which may include temporal characteristics.

At run-time, the framework deploys an event receiver that catches events which are exchanged by the different services and the co-ordination process of the system and stores them in an event database. This database is accessed by a monitor that can detect different types of violations of properties. These types are: (i) violations of functional properties and quality-of-service properties by the recorded behaviour of the service based system, (ii) violations and potential violations of behavioural properties, functional properties and quality- of-service properties by the expected system behaviour, and (iii) unjustified and potentially unjustified actions which the system has taken by wrongly assuming that certain pre-conditions associated with the undertaken actions were satisfied at run-time. The detection of these types of violations is fully automatic and is based on an algorithm that has been developed as a variant of algorithms for integrity constraint checking in temporal deductive databases [Ple93, Cho95]. We have implemented a prototype of the proposed monitoring framework and showed the effectiveness of the monitoring prototype through several case studies.

Publication Type:	Thesis (Doctoral)
Subjects:	Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments:	School of Science & Technology > Computer Science School of Science & Technology > School of Science & Technology Doctoral Theses Doctoral Theses

Export

Downloads