Expert systems (Computer science)

Web Service Business Process Execution Language (BPEL) has become a standard language in the world of Service Oriented Architecture (SOA) for specifying interactions between internet services. This standard frees developers from low-level concerns involving platform, implementation, and versioning. These freedoms risk development of less robust artifacts that may even become part of a mission-critical system. Model checking a BPEL artifact for correctness with respect to temporal logic properties is computationally complex, since it requires enumerating all communication and synchronization amongst various services with itself. This entails modeling BPEL features such as concurrency, hierarchy, interleaving, and non-deterministic choice. The thesis will provide rules and procedures for translating these features to a veriable model written in Promela. We will use these rules to build a program which automates the translation process, bringing us one step closer to push button verification. Finally, two BPEL artifacts will be translated, manually edited, verified, and analyzed.

Design of intelligent systems that can learn from the environment and adapt to the change in the environment has been pursued by many researchers in this age of information technology. The Group Method of Data Handling (GMDH) algorithm to be implemented is a multilayered neural network. Neural network consists of neurons which use information acquired in training to deduce relationships in order to predict future responses. Most software tool during the simulation of the neural network based algorithms in a sequential, single processor machine like Pascal, C or C++ takes several hours or even days. But in this thesis, the GMDH algorithm was modified and implemented into a software tool written in Verilog HDL and tested with specific application (XOR) to make the simulation faster. The purpose of the development of this tool is also to keep it general enough so that it can have a wide range of uses, but robust enough that it can give accurate results for all of those uses. Most of the applications of neural networks are basically software simulations of the algorithms only but in this thesis the hardware design is also developed of the algorithm so that it can be easily implemented on hardware using Field Programmable Gate Array (FPGA) type devices. The design is small enough to require a minimum amount of memory, circuit space, and propagation delay.

Preventing bad things from happening to engineered systems, demands improvements to how we model their operation with regard to safety. Safety-critical and fiscally-critical systems both demand automated and exhaustive verification, which is only possible if the models of these systems, along with the number of scenarios spawned from these models, are tractably finite. To this end, this dissertation ad dresses problems of a model's tractability and usefulness. It addresses the state space minimization problem by initially considering tradeoffs between state space size and level of detail or fidelity. It then considers the problem of human interpretation in model capture from system artifacts, by seeking to automate model capture. It introduces human control over level of detail and hence state space size during model capture. Rendering that model in a manner that can guide human decision making is also addressed, as is an automated assessment of system timeliness. Finally, it addresses state compression and abstraction using logical fault models like fault trees, which enable exhaustive verification of larger systems by subsequent use of transition fault models like Petri nets, timed automata, and process algebraic expressions. To illustrate these ideas, this dissertation considers two very different applications - web service compositions and submerged ocean machinery.

Web services intend to provide an application integration technology that can be successfully used over the Internet in a secure, interoperable and trusted manner. Policies are high-level guidelines defining the way an institution conducts its activities. The WS-Policy standard describes how to apply policies of security definition, enforcement of access control, authentication and logging. WS-Trust defines a security token service and a trust engine which are used by web services to authenticate other web services. Using the functions defined in WS-Trust, applications can engage in secure communication after establishing trust. BPEL is a language for web service composition that intends to provide convenient and effective means for application integration over the Internet. We address security considerations in BPEL and how to enforce them, as well as its interactions with other web services standards such as WS-Security and WS-Policy.