Skip to content
0 / 17
Pre-launch Review

A Formal Universal Systems Semantics for SysML


A Formal Universal Systems Semantics for SysML

Section titled “A Formal Universal Systems Semantics for SysML”

Margaret H. Hamilton and William R. Hackler, Hamilton Technologies, Inc., 2007

The paper positions 001AXES as a formal semantic foundation that can enhance SysML by reducing semantic ambiguity. SysML represents a subset of UML2 with extensions for systems engineering. Hamilton and Hackler propose that 001AXES’s axiom-based semantics can bridge “the semantic gap between systems, software, and other engineering disciplines.”

The novel contribution of this paper is the kernel block diagram (kbd) — a syntactic bridge between SysML’s block definition diagram (bdd) and internal block diagram (ibd) on one hand, and 001AXES’s formal semantics on the other. The kbd renders the three primitive control structures (Join, Include, Or) in block-diagram notation familiar to the model-based systems engineering community.

The kbd provides SysML specifications with capabilities that the standard SysML diagrams lack:

  • Executability and translatability (e.g., to software)
  • Built-in causality and total ordering of timing in terms of priority
  • Built-in schedulability for active distributed resources
  • Automatable design based on resource allocation implications
  • Automatable systems analysis based on optional resource architecture allocations

TMaps map to SysML structure diagrams. A vehicle block definition diagram and internal block diagram are shown mapped to a TMap in both default 001AXES syntax and kbd syntax. Flow directionality is captured via < and > relation annotations, constraining realization by resources such as sensor signals. The anti-lock controller portion demonstrates how physical system structure maps onto the formal type hierarchy.

Behavior Mapping: FMaps to SysML Activities

Section titled “Behavior Mapping: FMaps to SysML Activities”

FMap nodes integrate control, function, causality, and time — properties that SysML activity diagrams distribute across multiple diagram elements. The kbd uses a data-flow-like representation (ibd-style) rather than control-tree syntax.

The operate_car FMap demonstrates interrupt handling mapped to SysML’s OperateCar activity. The is:present(keyOff) mechanism provides non-blocking asynchronous decision-making, related to but more precisely defined than SysML’s <<interruptibleRegion>>. A key difference: “SysML is value driven while 001AXES is object state driven with the ability to ask if an object state exists or not.”

FMap variable semantics are fundamentally different from SysML’s: “An FMap variable by default always implies a fully asynchronous stream-like behavior.” Variables declare relationships between potential producer and receiver functions, and the invocation process integrates functional and resource architectures by invoking according to priority.

Constraints map to SysML parametrics. A fahrenheit/centigrade constraint demonstrates the approach: a primitive constraint add(a,b;c) (where the semicolon separates domain from codomain) produces three mappings: add(a,b)=c, sub(c,a)=b, sub(c,b)=a. By identifying which variables are domain (known inputs), the system automatically generates the appropriate computation. This bidirectional constraint resolution is more powerful than SysML’s parametric diagrams.

The allocation architecture (AA) maps a functional architecture (FA) onto a resource architecture (RA), producing a system architecture (SA). This strict separation — functional specifications never exhibit parallelism, which only emerges through resource allocation — is a central USL principle.

The paper uses Allen’s 13 interval time relationships (before, meets, overlaps, starts, during, finishes, equals, and their inverses) to characterize potential scheduling of Include (independent) children. This formal treatment of temporal relationships enables automated scheduling analysis.

Distributed object communication can be automated: “Communication between distributed objects can be automated by having fully traceable object states (or flows) between functions of the FA.” TCP/IP sends and receives are automatically generated as distributed design artifacts.

The Preliminary Findings section is unique in Hamilton’s published work. It contains direct technical critique of UML2/SysML semantic shortcomings, each contrasted with the 001AXES kernel’s approach:

1. Variables. UML2 variables refer to physical memory locations, causing side effects and traceability loss. 001AXES enforces single reference/single assignment. Example: x=x+1 would violate traceability and prevent generalized distributed scheduling.

2. Invocation policy. SysML defaults to synchronous invocation, reflecting an imperative “controlling a machine” orientation. The kernel defaults to asynchronous, event-driven invocation. Hamilton questions whether “a completely functional and asynchronous system specification can be defined from a 001AXES perspective” using SysML without enhancements.

3. Activity control mechanisms. In SysML, control mechanisms are not aligned with activity decomposition. Priority is not assigned to every action. Asynchronous traceable event-driven invocation is not the default. Because total ordering by priority is absent, automated resource allocation with automatic scheduling is not viable.

4. Existence of object states. SysML/UML2 lacks a mechanism to test whether a variable has a value (as opposed to what its value is). The kernel provides is:present for this purpose.

5. Complete mappings. SysML activities may lack inputs or outputs. Internal variables lose traceability to real interfaces. The kernel requires every function to have inputs and outputs — all variables are traceable, enabling full automation of scheduling with no deadlocks and no priority inversion.

6. Active objects. UML2’s passive/active object distinction with weak layering embeds resource allocations into functional specifications, restricting portability. The kernel always associates active objects with resource allocation mappings, maximizing portability.


The paper contains 21 references including the OMG SysML and UML2 specifications, Allen’s temporal interval algebra, the Bolinger and Sears linguistics work, and Hamilton’s prior publications.