论文标题
先发空实时系统的状态空间基于时间距离的计算
Time distance based computation of the state space of preemptive real time systems
论文作者
论文摘要
我们在本文中探讨了一种新颖的方法，该方法对先发制人实时系统的状态空间过度贴合。我们的图形构造将类的表达扩展到了时间距离系统，该时间距离系统编码了过去射击子序列的定量属性。这使得可以恢复相关的时间信息，这些信息将更多地拧紧可触及类的DBM过度应用。因此，我们成功地构建了有效地更紧密的近似图，这更合适地恢复了模型的定量属性。仿真结果表明，计算的图与确切图的大小相同，同时改善了其计算所需的时间。
We explore in this paper a novel approach that builds an overapproximation of the state space of preemptive real time systems. Our graph construction extends the expression of a class to the time distance system that encodes the quantitative properties of past fired subsequences. This makes it possible to restore relevant time information that is used to tighten still more the DBM overapproximation of reachable classes. We succeed thereby to build efficiently tighter approximated graphs which are more appropriate to restore the quantitative properties of the model. The simulation results show that the computed graphs are of the same size as the exact graphs while improving by far the times needed for their computation.
