Integration of Formal Methods and Testing for Model-based Systems Engineering

NII Shonan Meeting:

@ Shonan Village Center, December 1-4, 2014

NII Shonan Meeting Report (ISSN 2186-7437): No.2014-16


  • Tetsuya Tohdo, DENSO CORPORATION, Japan
  • Werner Damm, Carl von Ossietzky Universität Oldenburg, Germany
  • Alexander Pretschner, Technical University of Munchen, Germany
  • Jun Sun, Singapore University of Technology and Design, Singapore

Overview048_Group Photo

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
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