| The process and tools for designing time-triggered high-confidence embedded systems should encompass as many useful aspects of a system's behavior as possible in order to create a more comprehensive understanding of the system. The research presented in this thesis is not intended to capture every detail of these systems, but instead aims for a subset of behaviors that are of use to system designers. This research, in conjunction with other research being conducted on ESMoL, provides a useful theoretical basis and a set of practical modeling tools for high-confidence time-triggered embedded systems. |