Verifying SysML v2 Models

Semantifyr verifies SysML v2 models by translating them into OXSTS on top of a semantic library that defines what SysML v2 parts, ports, items and state machines do. This tutorial models a room with a switch and a lamp, verifies three requirements in the live editor, and reads the counterexample of a requirement that does not hold. All you need is a browser; the last section runs the same model from the command line.

The Model

The room has two parts. The switch reacts to presses of its button and tells the lamp to toggle; the lamp turns on and off whenever it is told to. The parts communicate through items sent over ports. Declare the items and the port definitions:

item def Press;
item def Toggle;

port def ButtonPort {
    in item press : Press;
}

port def TogglePort {
    out item toggle : Toggle;
}

Press and Toggle are item definitions without features: only their kind matters here. A ButtonPort receives presses, a TogglePort sends toggles. The in and out keywords give the direction of each item.

The switch is a part with a button, an output and a state machine:

part def Switch {
    port button : ButtonPort;
    port output : TogglePort;

    exhibit state Behaviour {
        transition first start then Off;

        state Off;
        state On;

        transition turnOn first Off
            accept Press via button
            do action { send new Toggle() via output; }
            then On;

        transition turnOff first On
            accept Press via button
            do action { send new Toggle() via output; }
            then Off;
    }
}

The state machine starts in Off. The transition turnOn fires when a Press arrives on the button while the switch is Off; it sends a new Toggle through the output and moves to On. The transition turnOff does the same in the other direction. Naming the transitions is optional, but the names show up in the witness later.

The lamp has an input port that is the conjugate (~) of TogglePort, so its toggle item flows in:

part def Lamp {
    port input : ~TogglePort;

    exhibit state Behaviour {
        transition first start then Dark;

        state Dark;
        state Lit;

        transition lightUp first Dark accept Toggle via input then Lit;
        transition goDark first Lit accept Toggle via input then Dark;
    }
}

Finally, the room puts the two parts together:

part def Room {
    port button : ButtonPort;

    part switch : Switch;
    part lamp : Lamp;

    bind button = switch.button;

    flow from switch.output to lamp.input;
}

The room's own button port is bound to the switch's button, and a flow connects the switch's output to the lamp's input.

The semantic library executes such a model in steps. In each step, the environment may put an item on each input port of the verified part; here that means someone may or may not press the button. Each state machine then fires at most one enabled transition, and a flow delivers the items sent in a step to the receiving port in the next step. An item that the receiver does not accept in that step is dropped.

Requirements and Verification Cases

Requirements talk to the verifier through three calculation definitions, declared at the top of the file:

private import ScalarValues::Boolean;

calc def <EF> eventually {
    in op: Boolean[1];
    return : Boolean[1];
}

calc def <AG> mustAlways {
    in op: Boolean[1];
    return : Boolean[1];
}

calc def isStateActive {
    in s: SysML::StateUsage[1];
    return : Boolean[1];
}

Semantifyr recognizes them by their names: eventually (short name EF) states that some execution reaches a situation, mustAlways (short name AG) that every execution stays in one, and isStateActive asks whether a state is currently active. The SysML v2 example models in the repository keep these definitions in a separate Verification.sysml next to the models; this tutorial keeps them in the model file, so that one file is all you need.

A verification case is a verification def whose subject is the system under verification and whose objective is a requirement over it. The first case asks whether the lamp can ever be lit:

verification def LampLitReachable {
    subject system : Room;

    objective {
        verify requirement {
            require constraint {
                eventually(
                    isStateActive(system.lamp.Behaviour.Lit)
                )
            }
        }
    }
}

The second claims that the lamp is never lit, which is false; the repository's convention marks such expected failures with the Violated suffix:

verification def LampNeverLitViolated {
    subject system : Room;

    objective {
        verify requirement {
            require constraint {
                mustAlways(not
                    isStateActive(system.lamp.Behaviour.Lit)
                )
            }
        }
    }
}

The third claims that the lamp is only ever lit while the switch is on. Before you run it, think about whether it holds:

verification def LampLitOnlyWhileSwitchOnViolated {
    subject system : Room;

    objective {
        verify requirement {
            require constraint {
                mustAlways(not(
                    isStateActive(system.lamp.Behaviour.Lit)
                    and isStateActive(system.switch.Behaviour.Off)
                ))
            }
        }
    }
}

The complete model is one file. Open it in the editor below:

private import ScalarValues::Boolean;

calc def <EF> eventually {
    in op: Boolean[1];
    return : Boolean[1];
}

calc def <AG> mustAlways {
    in op: Boolean[1];
    return : Boolean[1];
}

calc def isStateActive {
    in s: SysML::StateUsage[1];
    return : Boolean[1];
}

item def Press;
item def Toggle;

port def ButtonPort {
    in item press : Press;
}

port def TogglePort {
    out item toggle : Toggle;
}

part def Switch {
    port button : ButtonPort;
    port output : TogglePort;

    exhibit state Behaviour {
        transition first start then Off;

        state Off;
        state On;

        transition turnOn first Off
            accept Press via button
            do action { send new Toggle() via output; }
            then On;

        transition turnOff first On
            accept Press via button
            do action { send new Toggle() via output; }
            then Off;
    }
}

part def Lamp {
    port input : ~TogglePort;

    exhibit state Behaviour {
        transition first start then Dark;

        state Dark;
        state Lit;

        transition lightUp first Dark accept Toggle via input then Lit;
        transition goDark first Lit accept Toggle via input then Dark;
    }
}

part def Room {
    port button : ButtonPort;

    part switch : Switch;
    part lamp : Lamp;

    bind button = switch.button;

    flow from switch.output to lamp.input;
}

verification def LampLitReachable {
    subject system : Room;

    objective {
        verify requirement {
            require constraint {
                eventually(
                    isStateActive(system.lamp.Behaviour.Lit)
                )
            }
        }
    }
}

verification def LampNeverLitViolated {
    subject system : Room;

    objective {
        verify requirement {
            require constraint {
                mustAlways(not
                    isStateActive(system.lamp.Behaviour.Lit)
                )
            }
        }
    }
}

verification def LampLitOnlyWhileSwitchOnViolated {
    subject system : Room;

    objective {
        verify requirement {
            require constraint {
                mustAlways(not(
                    isStateActive(system.lamp.Behaviour.Lit)
                    and isStateActive(system.switch.Behaviour.Off)
                ))
            }
        }
    }
}

Verifying

The editor loads the SysML v2 standard library in the background, which takes about 15 seconds, and then lists the three cases under Verification Cases. Each case has its own run button, and the button in the panel's header runs them all. The live editor verifies with Theta and Spin, and each of these cases takes a few seconds.

Expect LampLitReachable to pass and both Violated cases to fail.

The model is yours to edit, as one file. The cases follow your edits, and a construct the translator does not support gets a diagnostic on that construct and keeps the model from being verified. The OXSTS tab shows the translation of the current file, an OXSTS model that instantiates the classes of the SysML v2 semantic library.

Reading the Witness

A case with a witness gets a button in its row that opens the Witness tab, which has three views:

• Trace: per step, the traced calls of the semantic library: the transitions that fired and the items that were sent.
• State: the values of the model's state in every step of the witness, starting from the initial state that initialization produces. State names are paths from the verified instance, root.
• Raw: the witness as a SysML v2 model, a part definition <case>Trace that specializes the verified part definition and declares the states, transitions and sends of this execution in time order (SysML v2 traces).

A failed mustAlways requirement has a counterexample. Open the witness of LampLitOnlyWhileSwitchOnViolated. The shortest counterexample has two steps:

1. The button is pressed: root.system.switch.Behaviour.turnOn fires and the switch's output sends a Toggle. Afterwards the switch is On, the lamp is still Dark, and the toggle waits on root.system.lamp.input.
2. The button is pressed again: turnOff fires and sends a second Toggle, while the lamp accepts the first one and root.system.lamp.Behaviour.lightUp fires. Afterwards the switch is Off and the lamp is Lit.

The requirement fails because the parts communicate asynchronously: the lamp follows the switch one step later. Whether that is a defect of the design or of the requirement is for the engineer to decide.

The Raw view tells the same story in SysML v2: LampLitOnlyWhileSwitchOnViolatedTrace specializes Room, its switch and lamp redefine the room's parts, and their exhibited states hold the occurred states and the fired transitions: turnOn1 and turnOff1 with the toggles they send, and lightUp1. Snapshots order the reactions, step1 and step2, and time slices the second after each, dwell1 and dwell2. Since the trace refines Room, any SysML v2 tool reads it next to the model.

The verifier finds a witness for LampLitReachable the same way: an execution in which the lamp lights up. A passing mustAlways requirement or a failing eventually requirement has no witness, since no single execution proves it.

On the Command Line

The semantifyr-sysml command verifies the same model locally, with every installed backend, and writes its artifacts to disk.

Requirements

• A Java 25 runtime found through JAVA_HOME or PATH.
• Node.js 22 or newer on PATH: the SysML v2 front end, a fork of SysIDE, runs on Node.js.
• The semantifyr-sysml command-line distribution (Getting Started), which verifies SysML v2 models (reference). It carries the translator from SysML v2 to OXSTS and the SysML v2 semantic library, so Node.js is the only prerequisite SysML v2 adds.

To build the distribution from a clone of the repository, which needs Git (the first build downloads its dependencies, the SysIDE fork among them, and takes several minutes):

git clone https://github.com/ftsrg/semantifyr.git
cd semantifyr
./gradlew :sysml-cli:installDist
export SEMANTIFYR_HOME="$PWD/subprojects/frontends/sysml/sysml-cli/build/install/semantifyr-sysml"

SEMANTIFYR_HOME now holds the same layout as the release zip: the launcher in bin/, Theta in theta-xsts-cli/ and the semantic library in libraries/. If you use the release zip instead, point SEMANTIFYR_HOME at the unzipped semantifyr-sysml-<version> directory. The commands on this page are written for Linux and macOS shells; on Windows, use bin\semantifyr-sysml.bat.

Verifying Locally

Create an empty directory and save the complete model in it as room.sysml. The translator reads every .sysml file in the model's directory, so keep other models out of it.

room.sysml

private import ScalarValues::Boolean;

calc def <EF> eventually {
    in op: Boolean[1];
    return : Boolean[1];
}

calc def <AG> mustAlways {
    in op: Boolean[1];
    return : Boolean[1];
}

calc def isStateActive {
    in s: SysML::StateUsage[1];
    return : Boolean[1];
}

item def Press;
item def Toggle;

port def ButtonPort {
    in item press : Press;
}

port def TogglePort {
    out item toggle : Toggle;
}

part def Switch {
    port button : ButtonPort;
    port output : TogglePort;

    exhibit state Behaviour {
        transition first start then Off;

        state Off;
        state On;

        transition turnOn first Off
            accept Press via button
            do action { send new Toggle() via output; }
            then On;

        transition turnOff first On
            accept Press via button
            do action { send new Toggle() via output; }
            then Off;
    }
}

part def Lamp {
    port input : ~TogglePort;

    exhibit state Behaviour {
        transition first start then Dark;

        state Dark;
        state Lit;

        transition lightUp first Dark accept Toggle via input then Lit;
        transition goDark first Lit accept Toggle via input then Dark;
    }
}

part def Room {
    port button : ButtonPort;

    part switch : Switch;
    part lamp : Lamp;

    bind button = switch.button;

    flow from switch.output to lamp.input;
}

verification def LampLitReachable {
    subject system : Room;

    objective {
        verify requirement {
            require constraint {
                eventually(
                    isStateActive(system.lamp.Behaviour.Lit)
                )
            }
        }
    }
}

verification def LampNeverLitViolated {
    subject system : Room;

    objective {
        verify requirement {
            require constraint {
                mustAlways(not
                    isStateActive(system.lamp.Behaviour.Lit)
                )
            }
        }
    }
}

verification def LampLitOnlyWhileSwitchOnViolated {
    subject system : Room;

    objective {
        verify requirement {
            require constraint {
                mustAlways(not(
                    isStateActive(system.lamp.Behaviour.Lit)
                    and isStateActive(system.switch.Behaviour.Off)
                ))
            }
        }
    }
}

In the directory of room.sysml, verify the model:

"$SEMANTIFYR_HOME/bin/semantifyr-sysml" verify room.sysml --artifact-directory ../room-artifacts

The verify command translates room.sysml to OXSTS, an OXSTS model that instantiates the classes of the SysML v2 semantic library, which takes about a minute. It then finds the three verification cases and verifies each with the default smart-full portfolio, which races every installed backend. The artifacts go outside the model's directory, since the translator reads every .sysml file below it and the run writes SysML v2 traces.

For each case, the command prints its name, PASSED or FAILED with the time it took, and the path of its report.json, and it exits with status 5 when a case fails (the exit codes). Expect LampLitReachable to pass and both Violated cases to fail. The case names start with semantifyr::sysml::model, the package the translator gives every model.

The Artifacts

--artifact-directory ../room-artifacts keeps the translated model in compiled/default/room.oxsts and the artifacts of every case in a directory named after the model file and the qualified name of the case, shortened with a hash when longer than 64 characters. Next to the backend's working files, the compiler's intermediate models (pipeline/) and the run's measurements (report.json), a case with a witness has four files:

• witness.json: the values of the model's state in every step of the witness: initializedStep, the initial state that initialization produces, then one entry per step. State names are paths from the verified instance, root.
• trace.json: per step, the traced calls of the semantic library: the transitions that fired and the items that were sent.
• witness.oxsts: the witness as an OXSTS model that replays exactly this execution.
• trace.sysml: the witness as a SysML v2 model, a part definition <case>Trace that specializes the verified part definition and declares the states, transitions and sends of this execution in time order (SysML v2 traces). SysIDE validates it against room.sysml before it is written; a witness the generator cannot express gets no trace.sysml and a warning in the log.

The counterexample above is in trace.json and witness.json in ../room-artifacts/room.LampLitOnlyWhileSwitchOnViolated/, and trace.sysml next to them is the model of the Raw view.