Reachability Preservation Based Parameter Synthesis for Timed Automata

详细信息    查看全文

• 作者：脡tienne Andr茅 (16)
  Giuseppe Lipari (17)
  Hoang Gia Nguyen (16)
  Youcheng Sun (18)
  
  16. Universit茅 Paris 13 ; Sorbonne Paris Cit茅 ; LIPN ; CNRS ; UMR 7030 ; Paris ; France
  17. CRIStAL 鈥?UMR 9189 ; Universit茅 de Lille ; USR 3380 CNRS ; Lille ; France
  18. Scuola Superiore Sant鈥橝nna ; Pisa ; Italy
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9058
• 期：1
• 页码：50-65
• 全文大小：340 KB
• 参考文献：1. Alur, R, Dill, DL (1994) A theory of timed automata. Theoretical Computer Science 126: pp. 183-235 CrossRef
  2. Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592鈥?01. ACM (1993)
  3. Andr茅, 脡, Chatain, T, Encrenaz, E, Fribourg, L (2009) An inverse method for parametric timed automata. IJFCS 20: pp. 819-836
  4. Andr茅, 脡., Coti, C., Evangelista, S.: Distributed behavioral cartography of timed automata. In: EuroMPI/ASIA 201414, pp. 109鈥?14. ACM (2014)
  5. Andr茅, 脡, Fribourg, L Behavioral cartography of timed automata. In: Ku膷era, A, Potapov, I eds. (2010) Reachability Problems. Springer, Heidelberg, pp. 76-90 CrossRef
  6. Andr茅, 脡, Fribourg, L, K眉hne, U, Soulat, R IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D, M茅ry, D eds. (2012) FM 2012: Formal Methods. Springer, Heidelberg, pp. 33-36 CrossRef
  7. Andr茅, 脡, Soulat, R Synthesis of timing parameters satisfying safety properties. In: Delzanno, G, Potapov, I eds. (2011) Reachability Problems. Springer, Heidelberg, pp. 31-44 CrossRef
  8. Bozzelli, L, Torre, S (2009) Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design 35: pp. 121-151 CrossRef
  9. Bucci, G, Fedeli, A, Sassoli, L, Vicario, E (2004) Timed state space analysis of real-time preemptive systems. Transactions on Software Engineering 30: pp. 97-111 CrossRef
  10. Chevallier, R, Encrenaz-Tiph猫ne, E, Fribourg, L, Xu, W (2009) Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design 34: pp. 59-81 CrossRef
  11. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with IC3. In: FMCAD, pp. 165鈥?68. IEEE (2013)
  12. Cimatti, A., Palopoli, L., Ramadian, Y.: Symbolic computation of schedulability regions using parametric timed automata. In: RTSS, pp. 80鈥?9. IEEE Computer Society (2008)
  13. Hune, T, Romijn, J, Stoelinga, M, Vaandrager, FW (2002) Linear parametric model checking of timed automata. JLAP 52鈥?3: pp. 183-220
  14. Jovanovi膰, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Transactions on Software Engineering (2014, to appear)
  15. Laarman, A, Olesen, MC, Dalsgaard, AE, Larsen, KG, Pol, J Multi-core emptiness checking of timed b眉chi automata using inclusion abstraction. In: Sharygina, N, Veith, H eds. (2013) Computer Aided Verification. Springer, Heidelberg, pp. 968-983 CrossRef
  16. Lime, D, Roux, OH, Seidner, C, Traonouez, L-M Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S, Philippou, A eds. (2009) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Heidelberg, pp. 54-57 CrossRef
  
• 作者单位：NASA Formal Methods
• 丛书名：978-3-319-17523-2
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

The synthesis of timing parameters consists in deriving conditions on the timing constants of a concurrent system such that it meets its specification. Parametric timed automata are a powerful formalism for parameter synthesis, although most problems are undecidable. We first address here the following reachability preservation problem: given a reference parameter valuation and a (bad) control state, do there exist other parameter valuations that reach this control state iff the reference parameter valuation does? We show that this problem is undecidable, and introduce a procedure that outputs a possibly underapproximated answer. We then show that our procedure can efficiently replace the behavioral cartography to partition a bounded parameter subspace into good and bad subparts; furthermore, our procedure can even outperform the classical bad-state driven parameter synthesis semi-algorithm, especially when distributed on a cluster.