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

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 develop...

وصف كامل

التفاصيل البيبلوغرافية
الحاوية / القاعدة:	IEEE Transactions on software engineering 28, 1 (2002).
المؤلف الرئيسي:	Frey, P.
التنسيق:	مقال
اللغة:	English
الموضوعات:	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.