An efficient software verification using multi-layered software verification tool
Keywords: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
 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.
 Schmidt RF, â€œSoftware engineering architecture-driven software developmentâ€, Amsterdam: Elsevier, (2013)
 Monteiro P, Machado RJ & Kazman R, â€œInception of software validation and verification practices within CMMI Level 2â€, Software Engineering Advances, (2009), pp.536-541.
 FilliÃ¢tre JC, â€œDeductive software verificationâ€, International Journal on Software Tools for Technology Transfer (STTT), Vol.13, (2011), pp.397-403.
 Knutson C & Carmichael S, â€œVerification and Validationâ€, Embedded Systems Programming, Vol. 25, (2001).
 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.
 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.
 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.
 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.
 Martignano M, â€œBounded model checking and abstract interpretation of large C codebasesâ€, Metrology for AeroSpace (MetroAeroSpace), (2017), pp.16-20.
 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.
 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.
 Eslamimehr M, Lesani M & Edwards G, â€œEfficient Detection and Validation of Atomicity Violations in Concurrent Programsâ€, Journal of Systems and Software, (2017).
 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.
 Mandrykin M & Khoroshilov A, â€œTowards deductive verification of concurrent Linux kernel code with Jessieâ€, Computer Science and Information Technologies (CSIT), (2015), pp.5-10.
 Zhang X, â€œDebugging Multithreaded Programs Using Symbolic Analysisâ€, Software Testing, Verification and Validation (ICST). (2017), pp.557-558.
 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.
 Uspenskiy S, â€œA survey and classification of software testing toolsâ€, Master of Science Thesis, Lappeenranta University of Technology, (2010).
 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.