Modeling a Verifiable Use Case

Most use cases are written to be read. This is about writing one to be derived from — so a tool can produce the states, the requirements, and the verification cases, and so that what it produces can be settled by a test rather than argued about in a review.

It needs less extra ceremony than it sounds like. Most of it is deciding on purpose what is otherwise decided by omission.

The one idea

A requirement is worth writing only if you can decide whether it was met. That decision happens at the boundary of the part under test — the interfaces, ports, and declared outputs the thing actually exposes. Everything inside the box is invisible unless somebody deliberately publishes it.

So the derivation does not write requirements about your use case’s internals. It projects every fact onto an evidence item: a record of what one execution was observed to do. Requirements are written over that record, and a verification case evaluates them against one populated instance of it.

Everything below is in service of that picture. Model the left box well and the right box is free.

Observable — can the harness see it?

A fact is observable at the boundary when it crosses an interface to an actor, is carried by a port, or is a declared use-case-level output. Everything else is internal, and lands in the report as instrumentation required.

You have exactly three honest responses to an internal fact.

Promote it to a use-case output, when the outcome really is part of what the use case delivers:

out modelCommitted : Boolean;
bind modelCommitted = 'Commit Verification Model'.committed;

Annotate it, when the application genuinely already publishes that step — a status endpoint, an event stream, a structured log:

#observable
action 'Perform Consistency Analysis' { out inconsistenciesFound : Boolean; }

Or accept the cost, leave it internal, and let the report say that somebody has to build a probe.

What the report must not become is a thing to tidy. Its only job is to say what a test can reach; annotating #observable until it looks clean turns a budget into a surprise waiting at integration.

It also catches the reverse. A fact priced as a probe may already be published, in which case the report is right given the model and the model is what is incomplete — it declared one of the things the system hands back and not the others. Declaring the rest moves them into the boundary band and the bill drops accordingly.

Controllable — can the harness drive it?

A stimulus is anything the harness can inject, and there are only two sources.

accept actions — the events that release a waiting state. Each becomes a controllable Boolean, an item def for the payload, and a port on the subject to receive it at:

action 'Await Order' accept ord : Arch::OrderCommand via app.orderPort;

Actor-performed actions — the harness plays the actor, so an actor’s outputs are stimuli rather than observations.

If a use case has no accept action and no actor, it has no control point at all. A harness can start it and watch, and nothing else. That is almost always a modeling gap rather than a property of the system: real systems have inputs, and a model that shows none has left them out.

Verifiable — is there a Boolean?

Every derived requirement carries assume and require constraints over evidence attributes. The prose is context; the Boolean expressions are the deliverable.

Two things sharpen them, and both are yours to supply. Declare outputs — an action with no out parameter gets a synthesized <action>Performed flag, which is verifiable but only tells you the step ran. And declare acceptance criteria, which is the next section, because it is the one that matters most.

Say what “good” means

A use case types its data. It never says what makes an instance acceptable, and that gap is the reason derived constraints so often degrade into notEmpty(x).

Declare the criteria once per item type, as a constraint def whose single in parameter names the type:

constraint def ModelContextValid {
    in ctx : ModelContext;
    attribute idMatches      : Boolean = ctx.contextId   == ctx.expectedContextId;
    attribute versionMatches : Boolean = ctx.version     == ctx.expectedVersion;
    attribute hashMatches    : Boolean = ctx.contentHash == ctx.expectedContentHash;
}

Every action that produces a ModelContext now derives real predicates instead of a presence check:

require constraint idMatches      { evidence.contextIdMatches }
require constraint versionMatches { evidence.contextVersionMatches }
require constraint hashMatches    { evidence.contextHashMatches }

Each predicate also becomes an evidence attribute the harness has to record. Write these once and they apply everywhere the item flows. This is the highest return on effort anywhere in the model: one constraint def upgrades every requirement downstream of that type.

Four keywords

The vocabulary is semantic metadata, and there is less of it than you would expect. Four keywords, each carrying something a flow genuinely cannot.

Annotation	Applies to	What it carries
#exception	an action usage	Valence — that this outcome is a failure rather than an equally valid result
#observable	an action usage	Visibility — that the application already publishes this step
#precondition	a constraint usage	A condition true before the use case runs; derives an assume
#postcondition	a constraint usage	A condition true once it has completed; derives a requirement of its own

Valence, visibility, and the two temporal roles of a condition. That is the whole list.

Nothing here applies to a use case

Every keyword annotates an action usage or a constraint usage, and that falls out of what semantic metadata means rather than being a rule laid on top. Applying one requires the annotated element to specialize the base type — and a use case is not a kind of behavior.

metadata def <exception> Exception :> SemanticMetadata {
    :> annotatedElement : SysML::ActionUsage;
    :>> baseType = exceptionBehaviors meta SysML::ActionUsage;
}

The annotation is not a type

This is worth stating carefully, because it compresses easily into something false. SemanticMetadata is a metaclass — a kind of metadata — and the Kernel Semantic Library defines it this way:

SemanticMetadata is a Metaobject that requires its single annotatedType to directly or indirectly specialize a baseType that models the semantics for the annotatedType.

So the keyword is not the classification. The keyword is what requires the classification, and the specialization — an ordinary one, between the annotated element and the base type — is what a tool adds and what does the work.

That distinction decides what inherits. A child does not inherit the annotation. It inherits the specialization, exactly the way it inherits anything else from a supertype. Which is why this classifies every usage with no keyword written on any of them:

action def PaymentDeclined :> ExceptionBehavior;

It is also why the classification is readable by tools that know nothing about this vocabulary. A specialization is plain SysML v2, so a view filter or a query can ask which behaviors are off-nominal without being taught the keyword. What is not in the language is what a derivation then does with that classification — a vocabulary travels between tools only as far as its meaning is expressed in SysML v2 or KerML itself, and past that point it is a convention that dedicated tooling understands.

Which is why placement matters

Put a keyword on the use case line and it will often type-check anyway, because UseCaseUsage specializes ActionUsage transitively. A tool that renders an element by its most specific classification will then draw your use case as the annotation rather than as a use case — because the specialization the keyword asked for has changed what the element is a kind of.

So #exception action 'Reject Card'; does not decorate the action. It requires the action to specialize ExceptionBehavior. Two useful things follow.

A misplaced annotation is now rejected. #exception part x; used to be accepted and silently ignored, which is the worst of both worlds.

And the vocabulary is extensible:

action def PaymentDeclined :> UseCaseSemantics::ExceptionBehavior;

action 'Card Declined'   : PaymentDeclined;
action 'Wallet Declined' : PaymentDeclined;

Both usages are off-nominal with no annotation written on either. Declare the shape of failure once and reuse it — a project with twelve failure behaviors no longer annotates twelve usages.

Annotate the usage, not the definition

An action def is a definition; an action that types itself by one is a usage. Both are behavioral elements, and the distinction that matters here is which of the two carries the annotation.

A definition can be used in several places, and the same behavior may be nominal in one and exceptional in another — so an annotation on the definition would be a claim it cannot support. Prefix metadata attaches to the usage, and a usage occupies exactly one position in the flow:

action def Notify { out attribute sent : Boolean; }

action notifySuccess : Notify;          // nominal here

#exception
action notifyFailure : Notify;          // same behavior, off-nominal here

That derives two states, and only the second requirement sits off the nominal path. The definition carries no annotation and stays reusable.

Off-nominal paths: the part you have to model

A use case is an existential statement — there is a path where this happens. A prohibition is universal — this never happens. Nothing manufactures a universal negative from an existential positive. If you want the system shall not X, you have to model the circumstance under which X must not happen.

The pattern is short:

#exception
action 'Record Context Retrieval Failure' {
    out contextFailureRecorded : Boolean;
    out failureReason : String;
}

first 'Retrieve Model Context' then contextCheck;
decide contextCheck;
if 'Retrieve Model Context'.contextRetrieved then 'Generate Verification Model';
else 'Record Context Retrieval Failure';

Note where the keyword goes: on the action the branch reaches, not on the branch. A branch cannot carry prefix metadata: #exception else … is rejected with no viable alternative at input ‘#exceptionelse’, and #exception if … fails the same way.

To put the valence on the branch itself, name the succession and point at it:

succession contextFailed
    first contextCheck if not 'Retrieve Model Context'.contextRetrieved
    then 'Record Context Retrieval Failure';
metadata exception about contextFailed;

That form has always parsed. Naming a branch means writing both branches out explicitly, because else will not parse after a named succession.

The ordering rule that will bite you

Read that block again, because the order of those three statements is load-bearing.

A branch takes its source from the member immediately before it. So the if/else pair must follow the decide with nothing in between. Write the edge into the decision first, then the declaration, then the branches — exactly the order above.

Putting the incoming succession between the decide and the branches reads perfectly naturally, and it silently attaches the branches to that succession instead of to the decision node. A validator then rejects the block and usually everything after it, because the parse never recovers. You get a wall of errors pointing at code that is fine, twenty lines below the line that is actually wrong.

This does not change what you get — the derivation normalizes every legal form to the same guard. It changes whether the model you wrote loads at all.

Timeouts are not specifications

accept after 30 [s] models the wait. It says nothing whatsoever about what happens if nothing arrives. A timeout with no branch is an unfinished sentence:

action 'Await Acknowledgement' accept after 30 [s];
action 'Record Acknowledgement Timeout' {
    out timeoutRecorded : Boolean;
    out acknowledged : Boolean;
}
first 'Record Acknowledgement Timeout' then acknowledgementCheck;
decide acknowledgementCheck;
if 'Record Acknowledgement Timeout'.acknowledged then commitJoin;
else 'Reissue Correction Request';

with #exception on 'Reissue Correction Request' itself.

Four shapes, and which to reach for

Shape	How to model it	Where it ends
Terminate — unrecoverable	#exception action, then terminate	a failed ending
Stop, legitimately	terminate with no #exception on the route	an early ending
Recover — handle and rejoin	#exception action, then a succession back	rejoins the nominal path
Retry — bounded	loop … until <condition>	the bound survives as a constraint

The second row is the one most often left out. “Nothing went wrong, and the declared outcomes were still not delivered” is a real ending — a user cancels, a quote expires — and it is neither success nor failure. Folding it into either loses something a test needs.

Note what distinguishes the first two: not a keyword, but whether every route to the ending passes through an #exception. The valence is already on the model, so the ending does not need its own annotation.

Nominal, alternate, exception — properties of a route

#exception on an action does not make that action “the exception step”. Nominal, alternate and exception describe a route through the use case, not a step in it. Consider a decision whose two branches both rejoin:

A → B → decide
        ├─ C → D
        └─ E → D

If the first branch is nominal and the second is an alternate, what is D? It is on both. Calling it a nominal step says something about D that is not true, and calling it alternate says something else that is not true either.

So the annotation goes on the usage — a usage sits at one position in the flow — and the route is derived. Every branch of every decision gets a traversal of its own, each one classified by what it takes: the unforced walk is nominal, another expected traversal is alternate, one that takes an error branch is an exception path. Paired with where it ends, that is the whole taxonomy, and none of it needed a new keyword:

	ends completed	ends early	ends failed
expected route	completed	stopped short	—
exception route	recovered	degraded	terminating

Each route gets its own sequence requirement and its own end-to-end test, so “the alternate path works” is something a run can settle.

Which element carries the mark matters. A state on two routes is genuinely on both, so giving it the least severe is fair: a step every run passes through is normal operation. A transition is not. Where C is nominal and E alternate and both lead to D, the edge E → D belongs only to the alternate route, and giving a transition the color of the state it leads to would make that edge nominal — false of an edge no nominal run crosses.

What must hold at the edges

Some facts are true at the boundaries of the use case rather than inside it:

#precondition  constraint 'ATM Is Stocked'      { atm.cashAvailable > 0.0 }
#postcondition constraint 'Card Is Not Retained' { atm.cardRetained == false }

The asymmetry between them is the interesting part. A precondition is assumed, never required — the system is not answerable for a condition it was handed. A postcondition gets a requirement of its own, under the name you gave it, so it appears in the verification plan as an obligation rather than disappearing into the completion requirement.

They are also not stateBefore and stateAfter. Those record which state an execution was in either side of a stimulus — position in the machine. A condition says nothing about position. Both land on the same evidence record and neither pins the other’s attributes.

In the generated tests this asymmetry shows up as behavior: a postcondition asserts at the end of the end-to-end case, while a precondition is arranged if the generator can set it and otherwise handed to your driver. A run whose precondition did not hold is reported skipped, not passed — because it proved nothing.

What this actually asks of you

The honest summary is that the modeling gets harder and everything after it gets easier.

You now have to decide, explicitly, four things you were previously deciding by omission: what counts as valid data, what must never happen, which outcomes are legitimate-but-not-success, and what the subject was already holding when the use case started. None of that is new information — it existed in somebody’s head, or in a review comment, or nowhere. Writing it down is the work.

What you stop doing is maintaining three descriptions of the same behavior in three notations and hoping they stay in agreement.

And you get a number. The instrumentation report says, before anyone writes code, how many facts the design cannot currently expose. That number is negotiable while the architecture is still soft and much less so later.

One consequence worth naming: every derived requirement is on the subject, never on an actor. A use case names the actor’s steps because a use case is a story about both sides, but a requirement is a claim on the system being specified. “The Customer shall insert the card” is an obligation on a person — unverifiable and unallocatable. What the subject owes is to be there for it, which is what the derived state calls awaitInsertCard.