Abstract
In this paper we present the RERS challenge 2015, a free-style program analysis challenge on reactive systems to evaluate the effectiveness of different validation and verification techniques. It brings together researchers from different areas including static analysis, model checking, theorem proving, symbolic execution, and testing. The challenge characteristics and set-up are discussed, while special attention is given to the Runtime Verification track that was newly introduced.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
RERS originally was an acronym for Regular Extrapolation of Reactive Systems. Although the acronym remained, the challenge itself has evolved towards a broader focus, which lead to a change of the name and scope.
References
RERS challenge website. http://www.rers-challenge.org/
Almeida, E.E., Luntz, J.E., Tilbury, D.M.: Event-condition-action systems for reconfigurable logic control. IEEE Trans. Autom. Sci. Eng. 4(2), 167–181 (2007)
Beyer, D.: Status report on software verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 373–388. Springer, Heidelberg (2014)
Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proceeding PLDI, pp. 300–309. ACM (2007)
Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472. Springer, Heidelberg (2005)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (2001)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceeding ICSE, pp. 411–420. ACM (1999)
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–123 (2001)
Havelund, K., Roşu, G.: Monitoring Java programs with Java PathExplorer. ENTCS 55(2), 200–217 (2001)
Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Softw. Test. Verification Reliab. 11(2), 65–79 (2001)
Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS Grey-Box Challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 608–614. Springer, Heidelberg (2012)
Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Păsăreanu, C.: Rigorous Examination of Reactive Systems. The RERS Challenges 2012 and 2013. Softw. Tools Technol. Transfer 16(5), 457–464 (2014)
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)
Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Rou, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Verification. Lecture Notes in Computer Science, vol. 6418, pp. 122–135. Springer, Berlin Heidelberg (2010)
Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293–303 (2009)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
Steffen, B., Howar, F., Isberner, M., Naujokat, S., Margaria, T.: Tailored generation of concurrent benchmarks. Int. J. Softw. Tools Technol. Transf. 16(5), 543–558 (2014)
Steffen, B., Howar, F., Merten, M.: Introduction to active automata learning from a practical perspective. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 256–296. Springer, Heidelberg (2011)
Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Softw. Tools Technol. Transfer 16(5), 465–479 (2014)
Acknowledgment
We would like to thank Ylis Falcone, Jaco van de Pol, and Markus Schordan for their feedback regarding the challenge problems, and for serving as members of the RERS 2015 Committee.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Geske, M., Isberner, M., Steffen, B. (2015). Rigorous Examination of Reactive Systems:. In: Bartocci, E., Majumdar, R. (eds) Runtime Verification. Lecture Notes in Computer Science(), vol 9333. Springer, Cham. https://doi.org/10.1007/978-3-319-23820-3_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-23820-3_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23819-7
Online ISBN: 978-3-319-23820-3
eBook Packages: Computer ScienceComputer Science (R0)