Politecnico di Torino and Centro Ricerche Fiat (CRF), Torino (ITALY)
CADP (Construction and Analysis of Distributed Processes) / TGV
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.
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.
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 our FTP site in PDF or PostScript
Dipartimento di Automatica e Informatica
Politecnico di Torino
corso Duca degli Abruzzi 24
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|