Formal specifications for an electrical power grid system stability and reliability
Galinski, Jonathan J.
MetadataShow full item record
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.
RightsThis 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.
Showing items related by title, author, creator and subject.
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 ...
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 ...
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 ...