| Peer-Reviewed

The Examination of Shall Be Impossible Situations for Verification During Execution

Received: 18 February 2018     Accepted: 5 March 2018     Published: 23 March 2018
Views:       Downloads:
Abstract

Runtime verification is looking for violations of the properties of the system functioning. Finding and describing the system properties that indicate behavioural disorders is a complex and labour-intensive process that needs to be automated. This article describes how system properties can be determined automatically during the correct functioning. Inspection of the combinations of fulfilled properties makes it possible to detect more system problems. Three methods of handling property combinations are offered. The methods are based on the examination of the input sequences and output results. In order to increase the volume of the properties of the system under consideration, only the possible pairs of properties are analysed. Pairs are formed from the output properties, as well as from the input conditions and output properties, and the maximum possible number of property pairs is evaluated. The available property pairs are captured during the operation. Impossible combinations of properties that never occur during the execution highlight situations that are not possible during proper functioning. Capture of impossible property pairs during verification indicates system problems. During the experiment, five types of disorders and three detection methods were considered. Experimental results show that there is no single best method for detecting disorders. Therefore, it is appropriate at the same time to use several methods to detect disorders. The experiment shows how much of the disorders can detect the proposed approach.

Published in American Journal of Computer Science and Technology (Volume 1, Issue 2)
DOI 10.11648/j.ajcst.20180102.12
Page(s) 44-54
Creative Commons

This is an Open Access article, distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution and reproduction in any medium or format, provided the original work is properly cited.

Copyright

Copyright © The Author(s), 2018. Published by Science Publishing Group

Keywords

Runtime Verification, System Properties, Capturing of Properties, Inspection of Proper Functioning

References
[1] Colin, S., & Mariani, L. (2005). “18 Run-Time Verification”. In Model-Based Testing of Reactive Systems (pp. 525-555). Springer, Berlin, Heidelberg. doi.org/10.1007/11498490_24.
[2] Leucker, M., & Schallhart, C. (2009). “A brief account of runtime verification”. The Journal of Logic and Algebraic Programming, 78 (5), 293-303. doi.org/10.1016/j.jlap.2008.08.004.
[3] Colombo, C., Pace, G. J., & Schneider, G. (2008). “Dynamic event-based runtime monitoring of real-time and contextual properties”. In International Workshop on Formal Methods for Industrial Critical Systems (pp. 135-149). Springer, Berlin, Heidelberg. doi.org/10.1007/978-3-642-03240-0_13.
[4] Aktug, I., & Naliuka, K. (2008). “ConSpec—a formal language for policy specification”. Science of Computer Programming, 74=(1-2), 2-12. doi.org/10.1016/j.scico.2008.09.004.
[5] Pnueli, A. (1977). ‘The temporal logic of programs”. In Foundations of Computer Science, 1977., 18th Annual Symposium on Foundations of Computer Science (pp. 46-57). IEEE. doi.org/10.1109/sfcs.1977.32.
[6] Penczek, W., & Lomuscio, A. (2003). “Verifying epistemic properties of multi-agent systems via bounded model checking”. In Proceedings of the second international joint conference on Autonomous agents and multiagent systems (pp. 209-216). doi.org/10.1145/860575.860609.
[7] Bodden, E., Hendren, L., Lam, P., Lhoták, O., & Naeem, N. A. (2007). “Collaborative runtime verification with tracematches”. In International Workshop on Runtime Verification (pp. 22-37). Springer, Berlin, Heidelberg. doi.org/10.1007/978-3-540-77395-5_3.
[8] Reger, G., Hallé, S., & Falcone, Y. (2016). “Third International Competition on Runtime Verification“. Lecture Notes in Computer Science, 21–37. doi.org/10.1007/978-3-319-46982-9_3.
[9] Bartocci, E., Bortolussi, L., Nenzi, L., & Sanguinetti, G. (2015). “System design of stochastic models using robustness of temporal properties”. Theoretical Computer Science, 587, 3-25. doi.org/10.1016/j.tcs.2015.02.046.
[10] Colombo, C., Pace, G. J., Camilleri, L., Dimech, C., Farrugia, R., Grech, J. P.,... & Adami, K. Z. (2016). “Runtime verification for stream processing applications”. In International Symposium on Leveraging Applications of Formal Methods (pp. 400-406). Springer, Cham. doi.org/10.1007/978-3-319-47169-3_32
Cite This Article
  • APA Style

    Rimantas Seinauskas. (2018). The Examination of Shall Be Impossible Situations for Verification During Execution. American Journal of Computer Science and Technology, 1(2), 44-54. https://doi.org/10.11648/j.ajcst.20180102.12

    Copy | Download

    ACS Style

    Rimantas Seinauskas. The Examination of Shall Be Impossible Situations for Verification During Execution. Am. J. Comput. Sci. Technol. 2018, 1(2), 44-54. doi: 10.11648/j.ajcst.20180102.12

    Copy | Download

    AMA Style

    Rimantas Seinauskas. The Examination of Shall Be Impossible Situations for Verification During Execution. Am J Comput Sci Technol. 2018;1(2):44-54. doi: 10.11648/j.ajcst.20180102.12

    Copy | Download

  • @article{10.11648/j.ajcst.20180102.12,
      author = {Rimantas Seinauskas},
      title = {The Examination of Shall Be Impossible Situations for Verification During Execution},
      journal = {American Journal of Computer Science and Technology},
      volume = {1},
      number = {2},
      pages = {44-54},
      doi = {10.11648/j.ajcst.20180102.12},
      url = {https://doi.org/10.11648/j.ajcst.20180102.12},
      eprint = {https://article.sciencepublishinggroup.com/pdf/10.11648.j.ajcst.20180102.12},
      abstract = {Runtime verification is looking for violations of the properties of the system functioning. Finding and describing the system properties that indicate behavioural disorders is a complex and labour-intensive process that needs to be automated. This article describes how system properties can be determined automatically during the correct functioning. Inspection of the combinations of fulfilled properties makes it possible to detect more system problems. Three methods of handling property combinations are offered. The methods are based on the examination of the input sequences and output results. In order to increase the volume of the properties of the system under consideration, only the possible pairs of properties are analysed. Pairs are formed from the output properties, as well as from the input conditions and output properties, and the maximum possible number of property pairs is evaluated. The available property pairs are captured during the operation. Impossible combinations of properties that never occur during the execution highlight situations that are not possible during proper functioning. Capture of impossible property pairs during verification indicates system problems. During the experiment, five types of disorders and three detection methods were considered. Experimental results show that there is no single best method for detecting disorders. Therefore, it is appropriate at the same time to use several methods to detect disorders. The experiment shows how much of the disorders can detect the proposed approach.},
     year = {2018}
    }
    

    Copy | Download

  • TY  - JOUR
    T1  - The Examination of Shall Be Impossible Situations for Verification During Execution
    AU  - Rimantas Seinauskas
    Y1  - 2018/03/23
    PY  - 2018
    N1  - https://doi.org/10.11648/j.ajcst.20180102.12
    DO  - 10.11648/j.ajcst.20180102.12
    T2  - American Journal of Computer Science and Technology
    JF  - American Journal of Computer Science and Technology
    JO  - American Journal of Computer Science and Technology
    SP  - 44
    EP  - 54
    PB  - Science Publishing Group
    SN  - 2640-012X
    UR  - https://doi.org/10.11648/j.ajcst.20180102.12
    AB  - Runtime verification is looking for violations of the properties of the system functioning. Finding and describing the system properties that indicate behavioural disorders is a complex and labour-intensive process that needs to be automated. This article describes how system properties can be determined automatically during the correct functioning. Inspection of the combinations of fulfilled properties makes it possible to detect more system problems. Three methods of handling property combinations are offered. The methods are based on the examination of the input sequences and output results. In order to increase the volume of the properties of the system under consideration, only the possible pairs of properties are analysed. Pairs are formed from the output properties, as well as from the input conditions and output properties, and the maximum possible number of property pairs is evaluated. The available property pairs are captured during the operation. Impossible combinations of properties that never occur during the execution highlight situations that are not possible during proper functioning. Capture of impossible property pairs during verification indicates system problems. During the experiment, five types of disorders and three detection methods were considered. Experimental results show that there is no single best method for detecting disorders. Therefore, it is appropriate at the same time to use several methods to detect disorders. The experiment shows how much of the disorders can detect the proposed approach.
    VL  - 1
    IS  - 2
    ER  - 

    Copy | Download

Author Information
  • Software Department, Informatic Faculty, Kaunas University of Technology, Kaunas, Lithuania

  • Sections