The Feasibility of Automated Feedback-Directed Specification-Based Test Generation: A Case Study of a High-Assurance Operating System.