Measuring behavioral correspondence to a timed concurrent model

Research in formal methods has produced fruitful techniques that can verify global properties of a design of a real-time system, or exact behavioral correspondence to the design. Exactness is often not achieved, however, and yet understanding how close the design and system correspond still would be very valuable, to direct further efforts in achieving exactness or to modify the design where the system simply cannot achieve the requirements. This paper describes a method and tool that fills this niche, by quantitatively measuring how closely the behavior of a real-time system corresponds to its specification, given in a timed, concurrent model.