Using model checking to analyze the system behavior of the LHC production grid
Formal methods are applied to model the grid system DIRAC used in the LHC experiment. The model enabled localizing race conditions and livelocks in the system. The discovered problems were notoriously difficult to trace with traditional testing. The mCRL2 tool is used for understanding the subtle concurrent-component interactions. General guidelines are given for modeling shared-memory distributed systems.
model checking lhc grid distributed system process algebra workflow