The design of digital systems is getting more complex with rapid improvements in VLSI design which can accommodate many millions of gates in one integrated chip (IC). Additionally, the speed with which the design is completed is also becoming significant due to the demands of the market for the ICs. Tools to automate the initial design process can make the designer's task simpler and more accurate. The ASPIN system being built at Virginia Polytechnic Institute and State University focuses on deriving a synthesizable model for a digital system from various kinds of informal specifications( e.g. natural language descriptions, flowcharts, block diagrams, timing diagrams). This thesis describes an interactive tool for validating and correcting formal models acquired from natural language specifications of digital system. Validation is important since the formal models have to be devoid of any ambiguities which might be present in the natural language specifications. The information acquired from the specifications is stored in an intermediate graphical notation called conceptual graphs. A preliminary tool called the Model Generator can produce a graphical display from conceptual graphs which helps the user visualize the model contained in the conceptual graph. The Back Annotator which is described in this thesis lets the user correct any misinterpretations by making changes to the graphical display such as additions, deletions, modifications, and movement / Master of Science