An efficient software verification using multi-layered software verification tool

  • Authors

    • S V. Gayetri Devi
    • C Nalini
    • N Kumar
    2018-04-20
    https://doi.org/10.14419/ijet.v7i2.21.12465
  • Verification, concurrency, contracts, swarm optimization.

  • Rapid advancements in Software Verification and Validation have been critical in the wide development of tools and techniques to identify potential Concurrent bugs and hence verify the software correctness. A concurrent program has multiple processes and shared objects. Each process is a sequential program and they use the shared objects for communication for completion of a task. The primary objective of this survey is retrospective review of different tools and methods used for the verification of real-time concurrent software. This paper describes the proposed tool ‘F-JAVA’ for multithreaded Java codebases in contrast with existing ‘FRAMA-C’ platform, which is dedicated to real-time concurrent C software analysis. The proposed system is comprised of three layers, namely Programming rules generation stage, Verification stage with Particle Swarm Optimization (PSO) algorithm, and Performance measurement stage. It aims to address some of the challenges in the verification process such as larger programs, long execution times, and false alarms or bugs, and platform independent code verification

     

     

  • References

    1. [1] Philippaerts P, Mühlberg JT, Penninckx W, Smans J, Jacobs B & Piessens F, “Software verification with VeriFast: Industrial case studiesâ€, Science of Computer Programming, Vol. 82, (2014), pp.77-97.

      [2] Schmidt RF, “Software engineering architecture-driven software developmentâ€, Amsterdam: Elsevier, (2013)

      [3] Monteiro P, Machado RJ & Kazman R, “Inception of software validation and verification practices within CMMI Level 2â€, Software Engineering Advances, (2009), pp.536-541.

      [4] Filliâtre JC, “Deductive software verificationâ€, International Journal on Software Tools for Technology Transfer (STTT), Vol.13, (2011), pp.397-403.

      [5] Knutson C & Carmichael S, “Verification and Validationâ€, Embedded Systems Programming, Vol. 25, (2001).

      [6] Gabmeyer S, Kaufmann P, Seidl M, Gogolla M & Kappel G, “A feature-based classification of formal verification techniques for software modelsâ€, Software & Systems Modeling, (2017), pp.1-26.

      [7] Dias RJ, Ferreira C, Fiedor J, Lourenço JM, Smrcka A, Sousa DG & Vojnar T, “Verifying Concurrent Programs Using Contractsâ€, Software Testing, Verification and Validation (ICST), (2017), pp.196-206.

      [8] Blanchard A, Kosmatov N, Lemerre M & Loulergue F, “Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programsâ€, Source Code Analysis and Manipulation (SCAM), (2016), 767-772.

      [9] Nguyen TL, Schrammel P, Fischer B, La Torre S & Parlato G, ‘Parallel bug-finding in concurrent programs via reduced interleaving instancesâ€, Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, (2017), pp.753-764.

      [10] Martignano M, “Bounded model checking and abstract interpretation of large C codebasesâ€, Metrology for AeroSpace (MetroAeroSpace), (2017), pp.16-20.

      [11] Tomasco E, Nguyen TL, Inverso O, Fischer B, La Torre S & Parlato G, “Lazy sequentialization for TSO and PSO via shared memory abstractionsâ€, Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design. FMCAD Inc, (2016), pp.193-200.

      [12] Blom S, Darabi S, Huisman M & Oortwijn W, “The VerCors tool set: verification of parallel and concurrent softwareâ€, International Conference on Integrated Formal Methods, (2017), pp.102-110.

      [13] Eslamimehr M, Lesani M & Edwards G, “Efficient Detection and Validation of Atomicity Violations in Concurrent Programsâ€, Journal of Systems and Software, (2017).

      [14] e Silva RAB, Arai NN, Burgareli LA, de Oliveira JMP & Pinto JS, “Formal verification with frama-C: A case study in the space software domainâ€, IEEE Transactions on Reliability, Vol.65, No.3, (2016), pp.1163-1179.

      [15] Mandrykin M & Khoroshilov A, “Towards deductive verification of concurrent Linux kernel code with Jessieâ€, Computer Science and Information Technologies (CSIT), (2015), pp.5-10.

      [16] Zhang X, “Debugging Multithreaded Programs Using Symbolic Analysisâ€, Software Testing, Verification and Validation (ICST). (2017), pp.557-558.

      [17] Shi Q, Huang J, Chen Z & Xu B, “Verifying Synchronization for Atomicity Violation Fixingâ€, IEEE Transactions on Software Engineering, Vol.42, No.3, (2016), pp.280-296.

      [18] Uspenskiy S, “A survey and classification of software testing toolsâ€, Master of Science Thesis, Lappeenranta University of Technology, (2010).

      [19] Boogerd C & Moonen L, “Prioritizing software inspection results using static profilingâ€, Source Code Analysis and Manipulation, (2006), pp.149-160.

      Etenting Hub-Online Free Software Testing Tutorial. (n.d.), Software Testing Verification, 2018.

  • Downloads

  • How to Cite

    V. Gayetri Devi, S., Nalini, C., & Kumar, N. (2018). An efficient software verification using multi-layered software verification tool. International Journal of Engineering & Technology, 7(2.21), 454-457. https://doi.org/10.14419/ijet.v7i2.21.12465