Verification and Validation in Systems Engineering (eBook)

Preface 6
Acknowledgments 9
Contents 10
List of Figures 15
List of Tables 18
Acronyms 20
1 Introduction 22
1.1 Verification and Validation Problem Statement 23
1.2 Systems Engineering 24
1.3 Systems Engineering Standards 26
1.4 Model-Driven Architecture 27
1.5 Systems Engineering Modeling Languages 29
1.5.1 UML 2.x: Unified Modeling Language 29
1.5.2 SysML: Systems Modeling Language 30
1.5.3 IDEF: Integration Definition Methods 31
1.6 Outline 32
2 Architecture Frameworks, Model-Driven Architecture, and Simulation 35
2.1 Architecture Frameworks 36
2.1.1 Zachman Framework 36
2.1.2 Open Group Architecture Framework 37
2.1.3 DoD Architecture Framework 38
2.1.4 UK Ministry of Defence Architecture Framework 45
2.1.5 UML Profile for DoDAF/MODAF 45
2.2 AP233 Standard for Data Exchange 46
2.3 Executable Architectures or from Design to Simulation 46
2.3.1 Why Executable Architectures? 47
2.3.2 Modeling and Simulation as an Enabler for Executable Architectures 48
2.4 DoDAF in Relation to SE and SysML 51
2.5 Conclusion 55
3 Unified Modeling Language 56
3.1 UML History 56
3.2 UML Diagrams 57
3.2.1 Class Diagram 58
3.2.2 Component Diagram 59
3.2.3 Composite Structure Diagram 60
3.2.4 Deployment Diagram 61
3.2.5 Object Diagram 62
3.2.6 Package Diagram 62
3.2.7 Activity Diagram 63
3.2.8 Activity Diagram Execution 66
3.2.9 Use Case Diagram 67
3.2.10 State Machine Diagram 68
3.2.11 Sequence Diagram 72
3.2.12 Communication Diagram 74
3.2.13 Interaction Overview Diagram 75
3.2.14 Timing Diagram 76
3.3 UML Profiling Mechanisms 77
3.4 Conclusion 78
4 Systems Modeling Language 79
4.1 SysML History 79
4.2 UML and SysML Relationships 80
4.3 SysML Diagrams 81
4.3.1 Block Definition Diagram 82
4.3.2 Internal Block Diagram 83
4.3.3 Package Diagram 84
4.3.4 Parametric Diagram 84
4.3.5 Requirement Diagram 85
4.3.6 Activity Diagram 87
4.3.7 State Machine Diagram 89
4.3.8 Use Case Diagram 90
4.3.9 Sequence Diagram 90
4.4 Conclusion 91
5 Verification, Validation, and Accreditation 92
5.1 V& V Techniques Overview
5.1.1 Inspection 94
5.1.2 Testing 94
5.1.3 Simulation 95
5.1.4 Reference Model Equivalence Checking 96
5.1.5 Theorem Proving 96
5.2 Verification Techniques for Object-Oriented Design 96
5.2.1 Design Perspectives 97
5.2.2 Software Engineering Techniques 97
5.2.3 Formal Verification Techniques 98
5.2.4 Program Analysis Techniques 99
5.3 V& V of Systems Engineering Design Models
5.4 Tool Support 105
5.4.1 Formal Verification Environments 105
5.4.2 Static Analyzers 107
5.5 Conclusion 109
6 Automatic Approach for Synergistic Verification and Validation 111
6.1 Synergistic Verification and Validation Methodology 112
6.2 Dedicated V& V Approach for Systems Engineering
6.2.1 Automatic Formal Verification of System Design Models 115
6.2.2 Program Analysis of Behavioral Design Models 116
6.2.3 Software Engineering Quantitative Techniques 117
6.3 Probabilistic Behavior Assessment 117
6.4 Established Results 118
6.5 Verification and Validation Tool 119
6.6 Conclusion 121
7 Software Engineering Metrics in the Context of Systems Engineering 122
7.1 Metrics Suites Overview 122
7.1.1 Chidamber and Kemerer Metrics 122
7.1.2 MOOD Metrics 123
7.1.3 Li and Henry's Metrics 124
7.1.4 Lorenz and Kidd's Metrics 124
7.1.5 Robert Martin Metrics 124
7.1.6 Bansiya and Davis Metrics 125
7.1.7 Briand et al. Metrics 125
7.2 Quality Attributes 126
7.3 Software Metrics Computation 126
7.3.1 Abstractness (A) 127
7.3.2 Instability (I) 127
7.3.3 Distance from the Main Sequence (DMS) 128
7.3.4 Class Responsibility (CR) 128
7.3.5 Class Category Relational Cohesion (CCRC) 129
7.3.6 Depth of Inheritance Tree (DIT) 129
7.3.7 Number of Children (NOC) 129
7.3.8 Coupling Between Object Classes (CBO) 130
7.3.9 Number of Methods (NOM) 131
7.3.10 Number of Attributes (NOA) 132
7.3.11 Number of Methods Added (NMA) 132
7.3.12 Number of Methods Overridden (NMO) 133
7.3.13 Number of Methods Inherited (NMI) 133
7.3.14 Specialization Index (SIX) 134
7.3.15 Public Methods Ratio (PMR) 134
7.4 Case Study 135
7.5 Conclusion 138
8 Verification and Validation of UML Behavioral Diagrams 140
8.1 Configuration Transition System 140
8.2 Model Checking of Configuration Transition Systems 142
8.3 Property Specification Using CTL 144
8.4 Program Analysis of Configuration Transition Systems 145
8.5 V& V of UML State Machine Diagram
8.5.1 Semantic Model Derivation 147
8.5.2 Case Study 149
8.5.3 Application of Program Analysis 153
8.6 V& V of UML Sequence Diagram
8.6.1 Semantic Model Derivation 156
8.6.2 Sequence Diagram Case Study 157
8.7 V& V of UML Activity Diagram
8.7.1 Semantic Model Derivation 160
8.7.2 Activity Diagram Case Study 160
8.8 Conclusion 167
9 Probabilistic Model Checking of SysML Activity Diagrams 168
9.1 Probabilistic Verification Approach 168
9.2 Translation into PRISM 170
9.3 PCTL* Property Specification 175
9.4 Case Study 176
9.5 Conclusion 181
10 Performance Analysis of Time-Constrained SysML Activity Diagrams 182
10.1 Time Annotation 182
10.2 Derivation of the Semantic Model 184
10.3 Model-Checking Time-Constrained Activity Diagrams 185
10.3.1 Discrete-Time Markov Chain 187
10.3.2 PRISM Input Language 187
10.3.3 Mapping SysML Activity Diagrams into DTMC 188
10.3.4 Threads Identification 188
10.4 Performance Analysis Case Study 191
10.5 Scalability 196
10.6 Conclusion 202
11 Semantic Foundations of SysML Activity Diagrams 204
11.1 Activity Calculus 204
11.1.1 Syntax 205
11.1.2 Operational Semantics 209
11.2 Case Study 215
11.3 Markov Decision Process 218
11.4 Conclusion 218
12 Soundness of the Translation Algorithm 219
12.1 Notation 219
12.2 Methodology 220
12.3 Formalization of the PRISM Input Language 220
12.3.1 Syntax 221
12.3.2 Operational Semantics 222
12.4 Formal Translation 224
12.5 Case Study 227
12.6 Simulation Preorder for Markov Decision Processes 229
12.7 Soundness of the Translation Algorithm 231
12.8 Conclusion 236
13 Conclusion 237
References 241
Index 254