This meeting aims to provide a forum for researchers and practitioners working on Formal Methods (FM) and Testing to identify research issues toward bringing related ideas, techniques, theories and tools in the both research areas to real industrial solutions.

The critical systems manufactured in automobile, railways and avionics need to be designed, developed, operated and maintained with high-level of confidence, and to keep evolving to adapt ever-changing environments, and responding to new demands in a timely manner with high productivity. Observing the industry, so called “Semi-Formal” approaches are widely taken with the use of executable models (the notable example is Simulink widely used in the automotive industry) in conjunction with the use of traditional Testing methods instead of formal techniques. While the adoption of results in Formal Methods research is gaining momentum, there continue to be gaps between practical industry needs and academic achievements. Among others, these gaps reflect concerns with return-on-investment, scalability, practicality, educational challenges, and the seamless embedding of methods and tools into an ever changing landscape of development processes.

This current situation motivates us to organize this meeting.
Model-based engineering approach based on the use of modeling descriptions with formal mathematical semantics (as used in FM) in combination with Testing is considered to be one of the best practical solutions over the system-lifecycle to ensure high level of confidence without decreasing productivity. However, the best way of combining FM and Testing techniques is not obvious, and we believe that there are numerous research issues on this approach. The main purpose of this meeting is to recognize and identify research issues which need to be solved in order to develop engineering methods which effectively combines FM and Testing theories, techniques and tools.

This forum has a strong focus on collaboration between academia and industry in order to foster further development of this cutting-edge technology and aims to establish a strong tie between academia and industry especially to Japanese industry. In order to make this happen, we carefully selected invitees from academia who are working on systems engineering, foundational theories between Testing and Formal Methods, and principal researchers conducting research projects on embedded systems, systems engineering and verification, and practitioners who are practicing verification in model-based systems engineering.

Some of the issues we would like to address at this meeting may include but not limited to the followings:

• Test case generation using formal proofs and model checking
• Unified theory of Testing and Formal Methods which underpins both technique in a single framework,
• Contractual framework for specification, design and verification
• Combination of static analysis and dynamic analysis/testing
• Testing and symbolic verification
• Approximation and abstract interpretation
• Refinement calculus and Testing
• Requirement-based verification
• Model-based testing
• Runtime Verification