Breakthrough Software Tool STAMINA Ensures Safety and Reliability in Complex Computer Systems

A new software tool has been developed by computer engineering researchers at Utah State University, designed to rigorously analyze complex computer systems — especially those where safety and mission-critical operations are at stake.

STAMINA, which stands for STochastic Approximate Model-checker for INfinite-state Analysis, is a valuable resource for synthetic biologists, computer engineers and system designers. It provides probabilistic model checking, which is used to ensure that systems with uncertain or random behaviors work correctly. These could be systems like synthetic biology networks, biochemical reactions, queuing networks or reliability engineering.

Assistant Professor Zhen Zhang, along with his Ph.D. student Joshua Jeppson and Associate Professor Chris Winstead, published their research in the 20th International Conference on Quantitative Evaluation of Systems this September.

STAMINA focuses on continuous-time Markov chain, or CTMC, models, which are used to model probabilistic systems like genetic regulatory networks . The challenge with CTMC models is that they often have infinite or very large finite state spaces — which represent the set of all possible configurations of a system — making traditional probabilistic model checking methods impractical. STAMINA can shorten the input CTMC model’s state space to enable probabilistic model checking, which then can scale formal analysis for complex real-world probabilistic system designs.

A second version of STAMINA, called STAMINA 2.0, is integrated with the STORM probabilistic model checker . STORM is a software tool used to analyze and verify finite-state probabilistic systems , but it cannot handle infinite-state systems. When STAMINA and STORM work together, they make the analysis of complex systems much more efficient and scalable.

“STAMINA is designed to analyze both bounded and unbounded CTMCs,” Zhang said. “It can efficiently produce accurate probability bounds for properties under verification and aims to improve the scalability of probabilistic model checking tools, making it suitable for real-world system designs.”

STAMINA is continually evolving and improving as more research is conducted, making it a state-of-the-art formal verification tool for probabilistic computing systems.

For more information, visit the STAMINA’s website at staminachecker.org.

###

Writer: Sydney Dahle, sydney.dahle@usu.edu, 435-797-7512

Contact: Zhen Zhang, zhen.zhang@usu.edu, 435-797-9068