一种支持实时软件时间建模的形式化方法

随着实时系统非功能性质研究的深入,为了分析软件对系统执行时间的影响并对其进行定量分析,提出了一种支持实时软件时间建模的形式化方法。通过扩展时间通信顺序进程的时间语义,将实时系统指令执行的时间映射成为时间通信顺序进程的时间,利用时间通信顺序进程对实时软件时间建模并进行量化分析。提出的时间最优调度算法可以判断时间通信顺序进程的可达性并计算时间最优路径。通过实例验证表明,该方法可以从很大程度上提高实时系统执行时间计算的准确性,计算结果有助于实时系统执行时间的量化分析与优化设计。

Formal method supporting for time modeling of real-time softwares

With the prog ress of non-funct io nal pro pert ies research on real-time systems, to analyze the effect of so ftw are on system running t ime, a formal metho d was proposed to suppo rt t ime mo deling of realt ime softw ares. By ex tending t ime informat io n on T imed Communicat ing Sequent ial Process ( T imed CSP) , the ex ecut io n t ime of inst ruct ions in real-time systems w as mapped into the t ime of Timed CSP. The execut ion time o f r eal-t ime so ftw ares could be modeled and opt imized using this formal method. A t ime o pt imal scheduling alg orithm w as proposed to est imate the reachability of Timed CSP and to fig ure out the time opt imal path. T he last instance show s that this formal method impro ves the accuracy and ef ficiency of the ex ecut ion t ime calculat io n of real-time systems, and that the calculat ion results can be used to quant itat ively analy ze and opt imize the execut ion t ime of real-t ime systems