NDAUTO: An Experimental Software Automation System

This paper describes the design and implementation of an experimental software automation system (NDAUTO). By combining the transformational and procedural approaches in software automation, the system can transform software functional specifications written in a graphical specification language GSPEC to executable programs automatically. The equivalence between a specification and its corresponding program can be guaranteed by the system, and the correctness of the specification can also be validated. The main new points of the work lie in the design of the specification language, the transformation mechanism and the correctness validation of the specification.