Date of Graduation


Document Type


Degree Type



Statler College of Engineering and Mineral Resources


Lane Department of Computer Science and Electrical Engineering

Committee Chair

Bojan Cukic.


Software engineering community is well aware of the usefulness of formal methods for specifying, designing and testing of the software. Despite this testing literature rarely deals with specification based testing. Testing from formal specifications offers a simple, structured and more rigorous approach to the functional tests than testing techniques. An important application of specification in testing is providing test oracles. The rise of use of computers in control safety critical systems, i.e., flight control systems, necessitates that rigorous system testing is performed before the deployment. In flight control systems, requirements are mostly concerned with the safety and maneuverability of an aircraft. In this domain, the use of formal approaches to requirements specification and system verification is strongly encouraged. In our study relational notation was used to model the requirements of generic flight control system. The advantage of relational approach is that the requirements can be partitioned into less complex components. Each component is separately specified with a set a relations. The formal aspect of the relational notation is exploited in a verification framework where the specifications are used as an oracle to test a system implementation.