A confirmation review of the safety plan is required during compliance assessment with ISO 26262. Its production could be facilitated by creating a specification of the standard's requirements in FCL (Formal Contract Logic), which is a language that can be used to automatically checking compliance. However, we have learned, via previous experiences, that interpreting ISO 26262 requirements and specifying them in FCL is complex. Thus, we perform a formalization-oriented pre-processing of ISO 26262 to find effective ways to proceed with this task. In this paper, we present the lessons learned from this pre-processing which includes the identification of the essential normative parts to be formalized, the identification of SCP (Safety Compliance Patterns) and its subsequent documentation as templates, and the definition of a methodological guideline to facilitate the formalization of normative clauses. Finally, we illustrate the defined methodology by formalizing ISO 26262 part 3 and discuss our findings.
A confirmation review of the safety plan is a piece of evidence required for compliance
assessment with ISO 26262 [
In our previous work [
The rest of the paper is structured as follows. In Section 2, we present essential background. In Section 3, we describe the formalization-oriented pre-processing of ISO 26262. In Section 4, we illustrate the methodological guideline derived from the pre-processing of ISO 26262. In Section 5, we discuss our findings. In Section 6, we present related work. Finally, in Section 7, we present conclusions and future work. 2
This section presents the background required in this paper. Section 2.1 recalls
essential information related to ISO 26262. Section 2.2 recalls the basis of Formal Contract
Logic. Finally, Section 2.3, recalls Safety Compliance Patterns.
2.1 ISO 26262
ISO 26262 [
The description of the phases of the safety process is distributed in clauses included
in the nine normative parts starting from Clause 5. Each of these clauses states its
Objectives, which describe the generic goals of the clause, General information, which
gives an overall explanation of the clause, Inputs of the clause, i.e., prerequisites,
Requirements and Recommendations (R&R), which describe the specific conditions that
the process should fulfill, and the Work products, which are the mandatory deliverables.
Notes and Examples are expected to help the applicant in interpreting the requirements.
We focus on a subset of requirements from ISO 26262 part 3 presented in Table 1,
which specifies the requirements for the concept phase for automotive applications.
7.4.4 Determination of ASIL and safety goals - The safety requirements shall be specified by an appropriate combination
of the methods as presented in the table (H means Highly and R means Recommended).
Formal Contract Logic (FCL) [
c = Normative effect.
Normative effects trigger deontic notions, namely, Obligations, Prohibitions, and
Permissions. An Obligation is a statement describing a mandatory situation. In FCL, an
obligation is represented by the operator [O] plus a proposition, which corresponds to
the content of the obligation. FCL is equipped with different kind of obligations, which
depend on the timing of the application of the normative provision and their persistence
after a violation (see [
Safety compliance patterns (SCP) [
Our initial efforts to formalize ISO 26262 into FCL (see our previous work [
As presented in Section 2.1, ISO 26262 has nine normative parts. In each of the normative parts, Clauses 1, 2 and 3 are not required to be formalized since the text does not represent a constraint to the development process. Clause 4 is subdivided into two items. Item 4.1, which title is General requirements, describes the tailoring of safety activities, namely its application in a way different to the indicated by the standard. Item 4.2, which title is Interpretation of tables, illustrate the way in which normative methods listed in tables (with consecutive and alternative entries) should be applied. By themselves, these two requirements are not directly constraining the process. However, they shape the way in which other requirements should be applied. Therefore, Clause 4 is an essential structure that gives important elements for the formalization process. The specific normative clauses that describe the phases of the safety process are documented from Clause 5 in each of the nine normative parts. In those clauses, the title represents the initiation of the phase. Therefore, the title is part of the formalization process. However, the formalization of the title must be preceded by the formalization of the Prerequisites, since they represent the preconditions constraining the initiation of the particular phase. Prerequisites as well as Work products are essential since they are part of the description of the safety process which is expected to be represented via a model embracing input/output elements. The presence of the verbs shall and must in the section R&R is an explicit indication of a normative provision that constrains the breakdown of the work as well as for guidance on how it should be planned and executed. Information under the titles Objectives, General, Notes and Examples are not formalized since they do not prescribe the process to be adopted. However, these elements can be used to provide context for the application of the requirements.
Within the essential normative parts of ISO 26262, seven SCP are identified. In Clause 4, the provision of a rationale is done in the same way whenever a safety activity is tailored. Similarly, the applicable methods that are described in tables with alternative entries and tables with consecutive entries. Therefore, Clause 4 describes three repetitive structures. Within the description of the phases of the safety process, represented from clause 5 in each of the normative parts, other three repetitive structures are easily recognizable. The first one is the Initiation of a phase, which is recognized in the title of every clause. The second repetitive structure corresponds to the Prerequisites, which describe the preconditions of the phase. Similarly, the Work products, which are defined as the result of safety activities, represent a third repetitive structure. Since R&R contains many requirements, and each one describes a different structure, we cannot consider this structure as repetitive itself (even though we can find the title R&R in all the normative parts). However, inside the R&R one repetitive structure, called Guidance, is recognized. A requirement, which we call the main normative effect, contains guidance when it is accompanied by a list of descriptive items ( a, b,..., n). Together, those items provide additional normative descriptions about the main normative effect, and therefore, they also become mandatory requirements. 3.3
For each SCP, we provide a general formalization structure in FCL which is derived from the interpretation of the repetitive structure it represents (as described in Section 2.3). The rules in the template contains the symbol # between brackets (f g), which should be replaced with the identification of the requirement that the rule is representing. The space between the brackets in the rule statement (f g) is a placeholder for the particular instantiation of the template.
Provision of a rationale: A rationale implies compliance with conditions. For being valid, it should be always verified by an expert. Therefore, when a rationale is attached to a safety process, its verification is obligated (see Template 1). rf#:gattachfRationaleg ) [O]veri f yByExpertfRationaleg (1) Alternative entries: The normative provision for tables with alternative entries obliges the verification of the ASIL, the provision of a combination of the listed methods and a the provision of a weak rationale. The combination of these methods also obliges the inclusion of those marked with the highest recommendation level. The provision of other methods is also possible if a strong rationale is provided. There is an inconsistency between rules rf#.a:gand rf#.g:g. Thus, a superiority relation that gives priority to rf#.g:g (which describes an exception for the requirement) is provided (see template 2).
rf#.a:gveri f yfASILg ) [O]provideCombinationO f ListedMethods rf#.b:gprovideCombinationO f ListedMethods ) [O]includefHigherRecommendedNotationsForASILg rf#.c:gincludefHigherRecommendedNotationsForASILg ) [O]attachWeakRationaleSupportingListedMethods rf#.d:gattachWeakRationaleSupportingMethods ) [O]Veri f yWeakRationaleByDomainExpert rf#.e:gincludeNotListedMethodsfOtherMethodsg ) [O]atachStrongRationaleSupportingfOtherMethodsg rf#.f:gatachStrongRationaleSupportingfOtherMethodsg ) [O]veri f yStrongRationaleByDomainExpertfOtherMethodsg rf#.g:gincludeNotListedMethodsfOtherMethodsg; [O]atachStrongRationaleSupportingfOtherMethodsg; veri f yStrongRationaleByDomainExpertfOtherMethodsg ) [P] provideCombinationO f T heListedMethods rf#:gg>rf#:ag (2) Consecutive entries: The normative provision for tables with consecutive entries obliges the verification of the ASIL and the utilization of all listed methods. The combination of methods beyond the ones listed in the table is also possible if a strong rationale is provided (see Template 3). There is an inconsistency between rules rf#.a:gand rf#.d:g. Thus, a superiority relation that gives priority to rf#.d:g (which describes an exception for the requirement) is provided (see template 2). rf#.a:gveri f yfASILg ) [O]provideAll f ListedMethods rf#.b:gincludeNotListedMethodsfotherMethodsg ) [O]atachStrongRationaleSupportingfotherMethodsg rf#.c:gattachStrongRationaleSupportingfotherMethodsg ) [O]veri f yStrongRationaleByDomainExpertfotherMethodsg rf#.d:gincludeNotListedMethodsfotherMethodsg; [O]atachStrongRationaleSupportingfotherMethodsg; veri f yStrongRationaleByDomainExpertfOtherMethodsg ) [P] provideCombinationO f T heListedMethods rf#:dg>rf#:ag
(3) Prerequisites: The antecedents of the initiation of a phase are the prerequisites. Therefore, they are obliged before the phase is initiated (see Template 4). Initiation of a phase: The template considers the prerequisites (formalization presented in Template 4) as the conditions of the applicability of the rule which normative conclusion is the initiation of the phase (see Template 5).
rf#:gprovidefprerequisiteAg:::; providefprerequisiteNg ) [O]initiatefTitleClauseg Guidance: Guidance components are the conditions that obliges the provision of the element guided (see formula 6). Work Product: Work products are the result of certain requirements. Therefore, these requirements are presented as antecedents that obliged the provision of the related work product (see Template 7).
r#:providefPreviousObligationsg ) [O]producefWorkProductg (7) 3.4
From the pre-processing tasks described above, we got an understanding of what to formalize and how we could proceed in the formalization process. The parts to formalized are those that determine the safety lifecycle, meaning those clauses that start from Clause 5. To formalize these clauses, we have described a methodological guideline, which we depict in Figure 2. (4) (5)
Initially, the context of the phase should be understood. For this, the reading and analysis of the objectives and the main general information of the clause to be formalized is required. Then, the formalization process initiates with the prerequisites and followed by the title. These two formalizations can be done by following the SCPs called Prerequisites and Initiation of a phase. After, one requirement is selected from the list of R&R. We suggest that the requirements are selected in the order they are presented and that the rules are named following the requirement numeration to ensure consistency and traceability. For instance, if a textual requirement is marked with the label 5.1, the corresponding rule should be called r.5.1. During the formalization of the requirements, SCP templates could be used to facilitate this task. However, if there are no templates, brainstorming sessions are required. The brainstorming session can be carried out in different ways, but the most relevant is that the group takes one requirement at the time, discuss its importance in the compliance process (e.g., related requirements or permits for tailoring), divide the requirement into smaller sentences that have only one idea, and discuss every sentence. If the requirement has to be divided into several rules, the name of the rule has to be named with the number that accompanies the requirement plus a letter, i.e., r.5.1.a, r.5.1.b. Finally, when all requirements available in R&R are covered, the work products can be formalized by using the SCP template called Work Product. The generated rule set should be verified to avoid inconsistencies and typos in the rules since Regorous do not recognize incorrectly formed rule sets. 4
In this section, we illustrate the methodological guideline depicted in Figure 2 by formalizing the requirements provided in Table 1. The formalization starts from clause 5 (see Table 1) providing requirements for the definition and description of the item. There are no prerequisites in this clause. Thus, we continue with the formalization of the title of the phase, which provides the obligation to initiate item definition (see rule r5). Then, we continue with the formalization of requirement 5.4.1, that defines guidance to provide the functional and non-functional requirements for the item definition. This requirements is formalized by using the SCP Guidance in which initially, the components of the guidance should be provided (see rules r5:4:1:a and r5:4:1:b), and then, they integrate the main normative provision (see r5:4:1). When all the requirements are formalized, we proceed with the work products, which are defined in clause 5.5. To formalize a work product, the requirements (in this case specified by clause 5.4) are presented as antecedents, and the work product itself is the normative provision (see r:5:5).
r5: ) [O]initiateItemDe f inition r5.4.1.a:per f ormItemDe f inition ) [O]provideFunctionalConcept r5.4.1.b:per f ormItemDe f inition ) [O]provideOperationalConstraints r5.4.1:provideFunctionalConcept; provideOperationalConstraints
) [O]provideFunctionalAndNonFunctionalRequirements r.5.5:provideFunctionalAndNonFunctionalRequirements ) [O]produceItemDe f inition Clause 6 in Table 1 presents the title of the clause and its inputs. Thus, we only applied the steps related to the formalization of the prerequisites and the title of the clause. The prerequisites were already formalized in clause 5, (see Table 1, Inputs of this clause: item definition in accordance with 5.5.). Therefore, it is only needed the formalization of the title which defines the obligation of performing the phase Initiation of the safety lifecycle after the normative provision produceItemDefinition (see rule r6).
r6:produceItemDe f inition ) [O]initiateInitiationSa f etyLi f eCycle Clause 7, which is related to Hazard analysis and risk assessment, does not mention any inputs for the clause and it is formalized as rule r5 (see rule r7). Two requirements are described in tables. The first requirement refers to a table which has constitutive information. The formalization of this table is done by taking the description of the entries as the antecedent of the rule and its category as the normative provision (see rules r7:4:3:a to 7:4:3:d).
r7: ) [O]per f ormHazardAnalysisAndRiskAssessment r7.4.3.a:descriptionSeverityS0 ) [O]CatergoryNoIn juries r7.4.3.b:descriptionSeverityS1 ) [O]CatergoryLightAndModerateIn juries r7.4.3.c:descriptionSeverityS2 ) [O]CatergorySevereAndli f eT hreateningIn juries
r7.4.3.d:descriptionSeverityS2 ) [O]CatergoryFatalIn juries Clause 7.4.4 is presented in a table with alternative entries. We take into account the selection of methods for ASIL A. As recalled in Section 2.1 for alternative entries the normative provision suggest the obligation to provide a combination of the methods listed in the table (see rule r7:4:4:a), which at the same time obliges the selection of those with higher recommendation level for the ASIL, in this case, Informal Notations (see ruler7:4:4:b). Also, a rationale shall be given that the selected methods comply with the corresponding requirements (see rule r7:4:4:c). If the highest recommended is selected, only a weak rationale (i.e., a less stringent explanation of the selection) must be provided. However, if the highest recommended is not selected, a more elaborated rationale (called strong) should be provided (see rule r7:4:4:e). A domain expert should verify the rationales (strong and weak) (see rule r7:4:4:d and r7:4:4: f ). Providing the strong rationale, its verification and the methods selected, grant the permit of not providing the combinations of the recommended methods (see rule r7:4:4:g).
r7.4.4.a:veri f yASILA ) [O]provideCombinationO f ListedMethods r7.4.4.b:provideCombinationO f ListedMethods ) [O]includeIn f ormalNotations r7.4.4.c:includeIn f ormalNotations ) [O]attachWeakRationaleSupportingListedMethods r7.4.4.d:attachWeakRationaleSupportingMethods ) [O]Veri f yWeakRationaleByDomainExpert
r7.4.4.e:includeNotListedMethods ) [O]atachStrongRationaleSupportingNotListedMethods r7.4.4.f:attachStrongRationaleSupportingNotListedMethods ) [O]veri f yStrongRationaleByDomainExpert r7.4.4.g:includeNotListedMethods; atachStrongRationaleSupportingNotListedMethods; veri f yStrongRationaleByDomainExpert ) [P] provideCombinationO f T heListedMethods r7:4:4:g>r7:4:4:a 5
Interpreting and specifying ISO 26262 requirements in FCL can be time-consuming and error-prone. One reason is that ISO 26262 is a large document with hundreds of requirements, which like many other standards and regulations, are difficult to interpret. The other reason is that FCL is not yet enough known and existing examples (mostly from the business and legal domains) are insufficient to guide the formalization of the normative notions that constrain the processes used in safety-critical development projects. However, the effort invested in the production of formal specifications of safety standards is compensated by several advantages, i.e., deep understanding of its requirements, practical application in development projects, and the provision of an essential input for facilitating automated compliance checking. Therefore, we consider that discovering efficient ways to proceed with the formalization work can boost the usage of this formal language in the compliance tasks in the safety-critical context. In the remainder, we discuss some aspects that were observed during the performing of the formalization-oriented pre-processing of ISO 26262 and the formalization of its part 3. Useful formalization path: As recalled in Section 2.1, ISO 26262 is structured in a specific way. However, not all the structures should be used to obtain the formal specification in FCL. Therefore, performing a pre-processing of ISO 26262 provides us an useful formalization path to follow, i.e., a methodological guideline and SCP templates. Process engineers in the automotive context, who are interested in starting their formalization work with FCL, may find useful this formalization path since it permits to focus on specific tasks and skip some others that may be not relevant in the formalization process. Performing a similar pre-processing of safety standards beyond ISO 26262 may also be useful for increasing and spreading the use of FCL and its potential benefits. Related skills, competencies and responsibilities: In our experience, group brainstorming sessions have facilitated the production of the FCL specifications. In particular, the participation of different kind of experts has provided different views that were important in the discussions performed during the formalization process. We highlight the fact that brainstorming sessions were mainly guided by the certification expert, whose knowledge provided specific details that are of importance for the safety auditor during the safety assessment. The opportunity to have an FCL expert speeded up the formalization and the creation of templates for reuse. However, FCL is not a very known language. Thus, there are not many FCL experts available. Therefore, it is necessary to provide training courses for teaching FCL. The target group for the training may be mainly conformed by process engineers who already have expertise in compliance management.
Tooling: In our current work, the rules were written manually, introducing the
possibility of typos in the syntax of the rules and inconsistencies in the rules statements.
Therefore, the production of our initial FCL specifications resulted in incoherent files
that were not understood by the compliance checker. To solved this issue, edition and
syntactic correctness of the FCL specifications were ensured manually. However,
manual corrections are long and tedious activities. For this reason, we consider that the
provision of tools for supporting the process of writing and verifying rules, as well as
the creation and instantiation of SCP templates should be developed. Part of our work
should also be the provision of these tools.
The collection of experiences distilled from formalization projects is an advisable way
to save time and avoid mistakes in future projects. We can find lessons learned in the
formalization of software engineering standards in [
The use of FCL for supporting compliance management tasks in automotive is a novelty. We did not find yet specific examples or guidelines that apply to the domain. Therefore, the results of the formalization-oriented pre-processing of ISO 26262 documented in this paper may be of interest for process engineers involved in the cars manufacturing. Additionally, we consider that this work can be used as a starting point to derive domain-specific guidance applicable to process-based safety standards beyond ISO 26262. 7
In this paper, we presented the lessons learned from performing a formalization-oriented pre-processing of ISO 26262. Initially, we identify the essential normative structures, namely those structures that define the safety process to be adopted for developing the car’s safety-critical systems. Then, we identified the repetitive structures of the standard that can be considered SCP. With the identified SCP, we create templates to consolidate a reusable knowledge base for future formalization jobs. The knowledge gathered in the pre-processing is used to define a methodological guideline for facilitating the formalization of normative clauses in ISO 26262. We also illustrate the defined methodology by formalizing ISO 26262 part 3 and discussed our findings.
From the discussion presented in Section 5, we consider that one important part of
the future work is the training of process engineers in FCL. Therefore, a course called
Quality assurance - Certification of safety-critical (software) systems3, which is under
construction, will consider an overview of compliance checking and the formalization
of compliance rules with FCL. We also need to optimize the creation and verification of
rule sets. Thus, we are considering the design and development of a pattern-based rule
editor to facilitate rules creation, and rule sets verification. We consider that
methodological guidelines are also needed in other safety-critical domains. Thus, we aim at
studying other safety standards and adapt any required step resulting from their
specificities. This work is also expected to be combined with previously achieved results [
Acknowledgments. This work is supported by the EU and VINNOVA via the ECSEL
JU project AMASS (No. 692474) [