Skip to main content

Optimization of Component-Based Systems Run Time Verification

  • Conference paper
  • First Online:
Modelling and Implementation of Complex Systems (MISC 2018)

Part of the book series: Lecture Notes in Networks and Systems ((LNNS,volume 64))

Abstract

As technology evolves, software systems become more and more voluminous and complex. Being currently unable to produce programs free of errors, and in order to ensure that program behaviors comply with their specifications, formal verification of their essential properties is paramount. To this end, model-checking verification approach has been widely used and continues to be. However, if these properties have been verified on a system model, would they still true during any real system execution? So, modeled behavior of a system would be exactly the same in real executions when interacting with its environment? That is why verification during current system execution is essential stage even as a complementary way to other verification approaches. In this paper, we are concerned by runtime verification optimization of component-based systems in Behavior Interactions Priority (BIP) framework in order to significantly reduce time overhead. Our contribution in this paper is to consider only component states involved in the property being verified. The required states imply their associated components to be activated and those useless are disabled. Also, when a steady state is reached during monitoring process, the monitor is stopped which reduces system consumption resources. Our experiment results showed that a non negligible amount of space-time overhead was avoided.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the bip framework. IEEE Softw. 28, 41–48 (2011)

    Article  Google Scholar 

  2. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebr. Programm. 78, 293–303 (2009)

    Article  MATH  Google Scholar 

  3. Falcone, Y., Jaber, M., Nguyen, T.H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems in the bip framework with formally-proved sound and complete instrumentation. Softw. Syst. Model. 14, 173–199 (2015)

    Article  Google Scholar 

  4. Zhou, G., Dong, W., Liu, W., Shi, H., Hu, C., Yin, L.: Optimizing monitor code based on patterns in runtime verification. In: 2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C), pp. 348–354. IEEE (2017)

    Google Scholar 

  5. Bonakdarpour, B., Navabpour, S., Fischmeister, S.: Sampling-based runtime verification. In: International Symposium on Formal Methods, pp. 88–102. Springer (2011)

    Google Scholar 

  6. Huang, X., Seyster, J., Callanan, S., Dixit, K., Grosu, R., Smolka, S.A., Stoller, S.D., Zadok, E.: Software monitoring with controllable overhead. Int. J. Softw. Tools Technol. Transf. 14, 327–347 (2012)

    Article  Google Scholar 

  7. Nazarpour, H., Falcone, Y., Bensalem, S., Bozga, M., Combaz, J.: Monitoring multi-threaded component-based systems. Technical Report TR-2015-5, Verimag Research Report (2015)

    Google Scholar 

  8. Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Logic Comput. 20, 651–674 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  9. Falcone, Y., Fernandez, J.C., Mounier, L.: What Can You Verify and Enforce at Runtime?, vol. 14, pp. 349–382. Springer, Berlin (2012)

    Google Scholar 

  10. Bauer, A., Leucker, M., Schallhart, C.: The Good, the Bad, and the Ugly, But How Ugly is Ugly?, pp. 126–138. Springer, Berlin (2007)

    Google Scholar 

  11. Falcone, Y., Fernandez, J.C., Mounier, L.: Runtime verification of safety-progress properties. International Workshop on Runtime Verification, pp. 40–59. Springer, Berlin (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Makhlouf Aliouat .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Aliouat, L., Aliouat, M. (2019). Optimization of Component-Based Systems Run Time Verification. In: Chikhi, S., Amine, A., Chaoui, A., Saidouni, D.E. (eds) Modelling and Implementation of Complex Systems. MISC 2018. Lecture Notes in Networks and Systems, vol 64. Springer, Cham. https://doi.org/10.1007/978-3-030-05481-6_21

Download citation

Publish with us

Policies and ethics