论文标题
定时自动机中的参数非干预
Parametric non-interference in timed automata
论文作者
论文摘要
我们考虑定时自动机（TAS）的不干预概念，该概念允许量化攻击的频率；也就是说，我们推断出攻击者的两个连续动作之间的最小时间值，以便他打扰了可及地点的集合。我们还将保证不干预的TA（被视为参数）的定时常数合成估值。我们表明，这可以降低参数定时自动机中的可及性合成。我们将我们的方法应用于Fischer相互排除方案的模型，并获得初步结果。
We consider a notion of non-interference for timed automata (TAs) that allows to quantify the frequency of an attack; that is, we infer values of the minimal time between two consecutive actions of the attacker, so that (s)he disturbs the set of reachable locations. We also synthesize valuations for the timing constants of the TA (seen as parameters) guaranteeing non-interference. We show that this can reduce to reachability synthesis in parametric timed automata. We apply our method to a model of the Fischer mutual exclusion protocol and obtain preliminary results.
