An efficient software verification using multi-layered software verification tool

  • Abstract
  • Keywords
  • References
  • PDF
  • Abstract

    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



  • Keywords

    Verification, concurrency, contracts, swarm optimization.

  • References

      [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.




Article ID: 12465
DOI: 10.14419/ijet.v7i2.21.12465

Copyright © 2012-2015 Science Publishing Corporation Inc. All rights reserved.