Formal Verification Of A Shopping Basket Application Model Using PRISM

TL;DR

This paper demonstrates the use of the PRISM model checker to formally verify a shopping basket application's behavior, ensuring correctness and accessibility in the shopping process model.

Contribution

It applies formal verification techniques to a shopping application model using PRISM, showcasing how model checking can validate complex software behaviors.

Findings

Successful simulation of shopper behavior states

Verification of accessibility and reachability properties

Validation of the shopping process model

Abstract

Formal verification is at the heart of model validation and correctness. With model checking, invaluable realizations have been accomplished in software engineering and particularly in software development. By means of this approach, complex applications can be simulated and their performance forecasted in light with requirements at hands and expected performance. In this short paper we present the results of a simulation using Prism Model Checker for a Shopping Basket Application Model. Applied on a modified model from a projected process model, the objective is to simulate the behavior of shoppers as they go through a number of defined states of the shopping process and express accessibility and reachability through a number of defined properties.