Spatio-temporal Model Checking for Mobile Real-Time Systems

摘要

This paper presents an automatic verification method for combined temporal and spatial properties of mobile real-time systems. We provide a translation of the Shape Calculus (SC), a spatio-temporal extension of Duration Calculus, into weak second order logic of one successor (WS1S). A prototypical implementation facilitates successful verification of spatio-temporal properties by translating SC specifications into the syntax of the WS1S checker MONA. For demonstrating the formalism and tool usage, we apply it to the benchmark case study "generalised railroad crossing" (GRC) enriched by requirements inexpressible in non-spatial formalisms.