Rigorous examination of reactive systems
详细信息 查看全文
- 作者：Falk Howar (1)
Malte Isberner (2)
Maik Merten (2)
Bernhard Steffen (2)
Dirk Beyer (3)
Corina S. P膬s膬reanu (1) - 关键词：Program analysis ; Model checking ; Verification ; Model ; based testing ; Competition ; Reactive system ; Event鈥揷ondition鈥揳ction system
- 刊名：International Journal on Software Tools for Technology Transfer (STTT)
- 出版年：2014
- 出版时间：October 2014
- 年：2014
- 卷：16
- 期：5
- 页码：457-464
- 全文大小：258 KB
- 参考文献：1. Almeida, E.E., Luntz, J.E., Tilbury, D.M.: Event-condition鈥揳ction systems for reconfigurable logic control. IEEE Trans. Autom. Sci. Eng. 4(2), 167鈥?81 (2007) CrossRef
2. Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87鈥?06 (1987) CrossRef
3. Bauer, O., Geske, M., Isberner, M.: Analyzing program behavior through active automata learning. Int. J. Softw. Tools Technol. Transf. doi:10.1007/s10009-014-0333-2 (2014)
4. Benatallah, B., Sheng, Q.Z., Dumas, M.: The Self鈥揝erv environment for web-services composition. Internet Comput. IEEE 7(1), 40鈥?8 (2003) CrossRef
5. Beyer, D.: Competition on software verification (SV-COMP). In: Proceedings of TACAS, LNCS 7214, pp. 504鈥?24. Springer (2012)
6. Beyer, D.: Second competition on software verification. In: Proceedings od TACAS, LNCS 7795, pp. 594鈥?09. Springer (2013)
7. Beyer, D.: Status report on software verification. In: Proceedings of TACAS, LNCS 8413, pp. 373鈥?88. Springer (2014)
8. Beyer, D., Henzinger, T. A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proceedings of PLDI, pp. 300鈥?09. ACM (2007)
9. Beyer, D., Stahlbauer, A.: BDD-based software model checking with CPAchecker. In: Proceedings of MEMICS, LNCS 7721, pp. 1鈥?1. Springer (2013)
10. Beyer, D., Stahlbauer, A.: BDD-based software verification: applications to event-condition鈥揳ction systems. Int. J. Softw. Tools Technol. Transf. doi:10.1007/s10009-014-0334-1 (2014)
11. Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Proceedings of FSTTCS, LNCS 1026, pp. 499鈥?13. Springer (1995)
12. Blom, S.C.C., van de Pol, J.C., Weber, L.T., Smin, M.: Distributed and symbolic reachability. In: Proceedings of CAV, LNCS 6174, pp. 354鈥?59. Springer (2010)
13. Boyer, J., Mili, H.: IBM WebSphere ILOG JRules. In: Agile Business Rule Development, pp. 215鈥?42. Springer (2011)
14. Browne, P.: JBoss Drools Business Rules: Capture, Automate, and Reuse Your Business Processes in a Clear English Language that Your Computer Can Understand. Packt Publishing (2009)
15. Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (editors): Model-based testing of reactive systems. In: LNCS 3472. Springer (2005)
16. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, USA (2001)
17. Cok, D. R., Griggio, A., Bruttomesso, R., Deters, M.: The 2012 SMT competition. In: Proceedings of SMT, pp. 131鈥?42 (2012)
18. Col贸n, M., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Proceedings of CAV, LNCS 2725, pp. 420鈥?32. Springer (2003)
19. Cuoq, P., Signoles, J., Baudin, P., Bonichon, R., Canet, G., Correnson, L., Monate, B., Prevosto, V., Puccetti, A.: Experience report: OCaml for an industrial-strength static analysis framework. In: Proceedings of ICFP, pp. 281鈥?86. ACM (2009)
20. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of ICSE, pp. 411鈥?20. ACM (1999)
21. Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Softw. Eng. 27(2), 99鈥?23 (2001) CrossRef
22. Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Proceedings of VMCAI, pp. 120鈥?35 (2009)
23. Havelund, K., Ro艧u, G.: Monitoring Java programs with Java PathExplorer. ENTCS 55(2), 200鈥?17 (2001)
24. Hayes-Roth, F.: Rule-based systems. Commun. ACM 28(9), 921鈥?32 (1985) CrossRef
25. Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Softw. Test. Verif. Reliab. 11(2), 65鈥?9 (2001) CrossRef
26. Howar, F., Isberner, M., Merten, M., Steffen, B., and Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Proceedings of ISoLA, LNCS 7609, pp. 608鈥?14. Springer (2012)
27. Huisman, M., Klebanov, V., Monahan, R.: On the organisation of program-verification competitions. In: Proceedings of COMPARE, CEUR Workshop Proceedings 873, pp. 50鈥?9. CEUR-WS.org (2012)
28. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385鈥?94 (1976) CrossRef
29. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Alg. Progr. 78(5), 293鈥?03 (2009) CrossRef
30. Lidman, J., Quinlan, D.J., Liao, C., McKee, S.A.: ROSE:FTTransform鈥攁 source-to-source translation framework for exascale fault-tolerance research. In: Proceedings of FTXS. IEEE (2012)
31. McCarthy, D., Dayal, U.: The architecture of an active database management system. In: Proceedings of ICMD, pp. 215鈥?24. ACM (1989)
32. Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Context-bounded model checking of LTL properties for ANSI-C software. In: Proceedings of SEFM, LNCS 7041, pp. 302鈥?17. Springer (2011)
33. Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Applying symbolic bounded model checking to the: RERS greybox challenge, p. 2014. J. Softw. Tools Technol. Transf. Int. doi:10.1007/s10009-014-0335-0 (2014)
34. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York, USA (1999)
35. Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transf. doi:10.1007/s10009-014-0338-x (2014)
36. Steffen, B., Howar, F., Isberner, M., Naujokat, S., Margaria, T.: Tailored generation of concurrent benchmarks. Int. J. Softw. Tools Technol. Transf. doi:10.1007/s10009-014-0339-9 (2014)
37. Steffen, B., Howar, F., Merten, M.: Introduction to active automata learning from a practical perspective. In: Proceedings of SFM, LNCS 6659, pp. 256鈥?96. Springer (2011)
38. Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Int. J. Softw. Tools Technol. Transf. doi:10.1007/s10009-014-0336-z (2014)
39. Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35鈥?8 (2006)
40. van de Pol, J., Ruys, T. C., te Brinke, S.: Thoughtful brute force attack of the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transf. doi:10.1007/s10009-014-0324-3 (2014) - 作者单位：Falk Howar (1)
Malte Isberner (2)
Maik Merten (2)
Bernhard Steffen (2)
Dirk Beyer (3)
Corina S. P膬s膬reanu (1)
1. Carnegie Mellon Silicon Valley/NASA Ames, Mountain View, USA
2. TU Dortmund, Dortmund, Germany
3. University of Passau, Passau, Germany - ISSN：1433-2787
文摘
The goal of the RERS challenge is to evaluate the effectiveness of various verification and validation approaches on reactive systems, a class of systems that is highly relevant for industrial critical applications. The RERS challenge brings together researchers from different areas of software verification and validation, including static analysis, model checking, theorem proving, symbolic execution, and testing. The challenge provides a forum for experimental comparison of different techniques on specifically designed verification tasks. These benchmarks are automatically synthesized to exhibit chosen properties, and then enhanced to include dedicated dimensions of difficulty, such as conceptual complexity of the properties (e.g., reachability, safety, liveness), size of the reactive systems (a few hundred lines to millions of lines), and complexity of language features (arrays and pointer arithmetic). The STTT special section on RERS describes the results of the evaluations and the different analysis techniques that were used in the RERS challenges 2012 and 2013.