This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Formal Specification and Verification Framework for Time Warp-Based Parallel Simulation
January 2002 (vol. 28 no. 1)
pp. 58-78

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 type-check 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. Solid-State Circuits, vol. 25, no. 2, pp. 353-363, 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. 417-429, 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. 122-127, 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 Industrial-Strength Formal Specification Techniques, (WIFT '95), Apr. 1995, available with specification files, fromhttp://www.csl.sri.comwift-tutorial.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. 50-58, June 1995.
[9] P. Frey, “Protocols for Optimistic Synchronization of Mixed-Mode 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 VHDL-AMS,” Winter Simulation Conf. (WSC '98), Dec. 1998.
[11] P. Frey, R. Radhakrishnan, H.W. Carter, and P. Wilsey, “Optimistic Synchronization of Mixed-Mode Simulators,” Int'l Parallel Processing Symp., (IPPS '98), pp. 694-699, Mar./Apr. 1998.
[12] R. Fujimoto, “Parallel Discrete Event Simulation,” Comm. ACM, vol. 33, no. 10, pp. 30-53, 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. 68-80, 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. 109-145, May 1993.
[15] D.R. Jefferson, "Virtual Time," ACM Trans. Programming Languages and Systems, vol. 7, no. 3, pp. 404-425, 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. 558-565, 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. 771-794, Nov. 1993.
[19] Y.-B. Lin, “Determining the Global Progress of Parallel Simulation with FIFO Commmunication Property,” Information Processing Letters, vol. 50, pp. 13-17, 1994.
[20] Y.-B. Lin and E. Lazowska, “Determining the Global Virtual Time in a Distributed Simulation,” Int'l Conf. Parallel Processing, pp. 201-209, 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. 423-434, 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. Stringer-Calvert, 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. Stringer-Calvert, 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 (FMSP-98), M. Ardis, ed., pp. 16-23, Mar. 1998.
[28] R. Radhakrishnan, D.E. Martin, M. Chetlur, D.M. Rao, and P.A. Wilsey, “An Object-Oriented Time Warp Simulation Kernel,” Proc. Int'l Symp. Computing in Object-Oriented Parallel Environments (ISCOPE '98), D. Caromel, R.R. Oldehoeft, and M. Tholburn, eds., pp. 13-23, Dec. 1998.
[29] R. Rönngren and R. Ayani, “Adaptive Checkpointing in Time Warp,” Proc. Eighth Workshop Parallel and Distributed Simulation (PADS 94), pp. 110-117, July 1994.
[30] M. Rumsey and J. Sackett, “An ASIC Methodology for Mixed Analog-Digital Simulation,” IEEE Micro 8, pp. 34-40, Aug. 1990.
[31] J. Rushby and D.W.J. Stringer-Calvert, “A Less Elementary Tutorial for the PVS Specification and Verification System,” Technical Report SRI-CSL-95-10, Computer Science Laboratory, SRI Int'l, Menlo Park, Calif., June 1995, revised, July 1996, available, with specification files, fromhttp://www.csl.sri.comcsl-95-10.html.

Index Terms:
formal specification, formal verification, theorem proving, parallel discrete event simulation, time warp
Citation:
P. Frey, R. Radhakrishnan, H.W. Carter, P.A. Wilsey, P. Alexander, "A Formal Specification and Verification Framework for Time Warp-Based Parallel Simulation," IEEE Transactions on Software Engineering, vol. 28, no. 1, pp. 58-78, Jan. 2002, doi:10.1109/32.979989
Usage of this product signifies your acceptance of the Terms of Use.