This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Generation of Execution Sequences for Modular Time Critical Systems
February 2000 (vol. 26 no. 2)
pp. 128-149
ASCII Text
x 
 
Pierluigi San Pietro, Angelo Morzenti, Sandro Morasca, "Generation of Execution Sequences for Modular Time Critical Systems," IEEE Transactions on Software Engineering, vol. 26, no. 2, pp. 128-149, February, 2000.
 
 
BibTex
x
 
@article{ 10.1109/32.841114,
author = {Pierluigi San Pietro and Angelo Morzenti and Sandro Morasca},
title = {Generation of Execution Sequences for Modular Time Critical Systems},
journal ={IEEE Transactions on Software Engineering},
volume = {26},
number = {2},
issn = {0098-5589},
year = {2000},
pages = {128-149},
doi = {http://doi.ieeecomputersociety.org/10.1109/32.841114},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Generation of Execution Sequences for Modular Time Critical Systems
IS - 2
SN - 0098-5589
SP128
EP149
EPD - 128-149
A1 - Pierluigi San Pietro,
A1 - Angelo Morzenti,
A1 - Sandro Morasca,
PY - 2000
KW - Functional testing
KW - structural testing
KW - specification testing
KW - formal specifications
KW - time critical systems
KW - modular notations.
VL - 26
JA - IEEE Transactions on Software Engineering
ER -
 

Abstract—We define methods for generating execution sequences for time-critical systems based on their modularized formal specification. An execution sequence represents a behavior of a time critical system and can be used, before the final system is built, to validate the system specification against the user requirements (specification validation) and, after the final system is built, to verify whether the implementation satisfies the specification (functional testing). Our techniques generate execution sequences in the large, in that we focus on the connections among the abstract interfaces of the modules composing a modular specification. Execution sequences in the large are obtained by composing execution sequences in the small for the individual modules. We abstract from the specification languages used for the individual modules of the system, so our techniques can also be used when the modules composing the system are specified with different formalisms. We consider the cases in which connections give rise to either circular or noncircular dependencies among specification modules. We show that execution sequence generation can be carried out successfully under rather broad conditions and we define procedures for efficient construction of execution sequences. These procedures can be taken as the basis for the implementation of (semi)automated tools that provide substantial support to the activity of specification validation and functional testing for industrially-sized time critical systems. In addition, we show how we have applied our techniques to an industrial-strength case study with the aid of a prototype tool.

[1] R.W. Butler and G.B. Finelli,“The infeasibility of quantifying the reliability of life-critical real-timesoftware,” IEEE Trans. Software Engineering, vol. 19, no. 1, pp. 3-12, 1993.
[2] R. Braeck and O. Haugen, Engineering Real-Time Systems: An Object-Oriented Methodology Using SDL. New York, London: Prentice Hall, 1993.
[3] M. Basso, E. Ciapessoni, E. Crivelli, D. Mandrioli, A. Morzenti, E. Ratto, and P. San Pietro, “Experimenting a Logic-Based Approach to the Specification and Design of the Control System of a Pondage Power Plant,” Proc. Workshop Industrial Application of Formal Methods, Apr. 1995.
[4] K.T. Cheng and J.Y. Jou, “Functional Test Case Generation for Finite State Machines,” Proc. IEEE Int'l Testing Conf., pp. 162-168, 1990.
[5] A. Coen-Porisini, R. Kemmerer, and D. Mandrioli, “A Formal Framework for ASTRAL Intra Level Proof Obligations,” IEEE Trans. Software Eng., vol. 20, no. 8, pp. 548-561, Aug. 1994.
[6] A. Coen-Porisini, “An Environment Supporting the Execution of TRIO Formal Specifications,” Technical Report 96.129, Dipartimento di Elettronica e Informazione, Politecnico di Milano, 1996.
[7] J. Chang, D.J. Richardson, and S. Sankar, “Structural Specification-Based Testing with ADL,” Proc. Int'l Symp. Software Testing and Analysis, Jan. 1996.
[8] E.H.H. Dürr and J. van Katwiik, “VDM++: A Formal Specification Language for Object-Oriented Designs,” Proc. Int'l Conf. Technology of Object-Oriented Languages and Systems, TOOLS 7, G. Heeg, B. Mugnusson, and B. Meyer, eds., pp. 63-78, 1992.
[9] L.K. Dillon and Q. Yu, “Oracles for Checking Temporal Properties of Concurrent Systems,” Proc. Symp. Foundations of Software Eng., pp. 140–153, Dec. 1994.
[10] B. Dasarathy, “Timing Constraints of Real-Time Systems: Constructs for Expressing Them, Methods of Validating Them,” IEEE Trans. Software Eng., vol 11, no. 1, pp. 80-86, Jan. 1985.
[11] O.J. Dahl, E.W. Dijkstra, and C.A.R. Hoare, Structured Programming. New York: Academic Press, 1972.
[12] R.A. DeMillo, M.W. McCracken, R.J. Martin, and J.F. Passafiume, Software Testing and Evaluation. Menlo Park, Calif.: Benjamin Cummings, 1987.
[13] P. Eades, X. Lin, and W.F. Smyth, “A Fast and Effective Heuristic for the Feedback Arc Set Problem,” Information Processing Letters, vol. 47, pp. 319-323, 1993.
[14] M. Felder and A. Morzenti, “Validating Real-Time Systems by History-Checking TRIO Specifications,” ACM Trans. Software Eng. and Methodologies, vol. 3, no. 4, Oct. 1994.
[15] S. Fujiwara, V.G. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi, “Test Selection Based on Finite State Machine Model,” IEEE Trans. Software Eng., vol. 17, no. 6, pp. 591-603, June 1991.
[16] M.M. Flood, “Exact and Heuristic Algorithms for the Weighted Feedback Arc Set Problem: A Special Case of the Skew-Symmetric Quadratic Assignment Problem,” NETWORKS, vol. 20, pp. 1-23, 1990.
[17] M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness.New York: W.H. Freeman, 1979.
[18] A. Gargantini, L. Liberati, A. Morzenti, and C. Zacchetti, “Specifying, Validating, and Testing a Traffic Management System in the TRIO Environment,” Proc. COMPASS, 11th Ann. Conf. Computer Assurance, June 1996.
[19] R. Hassin and S. Rubinstein, “Approximations for the Maximum Acyclic Subgraph Problem,” Information Processing Letters, vol. 51, pp. 133-140, 1994.
[20] W.E. Howden, Functional Program Testing Analysis. McGraw-Hill, 1987.
[21] R.A. Kemmerer, “Testing Formal Specifications to Detect Design Errors,” IEEE Trans. Software Eng., vol. 11, no. 1, pp. 32-43, Jan. 1985.
[22] L. Lamport and S. Owicki, "The Temporal Logic of Actions," ACM Trans. Programming Languages and Systems, vol. 16, pp. 872-923, May 994.
[23] K. Lano, “Z++, an Object-Oriented Extension to Z,” Proc. Fourth Ann. Z User Meeting, Workshop in Computing, J.E. Nicholls, ed., pp.151-172, 1991.
[24] G. Luo, G.V. Bochman, and A. Petrenko, “Test Selection Based on Communicating Nodetermistic Finite State Machines Using a Generalized wp-Method,” IEEE Trans. Software Eng., vol. 20, no. 2, pp. 149-162, Feb. 1994.
[25] A. Morzenti and P. San Pietro, “Object-Oriented Logic Specifications of Time Critical Systems,” ACM Trans. Software Eng. and Methodology, vol. 3, no. 1, pp. 56-98, Jan. 1994.
[26] H.K.T. Ma, R. Devadas, A. Newton, and A. Sangiovanni-Vincentelli, “Test Generation for Sequential Circuits,” IEEE Trans. Computer-Aided Design, vol. 7, pp. 1,081-1,093, Oct. 1988.
[27] A. Morzenti, D. Mandrioli, and C. Ghezzi, “A Model-Parametric Real-Time Logic,” ACM Trans. Programming Languages and Systems, vol. 14, no. 4, pp. 521-573, Oct. 1992.
[28] D. Mandrioli, S. Morasca, and A. Morzenti, “Generating Test Cases for Real-Time Systems from Logic Specifications,” ACM Trans. Computer Systems, vol. 13, no. 4, pp. 365-398, Nov. 1995.
[29] K. Mehlhorn and S.T. Näher, “Algorithm Design and Software Libraries: Recent Developments in the Leda Project,” Algorithms, Software, Architectures, Information Processing 92, vol. 1, 1992.
[30] A. Morzenti, P. San Pietro, and S. Morasca, “A Tool for Automated System Analysis Based on Modular Specifications,” Internal Report 98-071, Politecnico di Milano, Dipartimento di Elettronica e Informazione, 1998
[31] P. Pulli, M. Heikkinen, and R. Lintulampi, “Graphical Animation as a Form of Prototyping Real-Time Systems,” Incremental Prototyping Technology for Embedded Real-Time Systems, vol. 5,nos. 2/3, pp. 173-195, 1993.
[32] A. Petrenko, N. Yevtushenko, G.V. Bochmann, and R. Dssouli, “Testing in Context: Framework and Test Derivation,” Report No. 1,011, Département d'Informatique et de Recherche Opérationnelle, Universitéde Montréal, 1996.
[33] D.J. Richardson, “TAOS: Testing with Analysis and Oracle Support,” Proc. Int'l. Symp. Software Testing and Analysis, 1994.
[34] D.J. Richardson, S.L. Aha, and T.O. O'Malley, “Specification-Based Test Oracles for Reactive Systems,” Proc. Int'l Conf. Software Eng. (ICSE), pp. 105–118, May 1992.
[35] B. Selic, “An Efficient Object-Oriented Variation of Statecharts Formalism for Distributed Real-Time Systems,” Proc. IFIP Conf. Hardware Description Languages and Their Applications (CHDL '93), Apr. 1993.
[36] W.T. Tutte, “Graph Theory,” Encyclopedia of Math., vol. 21,Reading, Mass.: Addison Wesley, 1984.
[37] M.Y. Vardi and O. Kupferman, “Module Checking,” Proc. Conf. Computer Aided Verification (CAV '96), 1996.

Index Terms:
Functional testing, structural testing, specification testing, formal specifications, time critical systems, modular notations.
Citation:
Pierluigi San Pietro, Angelo Morzenti, Sandro Morasca, "Generation of Execution Sequences for Modular Time Critical Systems," IEEE Transactions on Software Engineering, vol. 26, no. 2, pp. 128-149, Feb. 2000, doi:10.1109/32.841114
Usage of this product signifies your acceptance of the Terms of Use.