loading...
Correctness-preserving synthesis for real-time control software
Beijing, China October 27-October 28
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QSIC.2006.21Sixth International Conference on Qua ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Jinfeng Huang, Eindhoven University of Technology, The Netherlands
Jeroen Voeten, Eindhoven University of Technology, The Netherlands; Embedded systems institute, The Netherlands
Henk Corporaal, Eindhoven University of Technology, The Netherlands
Formal theories for real-time systems (such as timed process algebra, timed automata and timed petri nets) have gained great success in the modelling of concurrent timing behavior and in the analysis of real-time properties. However, due to the ineliminable timing differences between a model and its realization, synthesising a software realization from a model in a correctness-preserving way is still a challenging research topic. In this paper, we tackle this problem by solving a set of sub-problems. First, we introduce property relations between real-time systems on the basis of their absolute and relative timing differences. Second, we bridge the timing differences between a model and its realization by a sequence of (absolute and relative) timing differences. Third, we propose two parameterised hypotheses to capture the timing differences between the model and its realization. The parameters of both hypotheses are used to predict the real-time properties of the realization from those of the model. Finally, we introduce a synthesis tool, which shows that the two hypotheses can be satisfied during software synthesis.
Citation:
Jinfeng Huang, Jeroen Voeten, Henk Corporaal, "Correctness-preserving synthesis for real-time control software," qsic, pp.65-73, Sixth International Conference on Quality Software (QSIC'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.