design

Design notes

How a subsystem is built and which normative reference it answers to. For maintainers; the behavior a user sees is the guide.

• The action executor — how a token moves through a lowered ActionGraph
• The analysis framework — one engine contract that the interpreter, explore, the sweep, the SMT solver, the model checkers and external tools register against, one scale for the strength of an answer (proved, bounded, witnessed, observed, not covered), dispatch by question with fallback, and runs isolated so they can be parallel; the contract, the registry and the four engines over existing code are implemented (internal/exec/analysis), the rest is a proposal
• OpenSysML MDK, a Cameo Systems Modeler plugin — a plugin for Cameo 2026x Refresh1, positioned as the successor to OpenMBEE's MDK, that exports the selection, runs Convert(xmi→sysml) and ParseSources over the Java client, executes and verifies on sysml-grpc, and lands each verdict on the Cameo element it came from through the migration report's xmi:id → target accounting; the vendor plugin mechanics, UI contribution points, export routes, Simulation Toolkit positioning and SysML v2 status answered from public documentation with every unverified claim marked, a migration benchmark over twenty public v1 models, a phased plan and the risks
• Bring your own engine — a proposal: a manifest and a protocol under which a user's own engine, scheduling policy, sampler or tool registers with the analysis framework as a process, a WebAssembly module or Go over the public package; every external witness is checked by the interpreter against the claim it supports, and a universal claim is observed only over executions the interpreter replayed, otherwise not covered until the site admits more against a referee record
• Bounded model checking of behaviors — a proposal: explore every admissible interleaving up to a bound with partial-order reduction, and report the requirement violations, deadlocks and schedule-dependent outcomes it finds
• An embedded target for Class A flight software — a proposal: a closed, serializable behavior IR with a written semantics as the requirement basis, a freestanding C profile (no allocation, no recursion, static loop bounds, no extensions, structurally coverable emission) over static tables, static refusal of every admissible scheduling choice and every unbounded resource, the artifacts and traceability a tool qualification argument consumes, and a fixed-step host interface proved under Zephyr on QEMU and as an F´ component
• Scheduling policies, choice points and exploration — how a run resolves what the library leaves unordered, reports each such choice without changing the run, takes another linearization under declared or seed:<n>, and enumerates every one within a budget under explore
• Recording the order of orthogonal regions — the entry and exit of a composite state's regions and the units of the firings one occurrence selects across regions as recorded choice points drawn on one front, with the kinds, the trace and witness lines, what each policy does at each, the rollback of a refused replay, the choice-point budget and the alignment row on firing granularity; and the designs, not yet implemented, of a do step against a dispatch and of a completion's firing inside the entry front
• Observing a run — a proposal: the trace recorder as one event stream and the executors' configuration as one snapshot shape, a wire session over them (OpenSession, unary commands, one server-streamed subscription) the REPL debuggers become an implementation of, client callbacks and @Observation::Listener metadata by which a model names a co-simulation or visualization hook, what a listener may do to the run without becoming a scheduler, and why translating to SCXML is not the route
• Orthogonal regions — concurrent substates, in the standard parallel notation; the bundled libraries give them no performance, so UML 2.5.1 supplies the semantics
• Pseudostates — choice, junction, fork, join and history
• Alignment with the UML precise-semantics specifications — an assessment: PSSM, fUML and PSCS mapped clause by clause against the SysML v2 notation, the KerML library and what the runtime does, with a verdict per row, a count of where a port could change behavior, the PSSM test suite assessed as a referee, options and a recommendation
• Python gRPC bindings — the service and client design
• SMT bounded model checking of behaviors — a proposal: unroll an action's token flow to a bounded number of moves and ask an SMT solver whether any schedule and any input violates a requirement, with every witness replayed in the interpreter and explore as the referee
• Surface parity — a proposal: the REPL, the CLI, the editor, the public Go package and the wire inventoried operation by operation, each difference sorted as shared already, missing and worth adding, interactive, protocol-bound or local-only, and the stages that give every operation one assembly the four surfaces call, add the stateless operations the wire lacks (satisfiability, checker options, replay, views, search), design a session API for the debuggers apart from the stateless calls, and make the agreement a conformance protocol rather than a claim
• A SysON plugin — a discovery and design: how Eclipse SysON's Sirius Web backend and React frontend take contributions, its textual exporter and SysIDE importer, its partial SysML v2 REST API and normative library ids, the mapping between a qualified-name Symbol.id and an EMF element, sysml -validate over SysON's textual models, then the layout of editors/syson/, the "Run with OpenSysML" sequence and a four-phase plan; nothing is implemented
• Transport evaluation — Connect and stdio measured beside gRPC, with the lifecycle-code delta and a recommendation
• Visual modeling in VS Code — the live diagram panel, the diagram-driven edits, and the graphical editor it builds to

The staged plans that built the bindings, kept for their rationale: phase 1 (the service), phase 2 (the client), phase 3 and its fixes, phase 4.