National institute of Technology，Okinawa College

Chikatoshi Yamada, Department of Information and Communication Systems Engineering, National Institute of Technology, Okinawa College

I stayed at the University of Victoria (UVic) in Canada for one year and studied on Model Checking of system designs.

Model checking is an important step in the design and verification of finite state machine specifications. In this research, I considered testing the reachability of a nondeterministic machine. I developed tool chains for model checking nondeterministic machines using the well-known SPIN model checking tool. Moreover, I considered reachability property, but the approach was applicable for other properties that can be checked by SPIN such as liveness and deadlock properties.

The machines are initially specified as Matlab/Simulink Stateflow models. The Stateflow model does not fully support nondeterministic behavior. If two outgoing transitions of a state are valid at the same time, one of them will be selected in a deterministic way using the so-called Stateflow 12 o'clock rule. However, if the system has valid nondeterministic behaviors this approach can lead to invalid results. In addition, Matlab/Simulink can not verify certain properties such as reachability, liveness and deadlock. Hence in this research, I explored the ways to use other tools to properly analyze nondeterministic behavior.

My first tool translates the XML description produced by Simulink to an intermediate specification. I then considered two approaches, one from the literature and our new tool, for translating that specification to a PROMELA language specification that can then be checked using SPIN model checking tool. I also showed how a three-valued abstraction applied to the intermediate language specification can improve the efficiency of these approaches.

Existing tools and languages as well as new tools developed for this work are used. I have developed translation tools from XML to Prism or PROMELA. Moreover, I used a three-valued abstraction to reduce the complexity of the model checking.

I reported these results of my research in the following conferences:
1. The 46th IEEE International Symposium on Multiple-Valued Logic 2015 (Waterloo, Canada), May 2015.
2. The 14th IEEE/ACIS International Conference on Computer and Information Science 2015 (Las Vegas, USA), July 2015.
3. IEEE TENCON 2015 (Macau, China), November 2015.
I reported these results of my research to following conferences:
1. The 46th IEEE International Symposium on Multiple-Valued Logic 2015 (Waterloo, Canada), May 2015.
2. The 14th IEEE/ACIS International Conference on Computer and Information Science 2015 (Las Vegas, USA), July 2015.
3. IEEE TENCON 2015 (Macau, China), November 2015.

This work was undertaken while I was a Visiting Scholar at the University of Victoria in Canada. I would like to thank Professor D. Michael Miller and Dr. Sudhakar Ganti for their technical supports and many pieces of valuable advice.

Courtyard on University of Victoria

Downtown of Victoria (Summer)

Downtown of Victoria (Winter)