Verification of Formal Requirements in the Context of ISO-26262

Organisation:	Politecnico di Torino and Centro Ricerche Fiat (CRF), Torino (ITALY)
Functionality:	System Design
Tools used:	Topcased CADP (Construction and Analysis of Distributed Processes) / TGV
Period:	2019-2020
Description:	The ISO-26262 standard is related to safety critical systems within road vehicles and it applies to a complete automotive safety lifecycle: management, development, production, operation, service, and decommissioning. It provides an automotive-specific risk-based approach to determine the Automotive Safety Integrity Levels (ASIL), a risk classification scheme for analyzing and classifying the impact of a particular potential hazard. During the various product development phases, ISO-26262 recommends the use of various specification and verification techniques, especially when dealing with items classified at the highest ASIL levels. The most relevant recommendations about formal methods refer to the left-hand side of the V models, where formal specification is recommended for the description of safety requirements and system designs at different abstraction levels, while formal verification is recommended for upwards design phase validation. However, the application of formal methods in industry is still hampered by their reputation of being hard-to-use and very time consuming, therefore onerous from an economic standpoint. To facilitate the usage of formal methods in the automotive domain, this work proposes a modeling approach that does not require sophisticated skills in formal methods and is tailored on concepts that industry people are already aware of and familiar with (e.g., state machines, activity and sequence diagrams, etc.). The input language considered is SysML, which is widely known and accepted in the automotive industry. A valuable feature of SysML is its ability to specify hierarchical requirements with associated behavioral models, thus enabling the management of safety requirements according to the ISO-26262 recommendations and at the same time the formal specification of requirements through such behavioral models. The formal models extracted from the SysML descriptions are then used for test generation based on requirements. A tool chain for model-based testing was built as a plugin to the Topcased environment. The SysML descriptions are translated first to CSP and then to LOTOS, one of the input languages of CADP. Test purposes are produced automatically (and possibly modified manually by the user if necessary) and used by the TGV tool of CADP to generate test cases. The tool chain was evaluated on a case study proposed by CRF within the VeTeSS (Verification and Testing to Support Functional Safety Standards) European Project. The case study was an electric gear selector, which provides mechanical locking or unlocking of the transmission when the parking mode is selected (by the driver or automatically), avoiding unwanted movement of the vehicle when stopped.
Conclusions:	The proposed methodology hides the complexity of formal notations and therefore improves usability. The case study demonstrated that a team of engineers from CRF without specific training in formal methods have successfully performed safety requirements specification and verification. The proposed approach was evaluated feasible and user friendly enough by the engineers, also showing adequate performance of the automated tools employed.
Publications:	[Makartetskiy-Marchetto-Sisto-et-al-20] Denis Makartetskiy, Guido Marchetto, Riccardo Sisto, Fulvio Valenza, Matteo Virgilio, Denise Leri, Paolo Denti, and Roberto Finizio. "(User-friendly) formal requirements verification in the context of ISO26262". Engineering Science and Technology, an International Journal 23(3):494-506, June 2020. Available on-line at: https://doi.org/10.1016/j.jestch.2019.09.005 or from the CADP Web site in PDF or PostScript
Contact:	Fulvio Valenza Dipartimento di Automatica e Informatica Politecnico di Torino corso Duca degli Abruzzi 24 Torino I-10129 ITALY Email: fulvio.valenza@polito.it
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page