Generating functional test cases in-the-large for time-critical systems from logic-based specifications

ABSTRACT

We address the problem of generating functional test cases for complex, highly structured time-critical systems starting from a modularized logic-based specification written in the TRIOR⁺ language, an object-oriented extension of the temporal logic TRIO.First, we present methods for producing test cases for a TRIO⁺ specification module, referring both to the internal, hidden, portion of the module and to its interface. Then, we discuss criteria to be used in the construction of test cases from a TRIO⁺ specification based on its composing modules and the connections among their interfaces. We formally define the notions related to test case derivation from TRIO⁺ modules and we introduce an executable language for describing a variety of strategies for constructing test cases for structured TRIO⁺ specifications starting from (parts of) the test cases of the composing modules. This language can be the basis for the implementation of an interactive tool for the semiautomatic construction of functional test cases from complex time-critical systems starting from their TRIO⁺ specification.

REFERENCES

• B&F93: R. W. Butler , G. B. Finelli, The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software, IEEE Transactions on Software Engineering, v.19 n.1, p.3-12, January 1993 [doi>10.1109/32.210303]
• BC&95: M,Basso, E.Ciapessoni, E. Crivelli, D. Mandrioli, A. Morzenti, E. Ratto, P. San Pietro, Experimenting a Logicbased Approach to the Specification and Design of the Control System of a Pondage Power Plant, in M. Wirsing (ed.), ICSE- 17 Workshop on Formal Methods Application in Software Engineering Practice, Seattle, April 1995.
• BCM90: J, Butch, E. Clarke, K.L. McMillan, D. Dill and H. Hwang, Symbolic model checking: 1020 states and beyond. In Proceedings of 5th Symposium on Logics in Computer Science, Philadelphia, June 1990, IEEE, pp. 428-439.
• CJ90: Cheng, K.T. and Jou, J.Y., Functional Test Case Generation for Finite State Machines. In Proceedings of IEEE Int. Testing Conference , I990, pp. 162-168.
• CSt90: Specification environments for real time systems based on a logic language, Technical annex to research contract 27/90, December I990, Case studies (in italian) on a regulator in a pondage power plant and on high-voltage substations.
• CSt92: Specification environments for real time systems based on a logic language, Technical annex to research contract 49/92, December 1992, Case studies (in Italian) on a programmable digital energy and power meters and on data collection and elaboration for dam security.
• D&Y94: Laura K. Dillon , Qing Yu, Oracles for checking temporal properties of concurrent systems, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.140-153, Dec. 1994
• Da85: Dasarathy, B., Timing Constraints of Real-Time Systems: Constructs for Expressing Them, Methods of Validating Them. IEEE Transaction on Software Engineering SE-11, I (January 1985), 80-86.
• DDH72: Ole Johan Dahl, Structured Programming, Academic Press, Inc., Orlando, FL, 1972
• DM&87: Richard A. DeMillo , W. Michael McCracken , R. J. Martin , John F. Passafiume, Software testing and evaluation, Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, 1987
• FB&91: Susumu Fujiwara , Gregor von Bochmann , Ferhat Khendek , Mokhtar Amalou , Abderrazak Ghedamsi, Test Selection Based on Finite State Models, IEEE Transactions on Software Engineering, v.17 n.6, p.591-603, June 1991 [doi>10.1109/32.87284]
• Ho87: William E Howden, Functional program testing and analysis, McGraw-Hill, Inc., New York, NY, 1986
• M&S94: Angelo Morzenti , Pierluigi San Pietro, Object-oriented logical specification of time-critical systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.1, p.56-98, Jan. 1994 [doi>10.1145/174634.174636]
• MD&88: Ma, H.K.T., Devadas, R., Newton, A., and Sangiovanni-Vincentelli, A., Test Generation for Sequential Circuits. IEEE Transactions on Computer-Aided Design 7(October 1988), 1081-1093.
• MMG92: Angelo Morzenti , Dino Mandrioli , Carlo Ghezzi, A model parametric real-time logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.4, p.521-573, Oct. 1992 [doi>10.1145/133233.129397]
• MMM92: Mandrioli, D., Morasca, S., and Morzenti, A. Functional test case generation for real-time systems. In Proceedings of DCCA3' 3rd International Working Conference on Dependable Computing for Critical Applications, IFIP, September t992. Springer Verlag, New York, pp. 13-26.
• MMM95: Dino Mandrioli , Sandro Morasca , Angelo Morzenti, Generating test cases for real-time systems from logic specifications, ACM Transactions on Computer Systems (TOCS), v.13 n.4, p.365-398, Nov. 1995 [doi>10.1145/210223.210226]
• Ric94: Debra J. Richardson, TAOS: Testing with Analysis and Oracle Support, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.138-153, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.187158]
• RLO92: 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]

INDEX TERMS

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

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

General Terms:
Design, Languages, Theory, Verification