Real-time property preservation in concurrent real-time systems
Jinfeng Huang, Jeroen P. M. Voeten, Marc C. W. Geilen · TU/e Research Portal · 2004
A key step in concurrent real-time system development is to build a model from which the implementation is synthesized. It is thus important to understand the relation between the properties of a model and its corresponding implementation. In this paper, we first build two relations: 1) #-weakening relations on MITLR formulas, which are used to express real-time properties of the system, and 2) #-neighboring relations on timed state sequences, which are used to describe the timing behavior of the system. Based on these relations, we formally prove the real-time property preservation in approximations of concurrent real-time systems. This result generalizes [11], which is restricted to sequential real-time systems. Finally, we demonstrate how the result can be applied to the real-time system development by a case study of a rail-road crossing system.