Mutation-Based Test Case Generation for Simulink Models
https://www.researchgate.net/publication/221047548_Mutation-Based_Test_Case_Generation_for_Simulink_Models
1 Introduction
2 Simulink Models
3 Generating Test Cases using Mutations
4 Generating Test-Cases for Many Mutations
5 Detecting Non-Observability of Mutations
6 Conclusion
References
- Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
https://mitpress.mit.edu/9780262032704/model-checking/ - Gadkari, A., Yeolekar, A., Suresh, J., Ramesh, S., Mohalik, S., Shashidar, K.C.: AutoMOTGen: Automatic model oriented test generator for embedded control systems. In Gupta, A., Malik, S., eds.: Computer Aided Veri cation (CAV). Volume 5123/2008 of LNCS., Springer (2008) 204{208
https://qiita.com/kaizen_nagoya/items/0b1f1e6ccf0aace3b588 - Kroening, D., Clarke, E.M., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Design Automation Conference (DAC), ACM (2003) 368{371
- Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: FShell: Systematic test case generation for dynamic analysis and measurement. In: Computer Aided Veri cation(CAV). Volume 5123 of LNCS., Springer (2008) 209{213
- Angeletti, D., Giunchiglia, E., Narizzano, M., Puddu, A., Sabina, S.: Automatic test generation for coverage analysis using CBMC. In: Computer Aided Systems Theory (EUROCAST). Volume 5717 of LNCS., Springer (2009) 287{294
- Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: Query-driven program testing. In: Veri cation, Model Checking and Abstract Interpretation (VMCAI). Volume 5403 of LNCS., Springer (2009) 151{166
- Ball, T.: A theory of predicate-complete test coverage and generation. In: Formal Methods for Components and Objects (FMCO). Volume 3657 of LNCS., Springer (2005) 1{22
- Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: International Conference on Software Engineering (ICSE). (2004) 326{335
- Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Transactions on Software Engineering (TSE) (2010)
- Kupferman, O., Li, W., Seshia, S.A.: A theory of mutations with applications to vacuity, coverage, and fault tolerance. In: Formal Methods in Computer-Aided Design (FMCAD), IEEE (2008) 1{9
- Ruthru , J.R., Burnett, M.M., Rothermel, G.: Interactive fault localization techniques in a spreadsheet environment. IEEE Transactions on Software Engineering (TSE) 32 (2006) 213{239
- Schuler, D., Dallmeier, V., Zeller, A.: E cient mutation testing by checking invariant violations. In: International Symposium on Software Testing and Analysis (ISSTA), ACM (2009) 69{80
- Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Formal Engineering (ICFEM). Volume 4260 of LNCS., Springer (2006) 606{620
- Fehnker, A., Krogh, B.H.: Hybrid system veri cation is not a sinecure: The electronic throttle control case study. In: Automated Technology for Veri cation and Analysis (ATVA). Volume 3299 of LNCS., Springer (2004) 263{277
- Joshi, A., Heimdahl, M.P.E.: Model-based safety analysis of Simulink models using SCADE design veri er. In: Computer Safety, Reliability, and Security (SAFECOMP). Volume 3688 of LNCS., Springer (2005) 122{135
- Ryabtsev, M., Strichman, O.: Translation validation: From simulink to c. In: Computer Aided Veri cation (CAV). Volume 5643 of LNCS., Springer (2009) 696{701
- The Mathworks: Simulink design veri er user's guide. http://www.mathworks.com/access/helpdesk/help/toolbox/sldv/ (2009) version 1.5.
- Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for oating-point arithmetic. In: Formal Methods in Computer-Aided Design (FMCAD), IEEE (2009)
69{76 - Kuehlmann, A., van Eijk, C.A.J.: Combinational and sequential equivalence checking. In: Logic Synthesis and Veri cation. Kluwer International Series in Engineering and Computer Science Series. Kluwer, Norwell, MA, USA (2002) 343{372
- Graf, S., Sa di, H.: Construction of abstract state graphs with PVS. In: Computer Aided Veri cation (CAV). Volume 1254 of LNCS. Springer (1997) 72{83
- Kroening, D., Clarke, E.: Checking consistency of C and Verilog using predicate abstraction and induction. In: IEEE/ACM International conference on Computeraided design, IEEE (2004) 66{72
- Victor A., C.: Interpretation of IEEE-854 oating-point standard and de nition in the HOL system. Technical report, NASA Langley (1995)
- Harrison, J.: Formal veri cation of square root algorithms. Formal Methods in System Design (FMSD) 22 (2003) 143{153
- Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min e, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation (PLDI), ACM (2003) 196{207
- Min, A.: Relational abstract domains for the detection of oating-point run-time errors. In: European Symposium on Programming (ESOP). Volume 2986 of LNCS., Springer (2004) 3{17
- Kroening, D., Strichman, O.: Decision Procedures. Springer (2008)
- E en, N., Sorensson, N.: An extensible SAT-solver. In: Theory and Applications of Satis ability Testing (SAT). Volume 2919 of LNCS., Springer (2004) 502{518
- Sheeran, M., Singh, S., St almarck, G.: Checking safety properties using induction and a SAT-solver. In: Formal Methods in Computer-Aided Design (FMCAD). Volume 1954 of LNCS., Springer (2000) 108{125
- Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 35 (1986) 677{691
- McMillan, K.L.: Interpolation and SAT-based model checking. In: Computer Aided Veri cation (CAV). Volume 2725 of LNCS., Springer (2003) 1{13
- Chockler, H., Kroening, D., Purandare, M.: Coverage in interpolation-based model checking. In: Design Automation Conference (DAC), ACM (2010) View publication