Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 5/2014

01.10.2014 | RERS

Thoughtful brute-force attack of the RERS 2012 and 2013 Challenges

verfasst von: Jaco van de Pol, Theo C. Ruys, Steven te Brinke

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2014

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

The Rigorous Examination of Reactive Systems’ (rers) Challenges provide a forum for experimental evaluation based on specifically synthesized benchmark suites. In this paper, we report on our ‘brute-force attack’ of the rers 2012 and 2013 Challenges. We connected the rers problems to two state-of-the-art explicit state model checkers: LTSmin and Spin. Apart from an effective compression of the state vector, we did not analyze the source code of the problems. Our brute-force approach was successful: it won both editions of the rers Challenge.
Vorheriger Artikel Property-driven benchmark generation: synthesizing programs of realistic structure
Nächster Artikel Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
Rationale of the rers Challenge from [16].
 
Literatur
1.
Blom, S.C.C., van de Pol, J.C., Weber, M.: ltsmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) Proceedings of CAV 2010 LNCS 6174, pp. 354–359. Springer, New York (2010)
2.
Evangelista, S., Laarman, A., Petrucci, L., van de Pol, J.: Improved multi-core nested depth-first search. In: Chakraborty, S., Mukund, M. (eds.) Proceedings of ATVA 2012, LNCS 7561, pp. 269–283. Springer, New York (2012)
3.
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of the 13th International Conference on Computer Aided Verification (CAV’01), Paris, vol. 2102. Lecture Notes in Computer Science, pp. 53–65. Springer, New York (2001)
4.
Holzman, G.J.: The Spin Model Checker—Primer and Reference Manual. Addison-Wesley, Boston (2003)
5.
Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Graf, S., Mounier, L. (eds.) Proceedings of SPIN 2004 LNCS 2989, pp. 76–91. Springer, New York (2004)
6.
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.) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, vol. 7609. Lecture Notes in Computer Science, pp. 608–614. Springer, Berlin (2012)
7.
Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous Examination of Reactive Systems. The RERS Challenges 2012 and 2013. Software Tools for Technology Transfer. doi:10.​1007/​s10009-014-0337-y (2014)
8.
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the First Symposium on. Logic in Computer Science, pp. 332–344. IEEE Computer Society (1986)
9.
Laarman, A.W., van de Pol, J.C., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Bloem, R., Sharygina, N. (eds.) Proceedings of FMCAD 2010, pp. 247–255. IEEE (2010)
10.
Laarman, A.W., van de Pol, J.C., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) Proceedings of NFM 2011, LNCS 6617, pp. 506–511. Springer, New York (2011)
11.
Laarman, A.W., van de Pol, J.C., Weber, M.: Parallel recursive state compression for free. In: Groce, A., Musuvathi, M. (eds.) Proceedings of SPIN 2011, LNCS 6823, pp. 38–56. Springer, New York (2011)
12.
Ruys, T.C., Kars, P.: Gossiping girls are all alike. In: Donaldson, A.F., Parker, D. (eds.) Proceedings of SPIN 2012, LNCS 7385, pp. 117–136. Springer, New York (2012)
13.
Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Softw. Tools Technol. Transf. doi:10.​1007/​s10009-014-0336-z (2014)
14.
van der Vegt, S., Laarman, A.W.: A parallel compact hash table. In: Kotásek, Z., Bouda, J., Cerná, I., Sekanina, L., Vojnar, T., Antos, D. (eds.) Proceedings of MEMICS 2011, LNCS 7119, pp. 191–204. Springer, New York (2011)
15.
16.
17.
Metadaten
Titel
Thoughtful brute-force attack of the RERS 2012 and 2013 Challenges
verfasst von
Jaco van de Pol
Theo C. Ruys
Steven te Brinke
Publikationsdatum
01.10.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 5/2014
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-014-0324-3

Weitere Artikel der Ausgabe 5/2014

International Journal on Software Tools for Technology Transfer 5/2014 Zur Ausgabe

Introduction

Rigorous examination of reactive systems

RERS

BDD-based software verification

RBT

A multiple case study on risk-based testing in industry

RBT

Dynamic test planning: a study in an industrial context

Rers

Analyzing program behavior through active automata learning

RERS

Tailored generation of concurrent benchmarks