Towards stronger property preservation in real-time system synthesis
Oana Florescu, Jinfeng Huang, Jpm Jeroen Voeten, Henk Corporaal · TU/e Research Portal · 2006
A key aspect in concurrent real-time system development is to build a model from which a "correct" implementation can be synthesised.Hence, it is important to understand the relation between the properties of a model and of its corresponding implementation.In this paper, we use timed action sequences to describe the behaviour of a real-time system.We first define a notion of distance as a metric to express the observable property preservation between timed action sequences.Furthermore, considering both model and implementation as sets of timed action sequences, we show that a smaller distance between them, and hence a stronger observable property preservation, is obtained when urgency on the execution of observable actions is imposed over the execution of unobservable ones.Based on this result, we extend a previous model synthesis approach to generate from a model an implementation with stronger property preservation.By means of a case study, we show how the proposed approach can be applied to the development of real-time systems.