A formal specification and verification framework for Time Warp-based parallel simulation

Author

Frey, Peter ; Radhakrishnan, Radharamanan ; Carter, Harold W. ; Wilsey, Philip A. ; Alexander, Perry

Author_Institution

Cadence Design Syst. Inc., San Jose, CA, USA

Volume

28

Issue

1

fYear

2002

fDate

1/1/2002 12:00:00 AM

Firstpage

58

Lastpage

78

Abstract

The 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

Keywords

formal specification; parallel programming; program verification; theorem proving; time warp simulation; PVS theorem prover; Prototype Verification System; Time Warp paradigm; Time Warp-based parallel simulation; causal ordering; common formal base; correct rollback processing; correctness conditions; distributed simulation kernels; domain specific simulators; event processing; formal specification; formal verification framework; parallel discrete event simulation; type-check condition system; Formal specifications; Time warp simulation;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.979989

Filename

979989