Date of Award


Degree Type


Degree Name

Doctor of Philosophy


Computer Science

Major Professor

Jesse H. Poore

Committee Members

Kenneth Stephenson, Michael G. Thomason, Lynne E. Parker


Software has become integral to the control mechanism of modern devices. From transportation and medicine to entertainment and recreation, embedded systems integrate fundamentally with time and the physical world to impact our lives; therefore, product dependability and safety are of paramount importance.

Model-based design has evolved as an effective way to prototype systems and to analyze system function through simulation. This process mitigates the problems and risks associated with embedding software into consumer and industrial products. However, the most difficult tasks remain: Getting the requirements right and reducing them to precise specifications for development, and providing compelling evidence that the product is fit for its intended use.

Sequence-based specification of discrete systems, using well-chosen abstractions, has proven very effective in exposing deficiencies in requirements, and then producing precise specifications for good requirements. The process ensures completeness, consistency, and correctness by tracing each specification decision precisely to the requirements. Likewise, Markov chain based testing has proven effective in providing evidence that systems are fit for field use.

Model-based designs integrate discrete and continuous behavior; models have both hybrid and switching properties. In this research, we extend sequence-based specification to explicitly include time, continuous functions, nondeterminism, and internal events for embedded real-time systems. The enumeration is transformed into an enumeration hybrid automaton that acts as the foundation for an executable model-based design and an algebraic hybrid I/O automaton with valuable theoretical properties. Enumeration is a step-wise problem solving technique that complements model-based design by converting ordinary requirements into precise specifications. The goal is a complete, consistent, and traceably correct design with a basis for automated testing.

Files over 3MB may be slow to open. For best results, right-click and select "save as..."