LoginSignup
0
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

科学・理論 Qiita Tech Festa 2025
Qiita Tech Festa20252025年7月15日まで開催中！
@kaizen_nagoya(Dr. Kiyoshi Ogawa)

AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems

Posted at

AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems
https://link.springer.com/chapter/10.1007/978-3-540-70545-1_19

References

  1. Ammann, P., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: ICFEM, p. 46 (1998)
  2. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
  3. Gadkari, A., Mohalik, S.K., Shashidhar, K.C., Yeolekar, A., Suresh, J., Ramesh, S.: Automatic generation of test-cases using model checking for SL/SF models. In: 4th International Workshop on Model Driven Engineering, Verification and Validation (MoDeVVa 2007) (2007) 208 A.A. Gadkari et al.
  4. Gargantini, A., Heitmeyer, C.L.: Using model checking to generate tests from requirements specifications. In: ESEC / SIGSOFT FSE, pp. 146–162 (1999)
  5. Hamon, G., deMoura, L., Rushby, J.: Generating efficient test sets with a model checker. In: 2nd International Conference on Software Engineering and Formal Methods, Beijing, China, September 2004, pp. 261–270. IEEE Computer Society, Los Alamitos (2004)
  6. The Mathworks, Inc., http://www.mathworks.com
  7. Reactis, Reactive Systems, Inc., http://www.reactive-systems.com
  8. SAL homepage, http://sal.csl.sri.com/
  9. Safety Test Builder, TNI-Software, http://www.tni-software.com

1. Ammann, P., Black, P.E., Majurski, W.:

Using model checking to generate tests from specifications. In: ICFEM, p. 46 (1998)
https://dl.acm.org/doi/10.1145/318774.318939

References

[1] P. Ammann, P. Black, and W. Majurski. Using model checking to generate tests from specifications. In Proc. 2nd IEEE Intern. Conf. on Formal Engineering Methods (ICFEM'98), Brisbane, Australia, December 1998.
[2] B. Beizer. Software Testing Techniques. Van Nostrand Reinhold, 1983.
[3] R. Bharadwaj and C. Heitmeyer. Model checking complete requirements specifications using abstraction. Automated Software Eng. J., 6(l), January 1999.
[4] M. R. Blackburn, R. D. Busser, and J. S. Fontaine. Automatic generation of test vectors for SCR-style specifications. In Proc. 12th Annual Conf. on Computer Assurance (COMPASS '97), Gaithersburg, MD, June 1997.
[5] J. Callahan, F. Schneider, and S. Easterbrook. Specification-based testing using model checking. In Proc. SPIN Workshop, Rutgers University, August 1996. Tech. Report NASA-IVV-96-022.
[6] P.-J. Courtois and David L. Parnas. Documentation for safety critical software. In Proc. 15th Id? Conf. on Softw. Eng. (ICSE '93), Baltimore, MD, 1993.
[7] S. Easterbrook and J. Callahan. Formal methods for verification and validation of partial specifications: A case study. Journal of Systems and Software, 1997.
[8] A. Engels, L.M.G. Feijs, and S. Mauw. Test generation for intelligent networks using model checking. In Proc. TACAS'97, pages 384-398. Springer, 1997. in E. Brinksma, editor, LNCS 1217.
[9] S. R. Faulk, L. Finneran, J. Kirby, Jr., S. Shah, and J. Sutton. Experience applying the CORE method to the Lockheed C-13OJ. In Proc. 9th Annual Conf. on Computer Assurance (COMPASS '94), Gaithersburg, MD, June 1994.
[10] .S. Fujiwara, G. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi. Test selection based on finite state models. IEEE Dans. on Softw. Eng., 17(6), June 1991.
[11] K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Proc. Formal Methods Europe (FME'96), pages 662- 681. Springer-Verlag, March 1996. LNCS 1051.
[12] C. Heitmeyer, J. Kirby, B. Labaw, M. Archer, and R. Bharadwaj. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE ZYans. on Sofew. Eng., 24(11), November 1998.
[13] C. Heitmeyer, J. Kirby, Jr., and B. Labaw. Tools for formal specification, verification, and validation of requirements. In Proc. 12th Annual Conf. on Computer Assurance (COMPASS '97), Gaithersburg, MD, June 1997.
[14] C. L. Heitmeyer, R. D. Jeffords, and B. G. Labaw. Automated consistency checking of requirements specifications. ACM Trans. on Software Eng. and Methodology, 5(3):231-261, April-June 1996.
[15] K. Heninger, D. Parnas, J. Shore, and J. Kallander. Software requirements for the A-7E aircraft. Technical Report 3876, Naval Research Lab., Wash., DC, 1978.
[16] G. J. Holzmann. The model checker SPIN. IEEE IFans. on Software Engineering, 23(5):279-295, May 1997.
[17] W. E. Howden. A functional approach to program testing and analysis. IEEE nans. on Softw. Eng., 15:997-1005, October 1986.
[18] R. Jeffords and C. Heitmeyer. Automatic generation of state invariants from requirements specifications. In Proc. Sixth ACM SIGSOFT Symp. on Foundations of Software Engineering, November 1998.
[19] D. Mandrioli, S. Morasca, and A. Morzenti. Generating test cases for real-time systems from logic specifications. ACM Bans. on Computer Systems, 13(4):365- 398, 1995.
[20] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Englewood Cliffs, NJ, 1993.
[21] S. P. Miller. Specifying the mode logic of a flight guidance system in CORE and SCR. In Proc. 2nd ACM Workshop on Formal Methods in Software Practice (FMSP '98), 1998.
[22] D. J. Richardson, S. L. Aha, and T. O'Malley. Specification-based test oracles for reactive systems. In Proc. 14th Intern. Conf. on Software Eng., pages 105-118. Springer, May 1992.
[23] P. Stocks and D. Carrington. A framework for specification-based testing. IEEE Z+ans. on Softw. Eng., 22(11):777-793, November 1996.
[24] E. Weyuker, T. Goradia, and A. Singh. Automatically generating test data from a boolean specification. IEEE Trans. on Softw. Eng., 201353-363, May 1994.

2. Clarke, E.M., Grumberg, O., Peled, D.A.:

Model Checking. The MIT Press, Cambridge (2000)
https://www.researchgate.net/publication/220689159_Model_Checking

References

  1. R. Alur, K. McMillan, D. Peled, Deciding global partial order properties, ICALP 1998, Aalborg, Denmark, Lecture Notes in computer science 1443, 41-52.
  2. A. Biere, A. Cimatti, E. M. Clarke, Y. Zhu, TACAS 1999, Amsterdam, The Netherlands, Lecture Notes in Computer Science 1579, Springer, 193-207.
  3. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Huang, Symbolic model checking: 1020 states and beyond, LICS 1990, Philadelphia, PA, USA. 428-439.
  4. E. M. Clarke, E. A. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic, Logic of programs, 1981, Lecture Notes in Temporal Logic 131, Springer, Yorktown Heights, NY, USA, 52-71.
  5. C, Courcoubetis, M. Y. Vardi, P. Wolper, M. Yannakakis, Memory efficient algorithms for the verification of temporal properties, CAV 1990, New Brunswick, NJ, USA, Lecture Notes in Computer Science 531, Springer, 233-242.
  6. E. A. Emerson, C.-L. Lei, Modalities for model checking: branching time logic strikes back. Science of Computer Programming 8(3), 1987, 275-306.
  7. E. A. Emerson, E. M. Clarke, Characterizing correctness properties of prallel programs using fixpoints, ICALP 1980, Noorweijkerhout, The Netherlands, Lecture Notes in Computer Science 85, Springer, 169-181.
  8. R. Gerth, D. Peled, M. Y. Vardi, P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, PSTV 1995, Warsaw, Poland, 3-18.
  9. G. J. Holzmann, D. Peled, M. Yannakakis, On nested depth first search, 2nd workshop on the SPIN verification system 1996, Dimacs series in discrete mathematics, volume 32, 1997, 23-32.
  10. L. Lamport, What good is temporal logic, Information processing 83, IFIP 9th world congress, Paris, France, 657-668.
  11. O. Lichtenstein, A. Pnutli, Checking that finite state concurrent programs satisfy their linear specification, POPL 1985, New Orleans, LO, USA, 97-107.
  12. D. Peled, M. Y. Vardi, M. Yannakakis, Black box checking, FORTE 1999, Beijing, China, 225-240.
  13. D. Peled, T. Wilke, Stutter-invariant temporal properties are expressive without the next-time operator, Information Processing Letters 63(5), 1997, 243-246.
  14. A. Pnueli, The temporal logic of programs, FOCS 1977, Providence, RI, USA, 46-57.
  15. J.-P. Quille, J. Sifakis, Specification and verification of concurrent systems in CESAR, Symposium on Programming 1982, Torino, Italy, Lecture Notes in Computer Science 137, Springer, 337-351.
  16. A. P. Sistla, E. M. Clarke, The complexity of propositional linear temporal logic, STOC 1982, San Francisco, CA, USA, 159-168.
  17. R. E. Tarjan, Depth-first search and linear graph algorithms, FOCS 1971, East lansing, MI, USA, 114-121.
  18. W. Thomas, Automata on infinite objects, Handbook on theoretical computer science, 1991, Volume B, 133-191.
  19. M. Vardi, P. Wolper, Automata theoretic techniques for modal logic of programs, STOC 1984, Washington, DC, USA, 446-456.
  20. I. Walukiewicz, Difficult configurations - on the complexity of LTrL, Lecture Notes in Computer Science 1443, ICALP 1998, 140-151.
  21. P. Wolper, Temporal logic can be more expressive, FOCS 1981, Nashville, TN, USA, 340-348.

3. Gadkari, A., Mohalik, S.K., Shashidhar, K.C., Yeolekar, A., Suresh, J., Ramesh, S.:

Automatic generation of test-cases using model checking for SL/SF models. In: 4th International Workshop on Model Driven Engineering, Verification and Validation (MoDeVVa 2007) (2007) 208 A.A. Gadkari et al.

4. Gargantini, A., Heitmeyer, C.L.:

Using model checking to generate tests from requirements specifications. In: ESEC / SIGSOFT FSE, pp. 146–162 (1999)

5. Hamon, G., deMoura, L., Rushby, J.:

Generating efficient test sets with a model checker. In: 2nd International Conference on Software Engineering and Formal Methods, Beijing, China, September 2004, pp. 261–270. IEEE Computer Society, Los Alamitos (2004)

cont.

  1. The Mathworks, Inc., http://www.mathworks.com
  2. Reactis, Reactive Systems, Inc., http://www.reactive-systems.com
  3. SAL homepage, http://sal.csl.sri.com/
  4. Safety Test Builder, TNI-Software, http://www.tni-software.com
0
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
0
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?