Scade2Nu: A tool for verifying safety requirements of SCADE models with temporal specifications

SCADE is both a language and a model-based software development environment that can develop systems in safety-critical fields. It is paramount for these systems to satisfy their safety requirements. Although SCADE can verify some properties by its Design Verifier (DV), it cannot verify the unbounded temporal or liveness properties due to its limitation. With the diversification of system application scenarios, these temporal properties also need to be verified to ensure the reliability of the system. In this paper, we concentrate on solving this problem by introducing Scade2Nu, a tool that can transform SCADE state machines into NuSMV input languages. Scade2Nu helps the designer to apply Linear-time Temporal Logic (LTL) and Computational Tree Logic (CTL) formulas as the requirements specifications of SCADE models. With the aid of the NuSMV model checker as well as its verification results, designers can explore more different kinds of properties to further reduce bugs at the requirements phase in the development cycle.