Translating SysML Activity Diagrams for nuXmv Verification of an Autonomous Pancreas

Orion Staskal, Josh Simac, Logan Swayne, Kristin Y. Rozier

This webpage contains further details and artifacts for reproducibility of the experiments in "Translating SysML Activity Diagrams for nuXmv Verification of an Autonomous Pancreas" by O. Staskal, J. Simac, L. Swayne, K.Y. Rozier

---

Results

We evaluate our AAPS nuXmv model against LTL and CTL specifications derived from the SysML model.

Model to regenerate all results in the paper can be found here.