Top

International Journal on Software Tools for Technology Transfer

Published in:

01-10-2014 | RERS

Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges

Authors: Markus Schordan, Adrian Prantl

Published in: International Journal on Software Tools for Technology Transfer | Issue 5/2014

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We present a combination of approaches for the verification of event-condition-action (ECA) systems. The analyzed ECA systems range from structurally simple to structurally complex systems. We address the verification of reachability properties and behavioral properties. Reachability properties are represented by assertions in the program and we determine statically whether an assertion holds for all execution paths. Behavioral properties are represented as linear temporal logic formulas specifying the input/output behavior of the program. Our approach assumes a finite state space. We compare a symbolic analysis with an exhaustive state space exploration and discuss the trade-offs between the approaches in terms of the number of computed states and run-time behavior. All variants compute a state transition graph which can also be passed to an LTL verifier. The variants have a different impact on the number of computed states in the state transition graph which in turn impacts the run-time and memory consumption of subsequent phases. We evaluate the different analysis variants with the RERS benchmarks.

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

next article BDD-based software verification

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

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)CrossRef

Armando, Alessandro, Mantovani, Jacopo, Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transf. 11(1), 69–83 (2009)CrossRef

Bauer, Andreas, Leucker, Martin, Schallhart, Christian: Comparing LTL semantics for runtime verification. J. Logic Comput. 20(3), 651–674 (2010)CrossRefMATHMathSciNet

Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Proc. CAV, LNCS 4590, pp. 504–518. Springer, Berlin (2007)

Beyer, Dirk, Henzinger, Thomas A., Jhala, Ranjit, Majumdar, Rupak: The software model checker Blast: applications to software engineering. Int. J. Softw. Tools Technol. Transf. 9(5), 505–525 (2007)CrossRef

Beyer, D., Stahlbauer, A.: BDD-based software verification. Applications to event–condition–action systems. Softw. Tools Technol. Transf. doi:10.1007/s10009-014-0334-1 (2014)

Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. In: Fifth Annual IEEE Symposium on Logic in Computer Science, 1990. LICS ’90, Proceedings, pp. 428–439, Jun 1990

Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of Haskell programs. SIGPLAN Not. 35(9), 268–279 (2000)CrossRef

Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7–34 (2001)CrossRefMATH

10.

Clarke, E.M.: 25 years of model checking. In: The Birth of Model Checking, pp. 1–26. Springer, Berlin (2008)

11.

Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, ASE ’09, pp. 137–148. IEEE Computer Society, Washington, DC (2009)

12.

Duret-Lutz, A.: LTL translation improvements in spot. In: Proceedings of the Fifth International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS’11, pp. 72–83. British Computer Society, Swinton (2011)

13.

Alexandre, D.L.: LTL translation improvements in Spot 1.0. Int. J. Crit. Comput.-Based Syst. 5(1/2):31–54 (2014)

14.

Holzmann, Gerard J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRefMathSciNet

15.

Holzmann, G.J.: Parallelizing the spin model checker. In: Proceedings of the 19th International Conference on Model Checking Software, SPIN’12, pp. 155–171. Springer, Berlin (2012)

16.

Holzmann, G.J., Bosnacki, D.: Multi-core model checking with spin. In: Parallel and Distributed Processing Symposium, 2007. IPDPS 2007. IEEE International, pp. 1–8, March (2007)

17.

Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event–condition–action systems. In: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change—5th International Symposium, ISoLA 2012, LNCS 4590, pp. 608–614. Springer, Berlin (2007)

18.

Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous examination of reactive systems. In: The RERS Challenges 2012 and 2013. Software Tools for Technology Transfer. doi:10.1007/s10009-014-0337-y (2014)

19.

Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1–21:54 (2009)

20.

Lerda, F., Sinha, N., Theobald, M.: Symbolic model checking of software. Electron. Notes Theoret. Comput. Sci., 89(3), 480–498 (2003). SoftMC 2003, Workshop on Software Model Checking (Satellite Workshop of CAV ’03)

21.

McCarthy, D., Dayal, U.: The architecture of an active database management system. In: Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, SIGMOD ’89, pp. 215–224. ACM, New York (1989)

22.

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)

Title: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges
Authors: Markus Schordan
Adrian Prantl
Publication date: 01-10-2014
Publisher: Springer Berlin Heidelberg
Published in: International Journal on Software Tools for Technology Transfer / Issue 5/2014
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-014-0338-x

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 5/2014

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

Tailored generation of concurrent benchmarks

Analyzing program behavior through active automata learning

Dynamic test planning: a study in an industrial context

Rigorous examination of reactive systems

Approaches for the combined use of risk analysis and testing: a systematic literature review

Premium Partner