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 Kernel Block Diagram
Section titled “The Kernel Block Diagram”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
Structure Mapping: TMaps to SysML
Section titled “Structure Mapping: TMaps to SysML”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.
Constraint Mapping
Section titled “Constraint Mapping”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.
System Architecture and Layering
Section titled “System Architecture and Layering”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.
Six Preliminary Findings
Section titled “Six Preliminary Findings”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.
References
Section titled “References”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.
Related Documents
Section titled “Related Documents”- USL for Preventative Systems Engineering (2007) — The companion CSER paper from the same year. The CSER paper contains worked examples (GN&C, Jset, interrupt snapshots) not in this paper; this paper contains the SysML mapping, kbd syntax, and the six findings not in the CSER paper. Reading both provides the most complete picture of 2007-era USL.
- USL: Lessons Learned from Apollo (2008) — Synthesizes both 2007 papers into a more accessible form but omits the SysML-specific mapping and the six findings.
- Higher Order Software (1976) — Origin of the axioms. This INCOSE paper shows how 30 years of refinement transformed HOS’s mathematical core into a practical formal language.
- The Relationship Between Design and Verification (1979) — The error analysis methodology. The Preliminary Findings on variables and complete mappings are direct descendants of the 1979 paper’s verification-by-construction approach.
- What the Errors Tell Us (2018) — Cites this paper as reference 10.
- Preventative Software Systems (1994) — Where DBTF was named. This INCOSE paper is the fullest expression of DBTF applied to standards-based systems engineering.