DocsGo to Lemmatica
Concepts

GSN V3 Notation Reference

This reference is based on the GSN Community Standard V3 (SCSC-141C), published by the Safety-Critical Systems Club. Features marked as "Planned" in the compliance table below are part of the GSN V3 specification but not yet available in Lemmatica.

Structural elements

Goal

A claim or assertion about the system. Goals are the core building blocks of every safety argument.

G1System is acceptably safe
G2Undeveloped goal
G3Away goal reference
  • Can have children: Strategy or Solution (not Goal directly)
  • Can have annotations: Context, Assumption, Justification
  • Special states: Undeveloped (dashed border, no children yet), Away (dashed border, links to sub-case)

Every safety argument has exactly one top-level goal — the overarching safety claim being made.

Strategy

The reasoning approach used to decompose a goal into sub-goals.

S1Argument by hazard classification
  • Can have children: Goal only
  • Can have annotations: Context, Assumption, Justification

A strategy answers the question: "How are we arguing this goal?" Common strategies include argument by decomposition, argument by evidence type, and argument by hazard classification.

Solution

A reference to evidence that supports a claim.

Sn1Test report v2.1
  • Can have children: None (always a leaf node)
  • Can have annotations: Context, Assumption, Justification

Solutions point to concrete artifacts: test reports, analysis results, review records, simulation outputs.

Annotation elements

Annotations do not participate in the argument tree hierarchy. They attach to structural nodes to provide additional context.

Context

Scoping information for a claim — definitions, system boundaries, operating conditions.

C1Operating environment: highway driving
  • Attaches to: Any structural node

Assumption

Something accepted as true without proof within this argument.

  • Shape: Oval (ellipse)
  • Attaches to: Any structural node

Don't hide assumptions

Hidden assumptions are a leading cause of safety case weaknesses. Making assumptions explicit — even obvious ones — strengthens your argument and makes it easier to review.

Justification

Rationale for why a particular approach is appropriate.

  • Shape: Oval (ellipse) with J marker
  • Attaches to: Any structural node

Structural rules

RuleDescription
Goals must be developedA goal must have at least one Strategy or Solution child, or be marked as undeveloped
Goals cannot parent goalsA goal cannot directly connect to a sub-goal; a Strategy must mediate
Strategies must have goal childrenA strategy's children must all be goals
Solutions are leaf nodesA solution cannot have any children
Single rootEach document has exactly one top-level goal with no parent
No cyclesThe argument tree must be acyclic

Live validation

Lemmatica checks all of these rules continuously as you edit. Violations appear as inline errors on the affected nodes — you don't need to run a separate validation step.

Edge types

Parent-child (SupportedBy)

Structural relationship forming the argument tree:

  • Goal → Strategy
  • Goal → Solution
  • Strategy → Goal

Annotation (InContextOf)

Attaches context, assumptions, or justifications to a structural node. Annotation edges do not form part of the tree hierarchy.

Modular extensions

Away goals

An away goal is a leaf goal that references another document. The referenced document contains the sub-argument that develops this goal.

G4Braking subsystem is safe

Away goals enable:

  • Decomposition of large arguments into manageable parts
  • Reuse of common sub-arguments across multiple safety cases
  • Team collaboration where different teams own different sub-cases

Undeveloped goals

A goal marked as undeveloped explicitly signals that the argument below it has not been completed. This is useful for work-in-progress safety cases.

G5Environmental hazards mitigated

Dialectic extension

Coming soon

The dialectic extension is part of the GSN V3 specification and is on Lemmatica's roadmap. The notation is documented here for reference.

The GSN V3 dialectic extension adds formal counter-argumentation to safety cases.

Challenge

A counter-argument raised against a goal or solution. Challenges question whether a claim is valid or whether evidence is sufficient.

Defeated state

When a challenge is accepted, the challenged node becomes defeated. Defeat propagates upward through the tree — if a child goal is defeated, its parent strategy and parent goal may also be affected.

G6All test cases pass
S2Argument by test coverage

This mechanism lets teams formally document objections, track their resolution, and make the impact of unresolved challenges visible at every level of the argument.

GSN V3 compliance

Lemmatica implements the GSN Community Standard V3 (SCSC-141C) with the following coverage:

FeatureStatus
Core node types (Goal, Strategy, Solution)Supported
Annotation types (Context, Assumption, Justification)Supported
Structural validation rulesSupported
Away goals (modular extension)Supported
Undeveloped goalsSupported
Dialectic extension (challenges, defeated state)Planned
Argument patternsPlanned