<p>Embedded systems are becoming increasingly common in our everyday lives. As techonology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). At the same time, the systems must still fulfill strict requirements on reliability and correctness.</p><p>This thesis proposes a formal verification methodology which smoothly integrates with component-based system-level design using a divide and conquer approach. The methodology assumes that the system consists of several reusable components. Each of these components are already formally verified by their designers and are considered correct given that the environment satisfies certain properties imposed by the component. What remains to be verified is the glue logic inserted between the components. Each such glue logic is verified one at a time using model checking techniques.</p><p>The verification methodology as well as the underlying theoretical framework and algorithms are presented in the thesis.</p><p>Experimental results have shown the efficiency of the proposed methodology and demonstrated that it is feasible to apply it on real-life examples.</p> / Report code: LiU-Tek-Lic-2003:57.

With the wide-spread adoption of hypermedia systems and the World Wide Web (WWW) in particular, these systems have evolved from simple systems with only textual content to those that incorporate a large content base, which consists of a wide variety of document types. Also, with the increase in the number of users, there has grown a need for these systems to be accessible to a wider range of users. Consequently, the growth of the systems along with the number and variety of users require new presentation and navigation mechanisms for a wider audience. One of the new presentation methods is the audio-only presentation of hypertext content and this research proposes a novel solution to this problem for complex and dynamic systems. The hypothesis is that the proposed Audio Browser is an efficient tool for presenting hypertext in audio format, which will prove to be useful for several applications including browsers for visually-impaired and remote users. The Audio Browser provides audio-only browsing of contents in a Petri-based hypertext system called Context-Aware Trellis (caT). It uses a combination of synthesized speech and pre-recorded speech to allow its user to listen to contents of documents, follow links, and get information about the navigation process. It also has mechanisms for navigating within documents in order to allow users to view contents more quickly.

The survivability concerns the service continuity when the components of a system are damaged. This concept is especially useful in the emergency management of the system, as often emergencies involve accidents or incident disasters which more or less damage the system. The overall objective of this thesis study is to develop a quantitative management approach to the emergency management of a wireless cellular telecommunication system in light of its service continuity in emergency situations namely the survivability of the system. A particular wireless cellular telecommunication system, WCDMA, is taken as an example to ground this research.<p>The thesis proposes an ontology-based paradigm for service management such that the management system contains three models: (1) the work domain model, (2) the dynamic model, and (3) the reconfiguration model. A powerful work domain modeling tool called Function-Behavior-Structure (FBS) is employed for developing the work domain model of the WCDMA system. Petri-Net theory, as well as its formalization, is applied to develop the dynamic model of the WCDMA system. A concept in engineering design called the general and specific function concept is applied to develop a new approach to system reconfiguration for the high survivability of the system. These models are implemented along with a user-interface which can be used by emergency management personnel. A demonstration of the effectiveness of this study approach is included.<p>There are a couple of contributions with this thesis study. First, the proposed approach can be added to contemporary telecommunication management systems. Second, the Petri Net model of the WCDMA system is more comprehensive than any dynamic model of the telecommunication systems in literature. Furthermore, this model can be extended to any other telecommunication system. Third, the proposed system reconfiguration approach, based on the general and specific function concept, offers a unique way for the survivability of any service provider system.<p>In conclusion, the ontology-based paradigm for a service system management provides a total solution to service continuity as well as its emergency management. This paradigm makes the complex mathematical modeling of the system transparent to the manager or managerial personnel and provides a feasible scenario of the human-in-the-loop management.

In the Service Oriented Architecture (SOA) services are computational elements that are published, discovered, consumed and aggregated across platform and organizational borders. The most commonly used technology to achieve SOA are Web Services (WSs). This is due to standardization process (WSDL, SOAP, UDDI standards) and a wide range of available infrastructure and tools. A very interesting aspect of WSs is their composeability. WSs can be easily aggregated into complex workflows, called Composite Web Services (CWSs). These compositions of services enable further reuse and in this way new, even more complex, systems are built.<p>Although there are many languages to specify or implement workflows, in the service-oriented systems BPEL (Business Process Execution Language) is widely accepted. With this language WSs are orchestrated and then executed with specialized engines (like ActiveBPEL). While being very popular, BPEL has certain limitations in monitoring and optimizing executions of CWSs. It is very hard with this language to adapt CWSs to changes in the performance of used WSs, and also to select the optimal way to execute a CWS. <p>To overcome the limitations of BPEL, I present a model-aware approach to execute CWSs. To achieve the model awareness the Coloured Petri Nets (CPN) formalism is considered as the basis of the execution of CWSs. This is different than other works in using formal methods in CWSs, which are restricted to purposes like verification or checking of correctness. Here the formal and unambiguous notation of the CPN is used to model, analyze, execute and monitor CWSs. Furthermore this approach to execute CWSs, which is based on the CPN formalism, is implemented in the model-aware middleware. It is also demonstrated how the middleware improves the performance and reliability of CWSs.

No description available.

No description available.

The survivability concerns the service continuity when the components of a system are damaged. This concept is especially useful in the emergency management of the system, as often emergencies involve accidents or incident disasters which more or less damage the system. The overall objective of this thesis study is to develop a quantitative management approach to the emergency management of a wireless cellular telecommunication system in light of its service continuity in emergency situations namely the survivability of the system. A particular wireless cellular telecommunication system, WCDMA, is taken as an example to ground this research.<p>The thesis proposes an ontology-based paradigm for service management such that the management system contains three models: (1) the work domain model, (2) the dynamic model, and (3) the reconfiguration model. A powerful work domain modeling tool called Function-Behavior-Structure (FBS) is employed for developing the work domain model of the WCDMA system. Petri-Net theory, as well as its formalization, is applied to develop the dynamic model of the WCDMA system. A concept in engineering design called the general and specific function concept is applied to develop a new approach to system reconfiguration for the high survivability of the system. These models are implemented along with a user-interface which can be used by emergency management personnel. A demonstration of the effectiveness of this study approach is included.<p>There are a couple of contributions with this thesis study. First, the proposed approach can be added to contemporary telecommunication management systems. Second, the Petri Net model of the WCDMA system is more comprehensive than any dynamic model of the telecommunication systems in literature. Furthermore, this model can be extended to any other telecommunication system. Third, the proposed system reconfiguration approach, based on the general and specific function concept, offers a unique way for the survivability of any service provider system.<p>In conclusion, the ontology-based paradigm for a service system management provides a total solution to service continuity as well as its emergency management. This paradigm makes the complex mathematical modeling of the system transparent to the manager or managerial personnel and provides a feasible scenario of the human-in-the-loop management.

In the Service Oriented Architecture (SOA) services are computational elements that are published, discovered, consumed and aggregated across platform and organizational borders. The most commonly used technology to achieve SOA are Web Services (WSs). This is due to standardization process (WSDL, SOAP, UDDI standards) and a wide range of available infrastructure and tools. A very interesting aspect of WSs is their composeability. WSs can be easily aggregated into complex workflows, called Composite Web Services (CWSs). These compositions of services enable further reuse and in this way new, even more complex, systems are built.<p>Although there are many languages to specify or implement workflows, in the service-oriented systems BPEL (Business Process Execution Language) is widely accepted. With this language WSs are orchestrated and then executed with specialized engines (like ActiveBPEL). While being very popular, BPEL has certain limitations in monitoring and optimizing executions of CWSs. It is very hard with this language to adapt CWSs to changes in the performance of used WSs, and also to select the optimal way to execute a CWS. <p>To overcome the limitations of BPEL, I present a model-aware approach to execute CWSs. To achieve the model awareness the Coloured Petri Nets (CPN) formalism is considered as the basis of the execution of CWSs. This is different than other works in using formal methods in CWSs, which are restricted to purposes like verification or checking of correctness. Here the formal and unambiguous notation of the CPN is used to model, analyze, execute and monitor CWSs. Furthermore this approach to execute CWSs, which is based on the CPN formalism, is implemented in the model-aware middleware. It is also demonstrated how the middleware improves the performance and reliability of CWSs.

In this dissertation, the artificial intelligent Petri nets is applied to find the optimal switching operation for service restoration and feeder loading balance for 18-feeders distribution systems that containing the whole 24-hours load profiles of service zones. After the fault location has been identified and isolated for a system fault contingency, the Petri nets model with inference mechanism is derived and applied to solve the optimal load transfer among distribution feeders. For system normal operation condition, the load balancing among distribution feeders is obtained by the Petri nets model to enhance the operation efficiency of distribution systems. The switching operation, which will result in the loading balance among distribution feeders, is derived by the Petri nets model according to the loading cost of distribution systems. To determine the effectiveness of the proposed methodology, a Taipower (Taiwan Power Company) distribution system which serves a mixed types of customers is selected to perform the computer simulation. It is found that the Petri nets approach can enhance the solution process of fault restoration with proper load transfer and improve feeder load balance for distribution systems by considering the load characteristics of the service customers.

This dissertation has focused on automated power system fault analysis. New contributions to fault section estimation, protection system performance evaluation and power system/protection system interactive simulation have been achieved. Intelligent techniques including expert systems, fuzzy logic and Petri-nets, as well as data from remote terminal units (RTUs) of supervisory control and data acquisition (SCADA) systems, and digital protective relays have been explored and utilized to fufill the objectives. The task of fault section estimation is difficult when multiple faults, failures of protection devices, and false data are involved. A Fuzzy Reasoning Petri-nets approach has been proposed to tackle the complexities. In this approach, the fuzzy reasoning starting from protection system status data and ending with estimation of faulted power system section is formulated by Petri-nets. The reasoning process is implemented by matrix operations. Data from RTUs of SCADA systems and digital protective relays are used as inputs. Experiential tests have shown that the proposed approach is able to perform accurate fault section estimation under complex scenarios. The evaluation of protection system performance involves issues of data acquisition, prediction of expected operations, identification of unexpected operations and diagnosis of the reasons for unexpected operations. An automated protection system performance evaluation application has been developed to accomplish all the tasks. The application automatically retrieves relay files, processes relay file data, and performs rule-based analysis. Forward chaining reasoning is used for prediction of expected protection operation while backward chaining reasoning is used for diagnosis of unexpected protection operations. Lab tests have shown that the developed application has successfully performed relay performance analysis. The challenge of power system/protection system interactive simulation lies in modeling of sophisticated protection systems and interfacing the protection system model and power system network model seamlessly. An approach which utilizes the "compiled foreign model" mechanism of ATP MODELS language is proposed to model multifunctional digital protective relays in C++ language and seamlessly interface them to the power system network model. The developed simulation environment has been successfully used for the studies of fault section estimation and protection system performance evaluation.