Date of Award

12-1992

Document Type

Thesis

Degree Name

Master of Science

Department

Department of Electrical and Computer Engineering

First Advisor

Kim Kanzaki, PhD

Abstract

We develop a methodology for formalizing, verifying, and validating the requirements specification of real-time systems based on a graphical and formal hierarchical Finite State Machine (FSM) language Reacto. We define a means to quantify time and express real-time constraints in Reacto and a transformation from Reacto to the Very High Speed Integrated Circuit (VHSIC) hardware Description Language (VHDL). Reacto's high level abstractions, graphical nature, and theorem prover produce efficient, accurate, and easily understood specifications. We use VHDL's event driven simulation capability, concurrency, and temporal operators to thoroughly examine temporal dependencies between the state machine transitions, and to increase simulation power by simulating multiple communicating FSMs. We apply the methodology to two example problems, a cruise control, and a lift (elevator) controller. We verify that the state machine specification is consistent and validate the specification using executable simulations in both Reacto and VHDL. We evaluate the methodology against criteria for real-time specification languages and conclude that Reacto and VHDL complement each other well. Together, they abstract the real world well, are clearly understood, verify that the specification and implementation are consistent, axe easy to modify, allow requirements tracing, and finally, support specification of concurrency and timing constraints.

AFIT Designator

AFIT-GCS-ENG-92D-24

DTIC Accession Number

ADA259224

Comments

The author's Vita page is omitted.

Download

Share

COinS