Abstract

Many critical systems industry-wide demand fail-safe process execution. Many of these systems are beginning to use low-code or no-code (LC/NC) solutions to their problems. Mechanisms for verifying the integrity of LC/NC solutions are extremely limited in comparison to traditional code. One solution exhaustively searches the execution state space for undesirable behavior, but it requires expertise in model checking and extensive manual labor. Additionally, error output from that method is exclusively text-based and demands time and familiarity to comprehend. We introduce a tool for automating model checking of LC/NC solutions. Participation in the automation process requires very little knowledge of the underlying model checking tools. We demonstrate the effectiveness of the tool using examples of models including subtle-but-critical errors. We present an extensible model to demonstrate the scalability of the automated verification tool. We also introduce an understandable visual representation of model failures to enable quick iteration on subsequent model versions. The visual representation is critical to understanding why a model doesn't comply with given temporal properties. We conclude that model checking is a viable method for verifying LC/NC systems.

Degree

College and Department

Computational, Mathematical, and Physical Sciences; Computer Science

Rights

https://lib.byu.edu/about/copyright/