Huus, Jan.2009-03-232009-03-2319921992Source: Masters Abstracts International, Volume: 32-01, page: 0276.9780315800113http://hdl.handle.net/10393/7759http://dx.doi.org/10.20381/ruor-6953Protocol validation has traditionally focused on detecting errors defined in terms of global states. A complementary approach is to analyze the process languages of a protocol, where a process language is defined as the set of executable event sequences of a process in the protocol. A general property of a process is "effectiveness", defined as the absence of unexecutable specified event sequences. A method is given for determining whether a specified process (the "host process") in a protocol is effective. The method involves generating a process language's finite state machine representation, called a process event graph (PEG). Every PEG node maps to a global state. Using the given method to generate a PEG, it is shown that, when the PEG generation does not detect error states, every reachable global state is reachable from a PEG node by an event sequence that does not include any host events. This introduces the possibility of a parallel approach to reachability analysis, in which a PEG is generated, and then a "local" reachability analysis is performed from each PEG node in parallel, ignoring host events. Other applications of PEGs are also given.96 p.Computer Science.Thesis