Formal specifications for an electrical power grid system stability and reliability
Author
Galinski, Jonathan J.
Date
2015-09Advisor
Drusinsky, Doron
Second Reader
Shing, Man-Tak
Metadata
Show full item recordAbstract
This thesis provides natural language requirements and associated formal specifications for an electric power grid. These specifications are the first step in using bounded constraint solving to detect early bleak states in an electric power grid system. We analyze several methods of software verification and validation including Theorem Proving, Model Checking, and Execution-based Model Checking before determining that Execution-based Model Checking is the most suitable for specifying properties of a power grid. The requirements and specifications are broken into four categories: undesirable events, downward trends, failure to recover, and undesirable fluctuations. All specifications are focused on system stability and reliability as indicated by system frequency and operating in a secure N-1 state. Specifications from three out of the four categories were tested to ensure they meet the spirit and letter of the natural language requirements while eliminating ambiguity inherent to natural languages. Finally, we show how a Hidden Markov Model can be used to perform run-time monitoring in the presence of hidden states, thereby enabling run-time monitoring of systems where monitored artifacts are not all perfectly visible.
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.Collections
Related items
Showing items related by title, author, creator and subject.
-
The application of a viewpoints framework in the development of C4I systems
Smith, Sheila A. (Monterey, California. Naval Postgraduate School, 2000-06);In the development of large distributed systems, both the detection and resolution of inconsistency in policy, requirements, and specifications pose major challenges. The purpose of this thesis is to examine the inconsistencies ... -
Reusable software component retrieval via normalized algebraic specifications
Steigerwald, Robert Allen (Monterey, California. Naval Postgraduate School, 1991-12);Efforts in the software engineering community to reuse code are hampered by a lack of tools. Reusability is particularly beneficial in a rapid prototyping environment. Rapid prototyping with automated reusable software ... -
Specification and Validation of Space System Behaviors
Raque, Steven; Drusinsky, Doron (Monterey, California. Naval Postgraduate School, 2010-02-02); NPS-CS-10-002The NASA Independent Verification and Validation (IV&V) Facility is using formal specification techniques for the IV&V of the flight software for several upcoming missions. Such formal specifications are typically created ...