Random testing of formal software models and induced coverage

ABSTRACT

This paper presents a methodology for random testing of software models. Random testing tools can be used very effectively early in the modeling process, e.g., while writing formal requirements specification for a given system. In this phase users cannot know whether a correct operational model is being built or whether the properties that the model must satisfy are correctly identified and stated. So it is very useful to have tools to quickly identify errors in the operational model or in the properties, and make appropriate corrections. Using Lurch, our random testing tool for finite-state models, we evaluated the effectiveness of random model testing by detecting manually seeded errors in an SCR specification of a real-world personnel access control system. Having detected over 80% of seeded errors quickly, our results appear to be very encouraging. We further defined and measured test coverage metrics with the goal of understanding why some of the mutants were not detected. Coverage measures allowed us to understand the pitfalls of random testing of formal models, thus providing opportunities for future improvement.

REFERENCES

• 1: Requirements Specification for Personnel Access Control System. National Security Agency, 2003.
• 2: Paul Anderson , Thomas Reps , Tim Teitelbaum, Design and Implementation of a Fine-Grained Software Inspection Tool, IEEE Transactions on Software Engineering, v.29 n.8, p.721-733, August 2003 [doi>10.1109/TSE.2003.1223646]
• 3: J. H. Andrews , L. C. Briand , Y. Labiche, Is mutation an appropriate tool for testing experiments?, Proceedings of the 27th international conference on Software engineering, p.402-411, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062530]
• 4: Sergio Antoy , Dick Hamlet, Automatically Checking an Implementation against Its Formal Specification, IEEE Transactions on Software Engineering, v.26 n.1, p.55-69, January 2000 [doi>10.1109/32.825766]
• 5: Myla Archer , Constance Heitmeyer , Elvinia Riccobene, Proving Invariants of I/O Automata with TAME, Automated Software Engineering, v.9 n.3, p.201-232, August 2002 [doi>10.1023/A:1016320523091]
• 6: Ramesh Bharadwaj , Steve Sims, Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.378-394, March 25-April 02, 2000
• 7: Alessandro Cimatti , Edmund M. Clarke , Enrico Giunchiglia , Fausto Giunchiglia , Marco Pistore , Marco Roveri , Roberto Sebastiani , Armando Tacchella, NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.359-364, July 27-31, 2002
• 8: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 9: J. Cobleigh, L. Clarke, and L. Osterweil. FLAVERS: a Finite-State Verification Technique for Software Systems. IBM Systems Journal, 41(1), 2002.
• 10: Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.146-162, September 06-10, 1999, Toulouse, France
• 11: Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005 [doi>10.1007/s10703-005-1489-x]
• 12: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 13: Alex Groce , Willem Visser, Heuristic Model Checking for Java Programs, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.242-245, April 11-13, 2002
• 14: R. Hamlet. Random Testing. In J. Maciniak, editor, Encyclopedia of Software Engineering. Wiley, 1994.
• 15: C. Heitmeyer, M. Archer, R. Bharadwaj, and R. Jeffords. Tools for Constructing Requirements Specifications: The SCR Toolset at the Age of Ten. International Journal of Computer Systems Science and Engineering, 20(1), 2005.
• 16: Constance L. Heitmeyer , Ralph D. Jeffords , Bruce G. Labaw, Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.3, p.231-261, July 1996 [doi>10.1145/234426.234431]
• 17: G. Holzmann. On-the-Fly, LTL Model Checking with SPIN. spinroot. com/spin/whatispin.html.
• 18: G. Holzmann. The SPIN Model Checker. Addison-Wesley, 2003.
• 19: Elizabeth I. Leonard , Constance L. Heitmeyer, Program Synthesis from Formal Requirements Specifications Using APTS, Higher-Order and Symbolic Computation, v.16 n.1-2, p.63-92, March-June 2003 [doi>10.1023/A:1023072104553]
• 20: K. McMillan. The SMV Model Checker. www-cad.eecs.berkeley.edu/~kenmcmil.
• 21: Rajeev Motwani , Prabhakar Raghavan, Randomized algorithms, Cambridge University Press, New York, NY, 1995
• 22: D. Owen and T. Menzies. Lurch: A Lightweight Alternative to Model Checking. In Proc. 15th International Conference on Software Engineering and Knowledge Engineering, 2003.
• 23: Debra J. Richardson , Stephanie Leif Aha , T. Owen O'Malley, Specification-based test oracles for reactive systems, Proceedings of the 14th international conference on Software engineering, p.105-118, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143100]
• 24: Steve Sims , Rance Cleaveland , Ken Butts , Scott Ranville, Automated Validation of Software Models, Proceedings of the 16th IEEE international conference on Automated software engineering, p.91, November 26-29, 2001
• 25: E. Weyuker , T. Goradia , A. Singh, Automatically Generating Test Data from a Boolean Specification, IEEE Transactions on Software Engineering, v.20 n.5, p.353-363, May 1994 [doi>10.1109/32.286420]
• 26: James A. Whittaker , J. H. Poore, Markov analysis of software specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.1, p.93-106, Jan. 1993 [doi>10.1145/151299.151326]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
      D.2.5 Testing and Debugging

General Terms:
Experimentation, Performance, Verification

Keywords:
formal methods, model testing, random testing