Search for a command to run...
# Artifact: Semantifyr for SysML v2 --- A Semantic Library Approach to Formal Verification This is the artifact accompanying the paper: > **Semantifyr for SysML v2: A Semantic Library Approach to Formal Verification**> Ármin Zavada, Bence Graics, Ákos Horváth, Vince Molnár> ACM/IEEE 29th International Conference on Model Driven Engineering Languages and Systems (MODELS '26) ## Overview **Semantifyr** is a language and framework for semantic library-driven formal verification of engineering models. Engineering models are mapped to reusable semantic library concepts authored in the Semantifyr declarative-operational language, which are then unfolded into the XSTS (Extended Symbolic Transition System) formalism and verified via model checking. This artifact contains the https://github.com/ftsrg/semantifyr checked out at commit `a5e130a69d2a9f9f109f440f4860f089bae2d481`. ## Test Models See `subprojects/frontends/sysmlv2/sysmlv2-semantics/TestModels`. ## Requirements - **Java 25** (OpenJDK 25 or later) ## Building the Project ```bash./gradlew build``` This assembles and tests the project, including regression testing and formal verifications. The required environment is automatically managed by Gradle, including the Theta binaries, and SysIDE extended with Semantifyr. The build should complete in 10-20 minutes. Note, that our SysIDE extension -- which is a fork -- is managed as a local git repository, and the pnpm scripts are executed by Gradle. Due to the integration of Gradle and PNPM, sometimes the build script fails silently, and the SysIDE frontend does not assemble the required standard library. This results in errors where SysIDE does not find elements from the standard library. To fix clean the project, and try again. ## Reproducing the Evaluation ### RQ1 --- Semantic Correctness To run the semantic validation suite and the standard verification cases: ```bash./gradlew :sysmlv2-semantics:testVerificationCases``` This runs all verification cases except for the uncompressed Spacecraft model (which may exceed the default timeout). To run all verification cases, including the uncompressed Spacecraft model (some cases will timeout): ```bash./gradlew :sysmlv2-semantics:allTests``` ### RQ2 --- Benchmarking (Unfolding Overhead) To reproduce the benchmark measurements from the paper: ```bash./gradlew benchmarkVerificationCases -Pbenchmark.runs=5``` Results are written to `subprojects/frontends/sysmlv2/sysmlv2-semantics/TestModels/benchmark-results.json`. Each verification case is run 5 times (configurable via `-Pbenchmark.runs=N`) and timing results are aggregated. The benchmark reports both the unfolding time (Semantifyr) and the model checking time (Theta) separately. ## Online Demonstration An online demonstration of the Semantifyr toolchain is available at:https://ftsrg.mit.bme.hu/semantifyr ## Related Repositories - **Semantifyr** (this repository): https://github.com/ftsrg/semantifyr- **SysML v2 Frontend** (SysIDE fork): https://github.com/arminzavada/sysml-2ls/tree/semantifyr-integration ## License Semantifyr is available under the [Eclipse Public License - v 2.0](https://www.eclipse.org/legal/epl-2.0/).