Change search
ReferencesLink to record
Permanent link

Direct link
A Verification Framework for Component Based Modeling and Simulation: “Putting the pieces together”
KTH, School of Information and Communication Technology (ICT), Software and Computer systems, SCS.
2013 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

The discipline of component-based modeling and simulation offers promising gains including reduction in development cost, time, and system complexity. This paradigm is very profitable as it promotes the use and reuse of modular components and is auspicious for effective development of complex simulations. It however is confronted by a series of research challenges when it comes to actually practice this methodology. One of such important issue is Composability verification. In modeling and simulation (M&S), composability is the capability to select and assemble components in various combinations to satisfy specific user requirements. Therefore to ensure the correctness of a composed model, it is verified with respect to its requirements specifications.There are different approaches and existing component modeling frameworks that support composability however in our observation most of the component modeling frameworks possess none or weak built-in support for the composability verification. One such framework is Base Object Model (BOM) which fundamentally poses a satisfactory potential for effective model composability and reuse. However it falls short of required semantics, necessary modeling characteristics and built-in evaluation techniques, which are essential for modeling complex system behavior and reasoning about the validity of the composability at different levels.In this thesis a comprehensive verification framework is proposed to contend with some important issues in composability verification and a verification process is suggested to verify composability of different kinds of systems models, such as reactive, real-time and probabilistic systems. With an assumption that all these systems are concurrent in nature in which different composed components interact with each other simultaneously, the requirements for the extensive techniques for the structural and behavioral analysis becomes increasingly challenging. The proposed verification framework provides methods, techniques and tool support for verifying composability at its different levels. These levels are defined as foundations of a consistent model composability. Each level is discussed in detail and an approach is presented to verify composability at that level. In particular we focus on theDynamic-Semantic Composability level due to its significance in the overallcomposability correctness and also due to the level of difficulty it poses in theprocess. In order to verify composability at this level we investigate the application ofthree different approaches namely (i) Petri Nets based Algebraic Analysis (ii) ColoredPetri Nets (CPN) based State-space Analysis and (iii) Communicating SequentialProcesses based Model Checking. All the three approaches attack the problem ofverifying dynamic-semantic composability in different ways however they all sharethe same aim i.e., to confirm the correctness of a composed model with respect to itsrequirement specifications. Beside the operative integration of these approaches inour framework, we also contributed in the improvement of each approach foreffective applicability in the composability verification. Such as applying algorithmsfor automating Petri Net algebraic computations, introducing a state-space reductiontechnique in CPN based state-space analysis, and introducing function libraries toperform verification tasks and help the molder with ease of use during thecomposability verification. We also provide detailed examples of using each approachwith different models to explain the verification process and their functionality.Lastly we provide a comparison of these approaches and suggest guidelines forchoosing the right one based on the nature of the model and the availableinformation. With a right choice of an approach and following the guidelines of ourcomponent-based M&S life-cycle a modeler can easily construct and verify BOMbased composed models with respect to its requirement specifications.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2013. , 201 p.
TRITA-ICT-ECS AVH, ISSN 1653-6363 ; 13:01
Keyword [en]
Modeling and Simulation, Component-based development, Composability, Semantic Composability, Dynamic-Semantic Composability, Verification, Correctness, Petri Nets Analysis, Algebraic Techniques, Colored Petri Nets, State-space Analysis, Communicating Sequential Processes, Model Checking.
National Category
Computer Systems
Research subject
URN: urn:nbn:se:kth:diva-116678ISBN: 978-91-7501-628-3OAI: diva2:600204
Public defence
2013-02-26, SAL E, Forum, KTH-ICT, Isafjordgatan 39, Kista, 14:00 (English)

Overseas Scholarship for PHD in selected Studies Phase II Batch I

Higher Education Commision of Pakistan.

QC 20130224

Available from: 2013-01-24 Created: 2013-01-23 Last updated: 2014-01-24Bibliographically approved

Open Access in DiVA

PHDThesis-imahmood2013(10601 kB)1163 downloads
File information
File name FULLTEXT01.pdfFile size 10601 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Mahmood, Imran
By organisation
Software and Computer systems, SCS
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 1163 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 955 hits
ReferencesLink to record
Permanent link

Direct link