An Overview of Sound and Modest Approaches to Quantitative Model Checking from Sea to Space

Quantitative system properties such as resilience, response times, and throughput are crucial measures in the design and operation of complex cyber-physical systems. The formal methods community has developed a variety of approaches to evaluate and optimise such properties with clear correctness and optimality guarantees. In practice, however, every application poses new challenges that require adaptations and novel combinations of the “off-the-shelf” methods we usually present in scientific papers. In this extended abstract accompanying the author’s FMICS 2025 invited presentation, we use recent case studies ranging from water management for storm surge protection to routing in satellite constellations to (i) contrast the different demands on model expressiveness and tool capabilities of each application and (ii) highlight the capabilities of the Modest Toolset to solve these challenges with the varied modelling, simulation, and verification approaches it implements. In addition to these examples, we outline how quantitative verification tools can deliver the correctness and optimality guarantees we would like to see.