Verification and Validation in Systems Engineering

by Debbabi, Mourad; Hassaine, Fawzi; Jarraya, Yosr; Soeanu, Andrei

• ISBN13: 9783642152276
• ISBN10: 3642152279
• Format: Hardcover
• Copyright: 2010-11-19
• Publisher: Springer-Nature New York Inc

Summary

Verification and validation represents an important process used for the quality assessment of engineered systems and their compliance with the requirements established at the beginning of or during the development cycle.Debbabi and his coauthors investigate methodologies and techniques that can be employed for the automatic verification and validation of systems engineering design models expressed in standardized modeling languages. Their presentation includes a bird's eye view of the most prominent modeling languages for software and systems engineering, namely the Unified Modeling Language (UML) and the more recent Systems Modeling Language (SysML). Moreover, it elaborates on a number of quantitative and qualitative techniques that synergistically combine automatic verification techniques, program analysis, and software engineering quantitative methods applicable to design models described in these modeling languages. Each of these techniques is additionally explained using a case study highlighting the process, its results, and resulting changes in the system design.Researchers in academia and industry as well as students specializing in software and systems engineering will find here an overview of state-of-the-art validation and verification techniques. Due to their close association with the UML standard, the presented approaches are also applicable to industrial software development.

Table of Contents

Introduction	p. 1
Verification and Validation Problem Statement	p. 2
Systems Engineering	p. 3
Systems Engineering Standards	p. 5
Model-Driven Architecture	p. 6
Systems Engineering Modeling Languages	p. 8
UML 2.x: Unified Modeling Language	p. 8
SysML: Systems Modeling Language	p. 9
IDEF: Integration Definition Methods	p. 10
Outline	p. 11
Architecture Frameworks, Model-Driven Architecture, and Simulation	p. 15
Architecture Frameworks	p. 16
Zachman Framework	p. 16
Open Group Architecture Framework	p. 17
DoD Architecture Framework	p. 18
UK Ministry of Defence Architecture Framework	p. 25
UML Profile for DoDAF/MODAF	p. 25
AP233 Standard for Data Exchange	p. 26
Executable Architectures or from Design to Simulation	p. 26
Why Executable Architectures?	p. 27
Modeling and Simulation as an Enabler for Executable Architectures	p. 28
DoDAF in Relation to SE and SysML	p. 31
Conclusion	p. 35
Unified Modeling Language	p. 37
UML History	p. 37
UML Diagrams	p. 38
Class Diagram	p. 39
Component Diagram	p. 40
Composite Structure Diagram	p. 41
Deployment Diagram	p. 42
Object Diagram	p. 43
Package Diagram	p. 43
Activity Diagram	p. 44
Activity Diagram Execution	p. 47
Use Case Diagram	p. 48
State Machine Diagram	p. 49
Sequence Diagram	p. 53
Communication Diagram	p. 55
Interaction Overview Diagram	p. 56
Timing Diagram	p. 57
UML Profiling Mechanisms	p. 58
Conclusion	p. 59
Systems Modeling Language	p. 61
SysML History	p. 61
UML and SysML Relationships	p. 62
SysML Diagrams	p. 63
Block Definition Diagram	p. 64
Internal Block Diagram	p. 65
Package Diagram	p. 66
Parametric Diagram	p. 66
Requirement Diagram	p. 67
Activity Diagram	p. 69
State Machine Diagram	p. 71
Use Case Diagram	p. 72
Sequence Diagram	p. 72
Conclusion	p. 73
Verification, Validation, and Accreditation	p. 75
V&V Techniques Overview	p. 76
Inspection	p. 77
Testing	p. 77
Simulation	p. 78
Reference Model Equivalence Checking	p. 79
Theorem Proving	p. 79
Verification Techniques for Object-Oriented Design	p. 79
Design Perspectives	p. 80
Software Engineering Techniques	p. 80
Formal Verification Techniques	p. 81
Program Analysis Techniques	p. 82
V&V of Systems Engineering Design Models	p. 83
Tool Support	p. 88
Formal Verification Environments	p. 88
Static Analyzers	p. 90
Conclusion	p. 92
Automatic Approach for Synergistic Verification and Validation	p. 95
Synergistic Verification and Validation Methodology	p. 96
Dedicated V&V Approach for Systems Engineering	p. 99
Automatic Formal Verification of System Design Models	p. 99
Program Analysis of Behavioral Design Models	p. 100
Software Engineering Quantitative Techniques	p. 101
Probabilistic Behavior Assessment	p. 101
Established Results	p. 102
Verification and Validation Tool	p. 103
Conclusion	p. 105
Software Engineering Metrics in the Context of Systems Engineering	p. 107
Metrics Suites Overview	p. 107
Chidamber and Kemerer Metrics	p. 107
MOOD Metrics	p. 108
Li and Henry's Metrics	p. 109
Lorenz and Kidd's Metrics	p. 109
Robert Martin Metrics	p. 109
Bansiya and Davis Metrics	p. 110
Briand et al. Metrics	p. 110
Quality Attributes	p. 111
Software Metrics Computation	p. 111
Abstractness (A)	p. 112
Instability (I)	p. 112
Distance from the Main Sequence (DMS)	p. 113
Class Responsibility (CR)	p. 113
Class Category Relational Cohesion (CCRC)	p. 114
Depth of Inheritance Tree (DIT)	p. 114
Number of Children (NOC)	p. 114
Coupling Between Object Classes (CBO)	p. 115
Number of Methods (NOM)	p. 116
Number of Attributes (NOA)	p. 117
Number of Methods Added (NMA)	p. 117
Number of Methods Overridden (NMO)	p. 118
Number of Methods Inherited (NMI)	p. 118
Specialization Index (SIX)	p. 119
Public Methods Ration (PMR)	p. 119
Case Study	p. 120
Conclusion	p. 123
Verification and Validation of UML Behavioral Diagrams	p. 125
Configuration Transition System	p. 125
Model Checking of Configuration Transition Systems	p. 127
Property Specification Using CTL	p. 129
Program Analysis of Configuration Transition Systems	p. 130
V&V of UML State Machine Diagram	p. 131
Semantic Model Derivation	p. 132
Case Study	p. 134
Application of Program Analysis	p. 138
V&V of UML Sequence Diagram	p. 141
Semantic Model Derivation	p. 141
Sequence Diagram Case Study	p. 142
V&V of UML Activity Diagram	p. 145
Semantic Model Derivation	p. 145
Activity Diagram Case Study	p. 145
Conclusion	p. 152
Probabilistic Model Checking of SysML Activity Diagrams	p. 153
Probabilistic Verification Approach	p. 153
Translation into PRISM	p. 155
PCTL* Property Specification	p. 160
Case Study	p. 161
Conclusion	p. 166
Performance Analysis of Time-Constrained SysML Activity Diagrams	p. 167
Time Annotation	p. 167
Derivation of the Semantic Model	p. 169
Model-Checking Time-Constrained Activity Diagrams	p. 170
Discrete-Time Markov Chain	p. 172
PRISM Input Language	p. 172
Mapping SysML Activity Diagrams into DTMC	p. 173
Threads Identification	p. 173
Performance Analysis Case Study	p. 176
Scalability	p. 181
Conclusion	p. 187
Semantic Foundations of SysML Activity Diagrams	p. 189
Activity Calculus	p. 189
Syntax	p. 190
Operational Semantics	p. 194
Case Study	p. 200
Markov Decision Process	p. 203
Conclusion	p. 203
Soundness of the Translation Algorithm	p. 205
Notation	p. 205
Methodology	p. 206
Formalization of the PRISM Input Language	p. 206
Syntax	p. 207
Operational Semantics	p. 208
Formal Translation	p. 210
Case Study	p. 213
Simulation Preorder for Markov Decision Processes	p. 215
Soundness of the Translation Algorithm	p. 217
Conclusion	p. 222
Conclusion	p. 223
References	p. 227
Index	p. 241
Table of Contents provided by Ingram. All Rights Reserved.