Qualifying archec in a safety project

A safety project has to show that the tools it relies on can be trusted for what it uses them for: ISO 26262-8 §11 for road vehicles, DO-330 (with DO-178C §12.2) for airborne software. archec qualify writes the documents for that, for the archec features you rely on.

archec qualify --list                                   # the use cases
archec qualify --use check,build,gen-c --asil C --dal B -o qualification --html
archec qualify --config qualify.yaml -o qualification   # your choices, with reasons

What it is not. The kit supports a qualification: it does not certify archec, and it is not a qualification by itself. archec is not developed to a safety standard. The classification starts from defaults that assume nothing about your process, so you confirm or change each level with your reasons. The evidence is archec's own test suite, run on archec's own example models. Your assessment, your records of archec in use and the approval of your tool manager are still needed. Check the clauses and tables cited against your edition of the standards.

Where it comes from#

The kit is written from three things, all in the arche-lang checkout at the commit of the archec you use (--repo, by default the checkout archec was built in):

• The self-model, examples/arche-lang. Each use-case of qualification.arche is a way of using archec (UC-GEN-C, --use gen-c). Each requirement on archec that refines a use case is a tool requirement of it. Each test-plan case that verifies a requirement (verification.arche) is a verification case. A case names a test file of npm test ("test/cert.test.js"), or the tests of a file whose names contain a phrase ("test/exporters.test.js › arxml"). test/qualify.test.js checks that every case names a file that exists, and tests that match.
• A run of the tests. By default archec qualify runs the test files of the use cases you chose, with node --test and a reporter of its own, in the checkout, on its dist/ (build it first). It records each test's result, the archec version, the git commit and whether the checkout has local changes, the sha256 of dist/ and the environment (Node.js, OS, CPU). results.json keeps the run. --results results.json writes the kit from a saved run; --no-run writes it with no evidence, marked as such.
• The docs. The known limits of each use case below, and the Limits sections of the docs each use case names, are its known errors.

The documents#

--html writes each document as a page too (index.html for the README). --standard iso26262 or do330 writes only that standard's documents. archec doc --template fills a Word template from a model; the kit's documents are Markdown and HTML, which you can paste into your own templates.

The levels#

ISO 26262-8. A use case's tool impact is TI2 unless a malfunction cannot introduce an error into the item or fail to detect one (TI1). Its tool error detection is TD1, TD2 or TD3, by how confident you are that your process prevents or detects such a malfunction. TI1, or TD1, gives TCL1 (no qualification needed); TI2 with TD2 gives TCL2; TI2 with TD3 gives TCL3. By default each use case is TI2, TD3, so TCL3. The kit claims nothing of your process. The classification lists, per use case, the measures that would justify TD1 or TD2 (reviews, back-to-back tests, archec difftest, compiling with warnings as errors, an independent tool). If you apply them, say so.

DO-330 / DO-178C §12.2. Criterion 1: the output is part of the airborne software and could insert an error (the code generators by default). Criterion 2: the tool automates verification and is used to reduce other processes. Criterion 3: it could fail to detect an error (the checks and analyses by default). With --dal, the TQL follows: criterion 1 gives TQL-1 to TQL-4 for levels A to D. Criterion 2 gives TQL-4 for A and B, TQL-5 for C and D. Criterion 3 gives TQL-5. The kit gives the operational side of DO-330 (TOR and their verification). For TQL-1 to TQL-4 the developer's side is also needed. Most projects verify the generated output instead, which takes the code generator out of criterion 1: say so in the config.

The config#

YAML or JSON:

project: Brake controller
asil: C
dal: B
standards: [iso26262, do330]      # or both (the default), or one
uses:
  check:
    td: TD2
    justification: Every model change is reviewed; the test plans run in Arche on each merge.
  gen-c:
    ti: TI2
    td: TD1
    criterion: 3
    justification: The generated C is unit-tested to MC/DC, run back-to-back with the model (archec difftest), and reviewed.
    detection: CI job c-verify, review checklist RC-12
  cert: {}

uses may also be a list: [check, gen-c] or [{ use: gen-c, td: TD2 }]. --use, --asil, --dal and --standard on the command line add to the config or override it. The exit code is 1 when a test failed. With --strict, it is also 1 when a requirement of a chosen use case is not shown (no test, not run, skipped). It is 2 for a wrong option.

Adding a use case or a requirement#

1. Add the use-case to examples/arche-lang/qualification.arche, and its defaults (impact, criterion, malfunctions, detection measures, docs) to USE_CASES in src/qualify.ts. test/qualify.test.js fails when the two disagree.
2. Write the requirement on archec with refines UC-…, and a case in verification.arche that verifies it and names its tests.
3. Write its known limits below.

Known limits#

The known errors of archec, by use case. The kit copies the ones of the use cases you chose into known-problems.md.

All use cases#

• The evidence is archec's tests on the example models of this repository, not on your models. A construct your model uses and no example does is not covered by it.
• The traces go from use cases to requirements to test files or test names, not to lines of code. A test that passes shows what it asserts, and that may be less than the requirement's text.
• A test that needs an outside tool (a C compiler, cargo, NuSMV, cppcheck, the Arche checkout) is skipped without it. A case whose tests were all skipped does not show its requirement. The outside tools are not qualified by this kit.
• --repo must be the checkout of the archec you use. The configuration index warns when the run's commit or dist/ hashes differ from the tool described.

UC-CHECK#

• Python in do, expect and handler bodies is checked only for the messages and states it names. The rest is checked when Arche runs it.
• The parity with the Arche app's verdicts is tested only when an Arche checkout is beside this one (test/parity.test.js skips otherwise).
• The state-machine checks (unreachable states, dead and shadowed transitions) run no Python. They read a guard only when it is a plain comparison (self.speed < 10, not armed). With any other guard they say less rather than guess, so a dead transition behind such a guard is not reported.

UC-BUILD#

• The project is checked against the Arche schema archec bundles (schemas/). An Arche release with another schema may read it differently: check the project with that release's arche-cli check.

UC-GEN-C#

• A handler body in Python that is not in the action language is left as a TODO in the C, and gen notes it. Code the model does not say is not generated.
• archec difftest compares the C with archec's own simulator, on the parts it simulates. Execution time, scheduling, buses, faults and plants are not compared (see the simulator).
• With no within, eventually and leads to cannot fail at run time, and their monitors are left out (--monitors).
• The C is compiled with -Wall -Wextra -Werror -pedantic in the tests. MISRA C:2012 findings (cppcheck's addon) are reported, and the generated code is not claimed to comply.

UC-GEN-EMBASSY#

• Port and transition deadlines, watchdogs and timeouts are generated in C. The Rust says it does not do them yet.
• A crate generated before priority levels existed does not start the levels, and gen notes it.
• The tests read the generated crate. They build it with cargo only when cargo is installed.

UC-GEN-TESTS#

• A case whose Python step cannot be translated to C is skipped in c-tests, with the reason.
• In C, a case's waits take no time. A body that loops for ever is an error for its case, and the next case still runs.

UC-GEN-ARXML#

• Left out: the data send and receive points of the runnables, units and data constraints. In the field-by-field mapping of a structure, its arrays, optional fields and unions are left out (the signal group is mapped).
• The schema is not redistributed. The ARXML, Classic and Adaptive, is validated against AUTOSAR_00049.xsd only when AUTOSAR_XSD names a copy of it; without it, those tests are skipped. The Adaptive export has not yet been validated against the schema.
• Adaptive: UDP and TCP ports, service discovery timings, E2E, security, persistency and platform health management are not generated. The data types are the Classic ones, not C++ implementation types. A field is made only for a message that crosses both ways, and its getter and setter ids are numbered after the methods. There is one application per process, not one per part. A microcontroller is a Classic ECU, so a service it provides has no provided instance.

UC-GEN-DBC#

• A frame's layout is the codec's (layout.ts), or the wire format the message writes. A DBC tool and the firmware agree on it, but nothing checks it against a layout defined outside the model.

UC-ANALYZE#

• The response times assume fixed-priority preemptive scheduling on each core, with the wcet the model gives. A cost the model does not give makes the figure unknown, not zero. Caches, interrupts and blocking outside the model are not counted.
• The bus load is the sum of bits per period of the routed messages. Arbitration, retransmissions and error frames are not modelled.

UC-VERIFY#

• NuSMV checks the machines untimed: a within deadline is checked by the monitors, archec replay and --conflicts, not by NuSMV.
• A guard that is not fully translated may fire or not in the NuSMV model, so a counterexample may not be possible in the model.
• leads to and eventually would need fairness: the generated model lets a state wait for ever.
• Without NuSMV on the PATH, each property is "not checked" (exit 2), never proven.

UC-SAFETY#

• The derived fault trees follow the error model as written. An error path the model does not write (a part, a link or a failure mode left out) is not in them.

UC-CERT#

• The levels and traces are those the model writes: derives, satisfies, verifies. A trace kept outside the model is not seen.

UC-REPLAY#

• A state is known from the log only. A check that reads the state of a part the log never gives is not checkable, and a response still awaited when the log ends is inconclusive, not a failure.

UC-REQIF#

• What has no place in the language is kept as a comment on the way in, not as data. Attributes are matched by name ("Object Text", "Description").

UC-DOC#

• A template placeholder that cannot be filled is marked in the document and printed, and the exit code is 1. A placeholder that fills with an element you did not mean (a filter too wide) is not detected.