
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
P. Frey, R. Radhakrishnan, H.W. Carter, P.A. Wilsey, P. Alexander, "A Formal Specification and Verification Framework for Time WarpBased Parallel Simulation," IEEE Transactions on Software Engineering, vol. 28, no. 1, pp. 5878, January, 2002.  
BibTex  x  
@article{ 10.1109/32.979989, author = {P. Frey and R. Radhakrishnan and H.W. Carter and P.A. Wilsey and P. Alexander}, title = {A Formal Specification and Verification Framework for Time WarpBased Parallel Simulation}, journal ={IEEE Transactions on Software Engineering}, volume = {28}, number = {1}, issn = {00985589}, year = {2002}, pages = {5878}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.979989}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  A Formal Specification and Verification Framework for Time WarpBased Parallel Simulation IS  1 SN  00985589 SP58 EP78 EPD  5878 A1  P. Frey, A1  R. Radhakrishnan, A1  H.W. Carter, A1  P.A. Wilsey, A1  P. Alexander, PY  2002 KW  formal specification KW  formal verification KW  theorem proving KW  parallel discrete event simulation KW  time warp VL  28 JA  IEEE Transactions on Software Engineering ER   
This paper describes a formal framework developed using the Prototype Verification System (PVS) to model and verify distributed simulation kernels based on the Time Warp paradigm. The intent is to provide a common formal base from which domain specific simulators can be modeled, verified, and developed. PVS constructs are developed to represent basic Time Warp constructs. Correctness conditions for Time Warp simulation are identified describing causal ordering of event processing and correct rollback processing. The PVS theorem prover and typecheck condition system are then used to verify all correctness conditions. In addition, the paper discusses the framework's reusability and extensibility properties in support of specification and verification of Time Warp extensions and optimizations.
[1] E.L. Acuna, J.P. Dervenis, A.J. Pagones, F.L. Yang, and R.A. Saleh, “Simulation Techniques for Mixed Analog/Digital Circuits,” IEEE J. SolidState Circuits, vol. 25, no. 2, pp. 353363, Apr. 1990.
[2] B.A.A. Antao and A.J. Brodersen, “Behavioral Simulation for Analog System Design Verification,” IEEE Trans. Very Large Scale Intergration Systems, vol. 3, no. 3, pp. 417429, Sept. 1995.
[3] H. Bauer, “Verteilte Diskrete Simulation Komplexer Systeme,” PhD thesis, Technische Univ. München, 1994.
[4] S. Bellenot, “Global Virtual Time Algorithms,” Society for Computer Simulation, Distributed Simulation, pp. 122127, Jan. 1990.
[5] K.M. Chandy and L. Lamport, "Distributed Snapshots: Determining Global States of Distributed Systems," ACM Trans. Computer Systems, Feb. 1985.
[6] V. Chernyakhovsky, P. Frey, R. Radhakrishnan, P.A. Wilsey, P. Alexander, and H.W. Carter, “A Formal Framework for Specifying and Verifying Time Warp Optimizations,” Proc. Fourth Int'l Workshop Formal Methods for Parallel Programming: Theory and Applications (FMPPTA '99), Apr. 1999.
[7] J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, “A Tutorial Introduction to PVS,” Workshop IndustrialStrength Formal Specification Techniques, (WIFT '95), Apr. 1995, available with specification files, fromhttp://www.csl.sri.comwifttutorial.html .
[8] J. Fleischmann and P.A. Wilsey, “Comparative Analysis of Periodic State Saving Techniques in TimeWarp Simulators,” Proc. Ninth Workshop Parallel and Distributed Simulation (PADS '95), pp. 5058, June 1995.
[9] P. Frey, “Protocols for Optimistic Synchronization of MixedMode Simulation,” PhD thesis, Univ. of Cincinnati, Aug. 1998.
[10] P. Frey, K. Nellayappan, V. Shanmugasundaram, R.S. Mayiladuthurai, C.L. Chandrashekar, and H.W. Carter, “SEAMS: Simulation Environment for VHDLAMS,” Winter Simulation Conf. (WSC '98), Dec. 1998.
[11] P. Frey, R. Radhakrishnan, H.W. Carter, and P. Wilsey, “Optimistic Synchronization of MixedMode Simulators,” Int'l Parallel Processing Symp., (IPPS '98), pp. 694699, Mar./Apr. 1998.
[12] R. Fujimoto, “Parallel Discrete Event Simulation,” Comm. ACM, vol. 33, no. 10, pp. 3053, Oct. 1990.
[13] S. Ghosh, “On the Proof of Correctness of Yet Another Asynchronous Distributed Discrete Event Simulation Algorithm (YADDES),” IEEE Trans. Systems. Man and Cybernetics–Part A: Systems and Humans, vol. 26, no. 1, pp. 6880, Jan. 1996.
[14] G.C. Gopalakrishnan and M. Fujimoto, “Design and Verification of the Rollback Chip Using Hop: A Case Study of Formal Methods Applied to Hardware Design,” ACM Trans. Computer Systems, vol. 11, no. 2, pp. 109145, May 1993.
[15] D.R. Jefferson, "Virtual Time," ACM Trans. Programming Languages and Systems, vol. 7, no. 3, pp. 404425, July 1985.
[16] B. Kannikeswaran, R. Radhakrishnan, P. Frey, P. Alexander, and P.A. Wilsey, “Formal Specification and Verification of the pGVT Algorithm,” Industrial Benefit and Advances in Formal Methods, (FME '96), Mar. 1996.
[17] L. Lamport, "Time, clocks and the ordering of events in a distributed system," Comm. ACM, vol. 21, no. 7, pp. 558565, July 1978.
[18] J.I. Leivent and R.J. Watro, “Mathematical Foundationsfor Time Warp Systems,” ACM Trans. Programming Languages and Systems, vol. 15, no. 5, pp. 771794, Nov. 1993.
[19] Y.B. Lin, “Determining the Global Progress of Parallel Simulation with FIFO Commmunication Property,” Information Processing Letters, vol. 50, pp. 1317, 1994.
[20] Y.B. Lin and E. Lazowska, “Determining the Global Virtual Time in a Distributed Simulation,” Int'l Conf. Parallel Processing, pp. 201209, 1990.
[21] D.E. Martin, T. McBrayer, and P.A. Wilsey, Warped: A Time Warp Simulation Kernel for Analysis and Application Development, 1995, available on the WWW athttp://www.ece.uc.edu/~pawwarped/.
[22] F. Mattern, “Efficient Algorithms for Distributed Snapshots and Global Virtual Time Approximation,” J. Parallel and Distributed Computing, vol. 18, no. 4, pp. 423434, Aug. 1993.
[23] N. Shankar, S. Owre, and J.M. Rushby, The PVS Proof Checker: A Reference Manual, Menlo Park, Calif.: Computer Science Laboratory, SRI Int'l, Feb. 1993.
[24] S. Owre, N. Shankar, J. Rushby, and D. StringerCalvert, PVS, System Guide, 2.3 ed. Menlo Park, Calif.: SRI Int'l Computer Science Laboratory, Sept. 1999.
[25] S. Owre, N. Shankar, and J.M. Rushby, The PVS Specification Language, Menlo Park, Calif.: Computer Science Laboratory, SRI Int'l, Feb. 1993.
[26] S. Owre, N. Shankar, J.M. Rushby, and D.W.J. StringerCalvert, PVS Language Reference. Menlo Park, Calif.: Computer Science Laboratory, SRI Int'l, Sept. 1999.
[27] J. Penix, D. Martin, P. Frey, R. Radhakrishnan, P. Alexander, and P.A. Wilsey, “Experiences in Verifying Parallel Simulation Algorithms,” Proc. Second Workshop Formal Methods in Software Practice (FMSP98), M. Ardis, ed., pp. 1623, Mar. 1998.
[28] R. Radhakrishnan, D.E. Martin, M. Chetlur, D.M. Rao, and P.A. Wilsey, “An ObjectOriented Time Warp Simulation Kernel,” Proc. Int'l Symp. Computing in ObjectOriented Parallel Environments (ISCOPE '98), D. Caromel, R.R. Oldehoeft, and M. Tholburn, eds., pp. 1323, Dec. 1998.
[29] R. Rönngren and R. Ayani, “Adaptive Checkpointing in Time Warp,” Proc. Eighth Workshop Parallel and Distributed Simulation (PADS 94), pp. 110117, July 1994.
[30] M. Rumsey and J. Sackett, “An ASIC Methodology for Mixed AnalogDigital Simulation,” IEEE Micro 8, pp. 3440, Aug. 1990.
[31] J. Rushby and D.W.J. StringerCalvert, “A Less Elementary Tutorial for the PVS Specification and Verification System,” Technical Report SRICSL9510, Computer Science Laboratory, SRI Int'l, Menlo Park, Calif., June 1995, revised, July 1996, available, with specification files, fromhttp://www.csl.sri.comcsl9510.html.