Symbolic Model-Checking Using ITS-Tools. We present verification toolset ITS-tools, featuring a symbolic model-checking back-end engine based on hierarchical set decision diagrams (SDD) that supports reachability, CTL and LTL model-checking and a user-friendly eclipse based front-end. Using model transformations to a Guarded Action Language (GAL) as intermediate format, ITS-tools can analyze third party (Uppaal, Spin, Divine...) specifications.
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Finkbeiner, Bernd; Gieseking, Manuel; Hecking-Harbusch, Jesko; Olderog, Ernst-Rüdiger: Model checking data flows in concurrent network updates (2019)
- Garavel, Hubert: Nested-unit Petri nets (2019)