Eliminating navigation errors in web applications via model checking and runtime enforcement of navigation state machines