Formal verification and validation with DEVS-Suite: OSPF Case study

Abstract

In this paper, verification and validation of the DEVS models in DEVS-Suite environment are discussed. A case example called OSPF-DEVS simulator is applied and verification and validation tests are performed on it to show usefulness of DEVS formalism. Performed verification and validation tests are followed using a technique developed by Forrester and Senge. Particular attention is paid to reliability and maintainability in view of the state-of-the-art network simulator ns-2. Results are documented to lend confidence to simulation users and to show DEVS-Suite environment's capabilities not to increase model infrastructure. (C) 2012 Elsevier B.V. All rights reserved.