SysML v2 Model Formalism Working Group

The SysML v2 Model Formalism project originated as part of the SysML Roadmap effort within the OMG Systems Engineering Domain Special Interest Group (SE DSIG). The near term goal is to identify requirements related to the logical formalism that SysML v2 will be derived from.

• The next-generation modeling language must include precise semantics that avoid ambiguity and enable a concise representation of the concepts.
• The language must derive from a well-specified logical formalism that can leverage the model for a broad range of analysis and model checking.
• This includes the ability to validate that the model is logically consistent, and the ability to answer questions such as the impact of a requirement or design change, or assess how a failure could propagate through a system.
• The language and tools must also integrate with a diverse range of equation solvers and execution environments that enable the capture of quantitative data.

• SysML 1.x was originally designed to support diagrams rather than analysis; since then, the expectations on modeling have changed.

• SysML 1.x is defined as a profile of UML 2.x, which renders its extension capabilities limited.
• SysML execution semantics are based on the current UML execution semantics, which only cover a small portion of the overall language.
  • More precisely, while fUML handles the execution semantics of the core of UML unambiguously, these semantics are based on a discrete model of behavior; whereas SysML needs to embrace both discrete and continuous behavior. Therefore, while SysML has access to unambiguous execution semantics for discrete behavior, the same cannot be said for the continuous behavior that SysML requires, which limits its applicability.
  • However, activity models can describe continuously changing quantities at small increments of time, like Simulink does. The attached activity diagram can be run in a clocked fashion, as in numerical simulation, see description around Figure 26 in http://tinyurl.com/ho537cp. fUML might support clocked execution, even though the reference implementation doesn't, but it doesn't support streaming. Clocked execution is within the UML semantics for activities, and it supports streaming, of course.
• The current formalism for SysML requires more robust capability to support the full range of reasoning and model checking to ensure system design. Below are some example use cases.
  • After learning of the government regulation to increase MPG to 27.5, the engineer updates this requirement in the SME. As a result, the SME informs the engineer of which elements in the system design might be impacted by this requirement change (e.g., elements dealing with gear selection).
  • After making a change to the gear selection algorithm in the system design, the SME informs the engineer of impacted model elements, along with the associated analysis that need to be re-run. Based on the analysis, the engineer discovers that the vehicle's acceleration performance has been reduced. The engineer then uses the SME to determine what other elements have an impact on the acceleration performance to see what other changes could be made to the system design to restore the acceleration performance to the specified level.
  • The engineer decides that weight reduction will be the preferred approach to restore the acceleration performance. As a result, the engineer uses the SME to consider potential system design changes that could reduce the weight. One such change is to reduce the weight of the transmission. The engineer identifies design alternatives to reduce the transmission weight. For one of the promising candidates, the engineer acquires a model of the transmission from the manufacturer and integrates it into the system model. However, the SME informs the engineer that the electrical connectors are incompatible, and the engineer proceeds to investigate other alternatives.
  • Based on analysis of other alternatives, the engineer identifies a design alternative that satisfies the required acceleration performance and the required increase in fuel efficiency. The engineer then performs a verification analysis through the SME to verify that the system design still meets the requirements.

• SysML v2 Formalism: Requirements & Benefits Brussels - June 2017
• Semantics Intro, Formalism Requirememts, Benefits, Use Cases, and Future Directions Reston - March 2017 (SysML 2 RFP WG)
• SysML 2.0 Formalism Requirements andPotential Language Architectures Coronado - December 6 (ADTF)
• SysML 2.0 Formalism:Requirement Benefits,Use Cases, andPotential Language Architectures Coronado - December 2016 (SysML 2 RFP WG)
• SysML v2 Formalism Requirements Chicago - September 2016
• Modeling Formalism (Modeling Language Foundations) Orlando - June 2016
• Modeling Formalism (Modeling Language Foundations) Reston - March 2016

• TBD

• OWL 2
• OWL 2 Direct Semantics
• IDEAS Foundation

• Use Case for expressing dysfunctional behavior
• Teleconference Powerpoint Slides (9/7 & 9/9)
• Teleconference Powerpoint Slides (8/15) - Algebraic Structures on Relationships/Customizable Inference Engines in SysML v2
• Teleconference Powerpoint Slides (8/1) - A Bayesian Learning Approach to Inconsistency Identification in MBSE, S.Herzig
• A Baysian Learning Approach to Inconsistency Identification in Model-Based Systems Engineering (Dissertation), S. Herzig
• 7/25/2016 Teleconference PowerPoint Slides
• 7/25/2016 Teleconference PowerPoint Slides

• TBD

• TBD

• OMG
  • Unified Architecture Framework FTF, adopted response to UPDM 3.0 RFP. OWL-like foundation (IDEAS) metamodel with UML/SysML Profile.
  • Distributed Ontology, Modeling, and Specification Language (DOL) can be used to integrate first order logic based languages (in finalization March 2016, from RFP December 2013). See Annexes for examples. Overview in ADTF presentation. More information on Ontolog.
  • MOF to RDF Structural Mapping in Support of Linked Open Data RFP and responses
  • Metamodel Extension Facility RFP and responses (SMOF-based alternative to profiles)

• Ontology
  • OntoUML
  • OWL 2 Direct Semantics
  • Onto Behavior Modeling (aka "UML3") (slides, updates available)
    • Special case of Domain-Specific Engineering of Domain-Specific Languages
  • Onto Product Modeling (slides)

• Model checking (a proof technique for semantic validation)
  • Towards a Multi-Formalism Model Checker Based on SDES Description
  • RDF2SPIN: Mapping Semantic Graphs to SPIN Model Checker

• Hamilton/Hackler
  • A Formal Universal Systems Semantics for SysML
  • Universal Systems Language for Preventative Systems Engineering

• Emphasize the need for SysML v2 to be computer interpretable.
• Clarify the need for both a textual notation similar to a programming language such as ALF and graphical notation for the formalism.
• Clarify that the SME should make you aware of inconsistencies, and provide options for resolving them.
• Clarify that the formalism should provide a precise and concise extension mechanism (similar to stereotypes).
• Clarify that the use cases for model checking should include well formedness checking such as for interface compatibility.
• Clarify the need to be able to apply varying degrees of formalism. For example, the language should not overly constrain the user when developing concepts, recognizing that concepts are formed throughout the life cycle and not just early on. This is partially addressed by differentiating the level of precision from the level of detail, but may also allow for relaxing formalism constraints based on user need.
• Continue to refine the usability criteria and how the formalism can impact usability. As an example, some system engineers struggle to understand how to organize a model which involves the concepts of namespace and containment. The criteria should enable us to measure and assess how well a concept aligns with the way different representative users think. Consider the following representative users:
  • A new SysML modeler who may be experienced with other models such as Simulink
  • An experienced SysML modeler
• Identify alternative formalisms and their pros and cons based on the requirements and evaluation criteria.