摘要：In this paper we report on an application and extension of the theory of Timed Modal Specifications (TMS) and its associated verification tool E PSILON . The novel feature with which E PSILON has been extended is the ability to automatically generate diagnostic information in cases of erroneous refinement steps.
