Reproducible Simulations, Trace Visualization and Model Exploration with Dynamic Partial Order Reduction in Real-Time ABS

Local traces are our means for recording and (deterministically) replaying Real-Time ABS models. The traces capture communication between actors in a model, and a tool has been developed for visualizing them. From a given trace, we can generate new traces, that can be executed by the Real-Time ABS simulator; doing this exhaustively results in a stateless model checker. To avoid redundant model exploration, we apply a technique called dynamic partial order reduction, which establishes equivalence classes of traces. The exploration algorithm is implemented in a highly parallelizable manner, using a database to persistently store the state of the search. As future work, we plan to persist the object states along with the traces, where global properties can be asserted by the means of writing database queries.  

hosted by