Runtime monitoring of state machines : formalism and analysis.
Published: 2005
Language: eng
Number of pages: 94
ISBN-13: 9780494164051
Description: Runtime verification is the process of checking that a program conforms to temporal behavioural specifications while it is running. It scales better than model checking; however, unlike model checking, which can prove the absence of an error, runtime verification can only prove its presence. This makes runtime verification useful for detecting safety properties. Business State Machines (BSM) is a new language developed by IBM to create distributed, web-based applications. In this thesis we attempt to support formal verification of BSM in two ways. First, we provide a formal model describing the semantics of a single machine. This facilitates the analysis and verification of a machine using a model checker. Second, we analyze the requirements of a framework for runtime verification of multiple machines. We describe and compare three different approaches to monitoring BSM programs.
Notes: Source: Masters Abstracts International, Volume: 44-06.

Thesis (M.A.Sc.)--University of Toronto, 2005.

Electronic version licensed for access by U. of T. users.

ROBARTS MICROTEXT copy on microfiche.