Pragmatic Model Checking of Industrial Behavioral SysML models
How to benefit from the Cloud to proceed toward scalable model checking?
Abstract
Model-Based Systems Engineering (MBSE) is a widely adopted method of analyzing, simulating, designing, and building industrial systems. SysML is a standardized language for systems modeling. The language proposes several concepts to be used for the structural, behavioral modeling, and simulation of systems.
The verification and validation of such models are crucial to develop high-quality systems. However, this is a challenging problem due to the complexity and size of the models. In this short blog post, we propose a workflow for checking the correctness of industrial behavioral SysML models. The workflow is deployed in Kubernetes to leverage the elastic scalability of the Cloud and to proceed toward scalable model checking.
Open Model Based Engineering Environment
The Open Model Based Engineering Environment (OpenMBEE) is an open-source collaborative engineering system that enables engineers to share their models across other tools easily. The ecosystem consists of a model repository (MMS), tool-specific plug-ins (MDK) to sync models to the repository, a View Editor to interact with the SysML models in a web-based environment, and a Cookbook that contains a collection of guidelines, best practices and lessons learned about systems modeling.
Although this ecosystem offers several tools for designing and analyzing models, there is no support for checking the correctness of the models in a rigorous and automated way. Therefore, we implemented validation and verification services that check the structural correctness of the models and verify that their behavior conforms to the engineers’ expectations.
Example Model
In Figure 1, we can see a model of a simplified Spacecraft and a Ground Station. The Ground Station sends a Start signal to the Spacecraft to start its operation. The Spacecraft sends data packets to the Ground Station every two milliseconds, and its battery decreases simultaneously. If the battery is below 80%, it recharges until it is fully charged. The Ground Station counts the received data packets in a variable and sends a ReceivedPacktes signal via the Status port to the environment about the number of packets it received. (For simplicity reasons, the model omits the technical details about the internal operation and communication between the two entities.)
For illustrative purposes, let’s consider that the Spacecraft shall never transmit when the battery is below 80%, and the Ground Station has already received at least 20 packets. In the top-right corner of the figure, we can see this requirement formalized on a SysML sequence diagram. The diagram references the states and internal variables of the Spacecraft and Ground Station state machines.
We used the sequence diagram formalism to represent reachability properties. A reachability property is a desirable (undesirable) state configuration that may (shall never) occur during the system’s lifetime. If the state configuration occurs, we return an execution trace, depicted as a SysML sequence diagram, which shows the engineer how to model can get into this state configuration.
In the following, we give a quick overview of the Cloud-based workflow that checks if such an execution trace exists (in other words, the model satisfies the reachability property).
The Workflow
In Figure 2, we can see the Cloud-based verification and validation workflow. Systems engineers design the models in their SysML design tool of choice. Then, they upload the models to the model repository (OpenMBEE MMS). From there, IncQuery Server fetches the revision and indexes it. Afterward, engineers open a web browser and start interacting with the workflow via the Jupyter notebook.
First, the Validation and Transformation Service fetches the model from IncQuery Server and validates its structural correctness and consistency. Second, we transform it into intermediate Gamma models. After that, the Gamma models are forwarded to the Model checker runtime, in which the Gamma Framework transforms them to the input formalisms of the model checker backends (UPPAAL or Theta) and calls the chosen model checker to check if the model satisfies the reachability property. If the property is satisfied, then an execution trace is returned that is back-annotated to a SysML sequence diagram (Figure 3). In the last step of the workflow, the sequence diagram is returned to the user.
In Figure 3, we can see an execution trace that has been back-annotated to a sequence diagram. On the diagram, we see the Ground Station and the Spacecraft state machines, and the external ports of the composite system represented on lifelines. The diagram is divided into steps. In each step, we see the active state configuration of the state machines (states and values of the local variables), the incoming and the outgoing signals of the composite system, and the time that was spent between two steps of the trace.
In Figure 3, we show the initial and final state configurations for brevity. In the final configuration, we see that the model satisfies the reachability property because the Spacecraft’s Transmitting state is active, its battery is below 80%, the Ground Station is in the Receiving state, and it has already received 20 packets.
The back-annotated SysML sequence diagram can be used for manual inspection of the execution and, in some cases, to simulate the state machines in a corresponding tool, e.g., Cameo Simulation Toolkit.
Conclusions
In this work, we introduced a Cloud-based workflow to check the correctness of industrial behavioral SysML models. More specifically, to verify that the model satisfies a user-defined reachability property.
Finally, there is only one question to be answered:
How to benefit from the Cloud to proceed toward scalable model checking?
As can be seen in Figure 2, the workflow is based on Kubernetes, an open-source system for automating deployment, scaling, and management of containerized applications. Each module of the workflow is a containerized application that can be deployed in pods on a Kubernetes cluster. The cluster can be built from different (virtual) machines with large computational capacity*. Besides, the Model checker runtime can be deployed in multiple pods, each of them serving separate verification requests. Combining these two aspects opens up the possibility of serving many users concurrently on a large pool of computational resources, i.e., the Cloud.
To learn more about the technical details of scalability with Kubernetes and our first experiments, read our paper in [1].
* On Amazon Web Services, an EKS cluster can consist of EC2 virtual machines that can scale up to 192 vCPUs and up to 384 GiB of memory (i.e., EC2 C6a instances).
Videos and Publication
Check out the video on YouTube, which explains the latest version of the verification and validation workflow:
We published an earlier workflow prototype at the OpenMBEE workshop of the MODELS 2020 conference [3]. Check out the paper to learn more about the details, or watch the workshop talk on YouTube [4]:
Further References
- [1] Horváth, B, Molnár, V, Graics, B, et al. Pragmatic verification and validation of industrial executable SysML models. Systems Engineering. 2023; 1- 22. 📃
- [2] https://www.pakistangulfeconomist.com/2022/11/18/the-usage-of-cloud-computing-in-pakistan/
- [3] Benedek Horváth, Bence Graics, Ákos Hajdu, Zoltán Micskei, Vince Molnár, István Ráth, Luigi Andolfato, Ivan Gomes, Robert Karban: Model checking as a service: towards pragmatic hidden formal methods, MODELS (Companion) 2020, 37:1–37:5. 📃
- [4] Model Checking as a Service: Towards Pragmatic Hidden Formal Methods, YouTube video of OpenMBEE workshop at MODELS 2020 🎦
- [5] Pragmatic Verification and Validation of Industrial Executable SysML Models, YouTube video 🎦
- Gamma Statechart Composition and Verification Framework 🛠
- IncQuery Suite: IncQuery Server, IncQuery Model Viewer, and much more! 🔎🧵 📄
- Lowcomote project 🔬👩🔬👨🔬
Acknowledgments
This research was a collaboration between IncQuery Labs, Critical Systems Research Group, 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.
