Abstract

Many safety critical systems involve mobility and real-time constraints. Examples can be found in robotics as well as in train and traffic control. The talk presents the Shape Calculus, a spatio-temporal logic based on an n-dimensional Duration Calculus, which is tailored for the specification and verification of this class of systems. After providing elementary properties like decidability and axiomatisation, a practical approach to automatic verification is presented which is built upon the WS1S verifier MONA as a backend.