Title: Formal Methods for Model-Based Testing Abstract: The use of formal system speci fications makes it possible to automate the derivation of test cases from speci fications. This allows to automate the whole testing process, not only the test execution part of it. This talk presents the state of the art and future perspectives in testing based on formal methods. The theory of formal testing is briefly outlined, a test tool is presented which automates both test derivation and test execution on-the-fly, and an application case study is discussed.