A model-based mutation testing (MBMT) approach enables to perform negative testing where test cases are generated using mutant models containing intentional faults. This paper introduces an alternative MBMT framework using pushdown automata (PDA) that relate to context-free (type-2) languages. There are two key ideas in this study. One is to gain stronger representational power to capture the features whose behavior depends on previous states of software under test (SUT). The other is to make use of a relatively small test set and concentrate on suspicious parts of the SUT by using MBMT approach. Thus, the proposed framework includes (1) a novel usage of PDA for modeling SUT, (2) novel mutation operators for generating PDA mutants, (3) a novel coverage criterion, and an algorithm to generate negative test cases from mutant PDA. A case study validates the approach, and discusses its characteristics and limitations.