Cyber-physical systems (CPS) such as cars and robots, which behave in the physical world controlled by software, are nowadays ubiquitous. As CPS become more complicated, safety assurance is increasingly important.

Testing is currently the dominant method for safety assurance of CPS. In testing, a system is executed or simulated with test inputs, and we check whether the behavior of the system is safe or not for those inputs. We cannot guarantee the safety of the system for inputs that have not been tested. There is another approach to CPS safety assurance called formal verification. In formal verification, unlike testing, we try to find a guarantee that the behavior of the system is safe for all inputs.

In this workshop, the participants tried a well-known formal verification tool called Spin model checker. To use the Spin model checker, the following two steps are required:
– Modeling the system of interest in Promela language; and

– Writing down the specification (the desired behavior) as a linear temporal logic (LTL) formula.

The purpose of this workshop was to examine the challenges of the second step extensively. For this purpose, the workshop consisted of the following four main steps:
1. Thinking of some systems and providing specifications (in Japanese) that the system should satisfy;

2. Taking a lecture on LTL formula and doing some exercises;
3. Taking a tutorial on Spin model checker and Promela language; and
4. Translating the Japanese specifications provided in the first step, designing a system that satisfies the specifications, and checking that it indeed satisfies the specifications using Spin model checker.

By observing the participants tackling the above four tasks and the feedback from the participants, we successfully identified some concrete challenges in formal specification. We expect that the results will help with developing formal specification tools that could be used in industry in the future.