A survey of simulation provenance systems: modeling, capturing, querying, visualization, and advanced utilization

A symbolic model checking approach in formal verification of distributed systems

Model checking is an influential method to verify complex interactions, concurrent and distributed systems. Model checking constructs a behavioral model of the system using formal concepts such as operations, states, events and actions. The model checkers suffer some weaknesses such as state space explosion problem that has high memory consumption and time complexity. Also, automating temporal logic is the main challenge to define critical specification rules in the model checking. To improve the model checking weaknesses, this paper presents Graphical Symbolic Modeling Toolkit (GSMT) to design and verify the behavioral models of distributed systems. A behavioral modeling framework is presented to design the system behavior in the forms of Kripke structure (KS) and Labeled Transition System (LTS). The behavioral models are created and edited using a graphical user interface platform in four layers that include a design layer, a modeling layer, a logic layer and a symbolic code layer. The GSMT generates a graphical modeling diagram visually for creating behavioral models of the system. Also, the temporal logic formulas are constructed according to some functional properties automatically. The executable code is generated according to the symbolic model verifier that user can choose the original model or reduced model with respect to a recursive reduced model. Finally, the generated code is executed using the NuSMV model checker for evaluating the constructed temporal logic formulas. The code generation time for transforming the behavioral model is compared to other model checking platforms. The proposed GSMT platform has outperformed evaluation than other platforms.