This pioneering research project started in 2019 with the collaboration of several participants. In addition to the current IncQuery team, the following have also contributed: Benedek Horváth, JKU, Vince Molnár, Bence Graics, Zoltán Micskei, Ákos Hajdú, Milán Mondok (Critical Systems Research Group), Luigi Andolfato (ESO), Robert Karban, Myra Lattimore, and Ivan Gomes (NASA JPL).
With the growing horizontal and vertical complexity of systems design scenarios and workflows, recently, novel methods for validation and verification (V&V) of model-based systems engineering artifacts have emerged as a focus point of digital engineering innovation. In particular, the issue of validating requirements pertaining to operational behavior poses a serious challenge. While SysML state machines and activity diagrams provide a structured means to express behavioral design, simulating a handful of traces is usually not enough to find subtle design errors in the models. The challenge consists of finding the right compromises for state space exploration in terms of structural constraints, allowing for an efficient behavioral validation process, even in industry-scale applications.
We aim at a design-time, optimized, simulation-based solution, which is capable of an automated and distributed state space exploration of behavioral system models of basically any size, enabling early detection of behavior paths leading to potentially unwanted system states.
Model checking, a formal verification technique has been often adopted to address the issue of behavior validation; however, this even today involves expertise and resource bottlenecks that are hard to overcome for organizations. Having a well-founded, yet pragmatic V&V approach involving operational and behavioral elements is a key issue in industries such as space, aerospace and manufacturing, where ever-growing demand for automation and ease of use meets high expectations toward safety and alignment with industry standards and regulations.
The Dynamic Verification Toolkit (DVT) of the IncQuery Validator addresses this complex problem space by
OpenMBEE, “an open source collaborative engineering system” driven and developed by a consortium of key industrial players and researchers, offers an architectural basis to accommodate novel functionalities and processes such as DVT.
The figure shows the central elements offered by OpenMBEE, as well as connections to further elements of a complex ecosystem, namely, model authoring tools and additional user-facing services. As for those central elements, the MMS (Model Management System) repository serves as a cloud-based storage, access and versioning service for models, accessed through tool-specific integration points, the so-called Model Development Kits (MDK). The following figure shows the DVT-specific extension of this architecture, concretizing what modeling tools are involved in the process, and what additional services do we offer.
The Gamma framework, an open-source toolkit “to model, verify and generate code for component-based reactive systems” based on the Yakindu statechart modeling tool, is an adequate intermediate format to combine our ecosystem with actual model checking tools (Theta and UPPAAL in our case) performing formal behavioral validation, while still allowing us to maintain our basic design intent: to eliminate expertise, performance and usability bottlenecks in our V&V ecosystem.
Regarding the lessons learned throughout the creation of DVT, we have conducted interviews with systems engineers at NASA JPL, one of the leading organizations in complex digital engineering innovation. Moreover, we have used the largest openly available MBSE test model, that of the Thirty Meter Telescope for evaluation. These experiments have revealed that pure SysML state machines alone are not enough to tackle practical engineering problems. Activity diagrams extended with some script-based guard languages to express complex conditions are frequently used for expressing behavior in system models in a precise way, easily understandable by engineers. Relying on the IncQuery Suite infrastructure allows us to address further needs of industrial systems design workflows. According to our investigations, the tool should be deployable both on-premise and to cloud infrastructure, should be able to integrate to other systems, provide authentication and authorization with auditing for state-of-the-art security, and should be able to serve jobs from multiple users in parallel with an acceptable response time.
As for performance and scaling, it turned out to be essential to limit the validation scope, where our combination of reducing the set of allowed elements to a pragmatic subset of SysML, as well as of the optimization possibilities provided by the Gamma Framework resulted in a horizontally and vertically scalable architecture with reasonable conceptual trade-offs. Technically, this means that we check if the model contains unsupported or structurally incorrect elements, indicated by validation errors returned to the user. In the background, there is a comprehensive rule-based validation suite consisting of more than 130 imperative and declarative rules, for checking the guard expressions, action and effect statements, as well as the structure of the SysML models, respectively.
If you want to learn more about the DVT approach and take a look at the tooling itself, watch a comprehensive video, also embedded in this short summary on the project outcome, which was also published as a Medium article. The research and development activities leading up to what is DVT now have been presented at the prestigious MODELS conference in 2020 and 2021 – and even at the Hungarian Researchers’ Night for a wider audience.
Acknowledgments
This research was a collaboration between IncQuery Labs, Critical Systems Research Group, Johannes Kepler University, and NASA JPL.
This work partially received funding from the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie grant agreement No 813884 (Lowcomote project) and the NRDI Fund of Hungary, financed under the 2019–2.1.1-EUREKA-2019–00001 funding scheme.
Disclaimer: Reference herein to any specific commercial product, process, or service by trade name, trademark, manufacturer, or otherwise does not constitute or imply its endorsement by the United States Government or the Jet Propulsion Laboratory, California Institute of Technology.
