Uncover: Using Coverability Analysis for Verifying Graph Transformation Systems

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9151
• 期：1
• 页码：266-274
• 全文大小：225 KB
• 参考文献：1. Abdulla, P.A., Bouajjani, A., Cederberg, J., Haziza, F., Rezine, A.: Monotonic abstraction for programs with dynamic memory heaps. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 341鈥?54. Springer, Heidelberg (2008) View Article
  2.Abdulla, P.A., C虇er膩ns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS 1996, pp. 313鈥?21. IEEE (1996)
  3.AUGUR2. http://鈥媤ww.鈥媡i.鈥媔nf.鈥媢ni-due.鈥媎e/鈥媟esearch/鈥媡ools/鈥媋ugur2/鈥?/span>
  4. Bansal, K., Koskinen, E., Wies, T., Zufferey, D.: Structural counter abstraction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 62鈥?7. Springer, Heidelberg (2013) View Article
  5.Bertrand, N., Delzanno, G., K枚nig, B., Sangnier, A., St眉ckrath, J.: On the decidability status of reachability and coverability in graph transformation systems. In: Proceedings of RTA 2012, vol. 15 of LIPIcs, pp. 101鈥?16 (2012)
  6. Delzanno, G., St眉ckrath, J.: Parameterized verification of graph transformation systems with whole neighbourhood operations. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 72鈥?4. Springer, Heidelberg (2014)
  7.Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1鈥?), 63鈥?2 (2001)MathSciNet View Article
  8.Graph Backwards Tool (GB). http://鈥媤ww.鈥媔t.鈥媢u.鈥媠e/鈥媟esearch/鈥媑roup/鈥媘obility/鈥媋dhoc/鈥媑bt
  9.Graphviz website. http://鈥媤ww.鈥媑raphviz.鈥媜rg/鈥?/span>
  10.GROOVE. http://鈥媑roove.鈥媍s.鈥媢twente.鈥媙l/鈥?/span>
  11.Holt, R.C., Sch眉rr, A., Sim, S.E., Winter, A.: GXL. http://鈥媤ww.鈥媑upro.鈥媎e/鈥婫XL/鈥?/span>
  12. Joshi, S., K枚nig, B.: Applying the graph minor theorem to the verification of graph transformation systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 214鈥?26. Springer, Heidelberg (2008) View Article
  13. K枚nig, B., St眉ckrath, J.: Well-structured graph transformation systems with negative application conditions. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 81鈥?5. Springer, Heidelberg (2012) View Article
  14. K枚nig, B., St眉ckrath, J.: A general framework for well-structured graph transformation systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 467鈥?81. Springer, Heidelberg (2014)
  15.Meyer, R.: Structural stationarity in the \(\pi \) -calculus. Ph.D. thesis, Carl-von-Ossietzky-Universit盲t Oldenburg (2009)
  16.Robertson, N., Seymour, P.: Graph minors XXIII. Nash-Williams鈥?immersion conjecture. J. Comb. Theory, Ser. B 100, 181鈥?05 (2010)MathSciNet View Article
  17. Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation: Volume 1: Foundations. World Scientific Publishing, River Edge (1997)
  18. Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 18鈥?2. Springer, Heidelberg (2008) View Article
  19.St眉ckrath, J.: UNCOVER. http://鈥媤ww.鈥媡i.鈥媔nf.鈥媢ni-due.鈥媎e/鈥媟esearch/鈥媡ools/鈥媢ncover/鈥?/span>
  
• 作者单位：Jan St眉ckrath (15)
  
  15. Universit盲t聽Duisburg-Essen, Essen, Germany
  
• 丛书名：Graph Transformation
• ISBN：978-3-319-21145-9
• 刊物类别：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

文摘

Uncover is a tool for high level verification of distributed or concurrent systems. It uses graphs and graph transformation rules to model these systems in a natural way. Errors in such a system are modelled by upward-closed sets for which two orders are provided, the subgraph and the minor ordering. We can then exploit the theory of well-structured transition systems to obtain exact or approximating decidability results (depending on the order and system) for the question whether an error can occur or not. For this framework we also introduced an extension of classical graph transformation which is capable of modelling broadcast protocols.