Maksym Tkach

Date of Award

January 2020

Document Type


Degree Name

Master of Science (MS)


Computer Science

First Advisor

Emanuel Grant


This thesis uses formal specification techniques to analyze and model a microgrid. A microgrid is a small, local electrical grid, often supplied by a single generator, that can connect to the larger electrical grid, but can also disconnect from it, going into “island mode.” Thanks to the growth in renewable energy, microgrids represent a growing segment of the electrical power generation domain. And like any member of the domain they are safety-critical systems, meaning that even a small mistake in their implementation risks damage to life and property.Formal specification is a way to abrogate the risks of safety critical systems by ensuring that the system under consideration is fully described, modeled, and analyzed prior to implementation, and the description and model are robust and error-free. However, at present there is no established approach to the use of formal specification techniques of microgrid systems. This thesis proposes a specification that can serve as a foundation for future work in the microgrid domain as well as an aid to communication about microgrids. The work uses Unified Modeling Language (UML) graphical notation and an accompanying Object Constraint Language (OCL) formal specification. The model transformation accomplished through the use of Iterative Development techniques is outlined in detail to serve as a guide to future researchers.