Please use this identifier to cite or link to this item:
Title: Composable simulation models and their formal validation
Keywords: semantic composability, validation, simulation
Issue Date: 7-Sep-2010
Source: CLAUDIA SZABO (2010-09-07). Composable simulation models and their formal validation. ScholarBank@NUS Repository.
Abstract: In component-based modeling and simulation, shared models are reused and assembled in various combinations to meet different user requirements, resulting in an appealing approach to reduce the time and cost of developing complex simulations. Towards achieving this goal, there are several challenges including the lack of methodologies and techniques to support the life-cycle of component-based development, and the validation of semantic composability among others. This thesis focuses on two main directions: a new component-based modeling and simulation approach, and a novel semantic composability validation strategy.<br/><br/> The key to our proposed integrated component-based approach is the abstraction and specification of components as meta components using semantically sugared attribute values from a new component-based simulation ontology. This ontology is designed to capture component behaviors and to support model composition across applications, as well as the verification and validation of the composed model. Using a component-connector paradigm, components in a composed model interact only through well-defined connectors. This allows us to formally specify the composition using EBNF grammars. The representation of the composed models as production strings simplifies and facilitates automated syntactic verification and model discovery and selection. Another key design decision in our approach is the modeling of real-world basic entities as base components, and reusable models as model components, to achieve greater reuse within and across application domains.<br/><br/> In semantic composability, our main design considerations and trade-offs are validation accuracy and computational cost. Two key observations are: in model validation, the interactions of component behaviors grow rapidly and lead to the problem of exponential state-space explosion; and current techniques that focus on checking that a model is semantically valid are computationally more costly than checking for model invalidity. Based on these two insights, we propose a new deny validity semantic validation strategy. Firstly, the model is validated for general model properties such as safety and liveness, which is less costly for identifying invalid models. Models that pass this test have increased credibility, and are then subjected to a more rigorous but expensive formal semantic validation. A new time-based semantic validation technique is proposed. Since semantic validity is not a fixed-point answer, we introduce a new metric to quantify semantic similarity among different models. <br/><br/> Our approach is validated using both theoretical and experimental analysis. We illustrate our component-based approach using three examples: a simple queueing system to introduce key concepts, a more complex component-based grid system to illustrate model component reuse, and a data-driven military training simulation scenario to demonstrate composition and validation in a new and more complex application domain. Theoretical and experimental analysis using our prototype implementation demonstrates that our approach is appealing as initially envisaged, and our deny validity semantic validation strategy provides a framework to advance the understanding of the trade-offs between validation accuracy and computational cost. Lastly, we highlight a number of new insights and research challenges.
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
ClaudiaSzabo - PhD Thesis - Composable Simulation Models and their Formal Validation.pdf2.83 MBAdobe PDF



Page view(s)

checked on Dec 11, 2017


checked on Dec 11, 2017

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.