(User-friendly) formal requirements verification in the context of ISO26262

In order to achieve the highest safety integrity levels, ISO26262 recommends the use of formal methods for various verification activities, throughout the lifecycle of safety-related embedded systems for road vehicles. Since formal methods are known to be difficult to use, one of the main challenges raised by these ISO26262 requirements is to find cost-effective approaches for being compliant with them. This paper proposes an approach for requirements formal verification where formal methods, languages, and tools are only minimally exposed to the user, and are integrated into one of the commonly used system modeling environments based on SysML. This approach does not require particular expertise in formal methods still allowing to apply them. Hence, personnel training costs and development costs should be kept limited. The proposed approach has been implemented as a plugin of the Topcased environment. Although it is limited to discrete system models, it has been successfully experimented on an industrial use case.