Embedded systems : analysis and modeling with SysML, UML and AADL

Since the construction of the first embedded system in the 1960s, embedded systems have continued to spread. They provide a continually increasing number of services and are part of our daily life. The development of these systems is a difficult problem which does not yet have a global solution. Another difficulty is that systems are plunged into the real world, which is not discrete (as is generally understood in computing), but has a richness of behaviors which sometimes hinders the formulation of simplifying assumptions due to their generally autonomous nature and they must face possibly unforeseen situations (incidents, for example), or even situations that lie outside the initial design assumptions.

Embedded Systems presents the state of the art of the development of embedded systems and, in particular, concentrates on the modeling and analysis of these systems by looking at "model-driven engineering", (MDE2): SysML, UML/MARTE and AADL. A case study (based on a pacemaker) is presented which enables the reader to observe how the different aspects of a system are addressed using the different approaches. All three systems are important in that they provide the reader with a global view of their possibilities and demonstrate the contributions of each approach in the different stages of the software lifecycle. Chapters dedicated to analyzing the specification and code generation are also presented.

Contents

Foreword, Brian R. Larson.
Foreword, Dominique Potier.
Introduction, Fabrice Kordon, Jérôme Hugues, Agusti Canals and Alain Dohet.
Part 1. General Concepts
1. Elements for the Design of Embedded Computer Systems, Fabrice Kordon, Jérôme Hugues, Agusti Canals and Alain Dohet.
2. Case Study: Pacemaker, Fabrice Kordon, Jérôme Hugues, Agusti Canals and Alain Dohet.
Part 2. SysML
3. Presentation of SysML Concepts, Jean-Michel Bruel and Pascal Roques.
4. Modeling of the Case Study Using SysML, Loïc Fejoz, Philippe Leblanc and Agusti Canals.
5. Requirements Analysis, Ludovic Apvrille and Pierre De Saqui-Sannes.
Part 3. MARTE
6. An Introduction to MARTE Concepts, Sébastien Gérard and François Terrier.
7. Case Study Modeling Using MARTE, Jérôme Delatour and Joël Champeau.
8. Model-Based Analysis, Frederic Boniol, Philippe Dhaussy, Luka Le Roux and Jean-Charles Roger.
9. Model-Based Deployment and Code Generation, Chokri Mraidha, Ansgar Radermacher and Sébastien Gérard.
Part 4. AADL
10. Presentation of the AADL Concepts, Jérôme Hugues and Xavier Renault.
11. Case Study Modeling Using AADL, Etienne Borde.
12. Model-Based Analysis, Thomas Robert and Jérôme Hugues.
13. Model-Based Code Generation, Laurent Pautet and Béchir Zalila.

Author Notes

Fabrice Kordon is Professor at University Pierre and Marie Curie in Paris, France, where he is in charge of the team "Modlisation et vrification" of the LIP6. His research field is at the crossroads of distributed systems, software engineering and formal methods.
Jrme Hugues is lecturer-researcher at the Institut Suprieur de I'Aronautique et de I'Espace (ISAE) in Toulouse, France and has been a member of the language standardization committee (AADL) since 2006. His research fields cover the engineering of embedded systems and the generation of automatic code of these systems from modeling languages, integrating verification and analysis tools on the model and code level.
Agusti Canals is a software engineer and has worked at CS "Communication et Systmes" in Paris, France since 1981. He is deputy director of the "Direction de la Qualit et des Audits Techniques" (DQAT) of CS and an expert in software engineering (certified "UML Professional" and "SysML Builder" by OMG).
Alain Dohet is a general armament engineer at the "Direction Gnrale pour I'Armement" (organization of the French Defense Minister ensuring the conduct of system programs), where he is in charge of guiding activities, skills, methods and tools in the fields of systems of systems (SoS), systems engineering, analysis for certification purposes, operational safety of embedded computing systems and critical software.

Brian R. LarsonDominique PotierFabrice Kordon and Jérôme Hugues and Agusti Canals and Alain DohetFabrice Kordon and Jérôme Hugues and Agusti Canals and Alain DohetFabrice Kordon and Jérôme Hugues and Agusti Canals and Alain DohetJean-Michel Bruel and Pascal RoquesLoïc Fejoz and Philippe Leblanc and Agusti CanalsLudovic Apvrille and Pierre de Saqui-SannesSébastien Gérard and François TerrierJérôme Delatour and Joël ChampeauFrederic Boniol and Philippe Dhaussy and Luka Le Roux and Jean-Charles RogerChokri Mraidha and Ansgar Radermacher and Sébastien GérardJérome Hugues and Xavier RenaultEtienne BordeThomas Robert and Jérôme HuguesLaurent Pautet and Béchir Zalila

Foreword	p. xiii
Foreword	p. xv
Introduction	p. xix
Part 1 General Concepts	p. 1
Chapter 1 Elements for the Design of Embedded Computer Systems	p. 3
1.1 Introduction	p. 3
1.2 System modeling	p. 5
1.3 A brief presentation of UML	p. 6
1.3.1 The UML static diagrams	p. 9
1.3.2 The UML dynamic diagrams	p. 10
1.4 Model-driven development approaches	p. 10
1.4.1 The concepts	p. 10
1.4.2 The technologies	p. 11
1.4.3 The context of the wider field	p. 12
1.5 System analysis	p. 14
1.5.1 Formal verification via proving	p. 15
1.5.2 Formal verification by model-checking	p. 15
1.5.3 The languages to express specifications	p. 16
1.5.4 The actual limits of formal approaches	p. 19
1.6 Methodological aspects of the development of embedded computer systems	p. 20
1.6.1 The main technical processes	p. 22
1.6.2 The importance of the models	p. 23
1.7 Conclusion	p. 24
1.8 Bibliography	p. 25
Chapter 2 Case Study: Pacemaker	p. 29
2.1 Introduction	p. 29
2.2 The heart and the pacemaker	p. 30
2.2.1 The heart	p. 30
2.2.2 Presentation of a pacemaker	p. 32
2.3 Case study specification	p. 33
2.3.1 System definition	p. 34
2.3.2 System lifecycle	p. 35
2.3.3 System requirements	p. 36
2.3.4 Pacemaker behavior	p. 39
2.4 Conclusion	p. 42
2.5 Bibliography	p. 43
Part 2 SysML	p. 45
Chapter 3 Presentation of SysML Concepts	p. 47
3.1 Introduction	p. 47
3.2 The origins of SysML	p. 48
3.3 General overview: the nine types of diagrams	p. 49
3.4 Modeling the requirements	p. 50
3.4.1 Use case diagram	p. 50
3.4.2 Requirement diagram	p. 51
3.5 Structural modeling	p. 53
3.5.1 Block definition diagram	p. 54
3.5.2 Internal block diagram	p. 56
3.5.3 Package diagram	p. 58
3.6 Dynamic modeling	p. 59
3.6.1 Sequence diagram	p. 59
3.6.2 State machine diagram	p. 61
3.6.3 Activity diagram	p. 63
3.7 Transverse modeling	p. 65
3.7.1 Parametric diagram	p. 65
3.7.2 Allocation and traceability	p. 67
3.8 Environment and tools	p. 68
3.9 Conclusion	p. 68
3.10 Bibliography	p. 68
Chapter 4 Modeling of the Case Study Using SysML	p. 71
4.1 Introduction	p. 71
4.2 System specification	p. 73
4.2.1 Context	p. 73
4.2.2 Requirements model and operational scenarios	p. 75
4.2.3 Requirements model	p. 78
4.3 System design	p. 80
4.3.1 Functional model	p. 81
4.3.2 Domain-specific data	p. 83
4.3.3 Logical architectural model	p. 86
4.3.4 Physical architectural model	p. 90
4.4 Traceability and allocations	p. 90
4.4.1 "Technical needs: divers" traceability diagram	p. 90
4.4.2 Traceability diagram "technical needs: behavior of the pacemaker"	p. 91
4.4.3 Allocation diagram	p. 92
4.5 Test model	p. 93
4.5.1 Traceability diagram "system test: requirements verification"	p. 93
4.5.2 Sequence diagram for the test game TC-PM-07	p. 94
4.5.3 Diagrams presenting a general view of the requirements	p. 94
4.6 Conclusion	p. 95
4.7 Bibliography	p. 97
Chapter 5 Requirements Analysis	p. 99
5.1 Introduction	p. 99
5.2 The AVATAR language and the TTool tool	p. 100
5.2.1 Method	p. 101
5.2.2 AVATAR language and SysML standard	p. 101
5.2.3 The TEPE language for expressing properties	p. 102
5.2.4 TTool	p. 103
5.3 An AVATAR expression of the SysML model of the enhanced pacemaker	p. 103
5.3.1 Functioning of the pacemaker and modeling hypotheses	p. 103
5.3.2 Requirements diagram	p. 104
5.4 Architecture	p. 105
5.5 Behavior	p. 106
5.6 Formal verification of the VVI mode	p. 107
5.6.1 General properties	p. 108
5.6.2 Expressing properties using TEPE	p. 108
5.6.3 The use of temporal logic	p. 109
5.6.4 Observer-guided verification	p. 111
5.6.5 Coming back to the model	p. 112
5.7 Related work	p. 113
5.7.1 Languages	p. 113
5.7.2 Tools	p. 114
5.8 Conclusion	p. 115
5.9 Appendix: TTool	p. 116
5.10 Bibliography	p. 116
Part 3 Marte	p. 119
Chapter 6 An Introduction to MARTE Concepts	p. 121
6.1 Introduction	p. 121
6.2 General remarks	p. 121
6.2.1 Possible uses of MARTE	p. 122
6.2.2 How should we read the norm?	p. 123
6.2.3 The MARTE architecture	p. 124
6.2.4 MARTE and SysML	p. 127
6.2.5 An open source support	p. 128
6.3 Several MARTE details	p. 128
6.3.1 Modeling non-functional properties	p. 128
6.3.2 A components model for the real-time embedded system	p. 133
6.4 Conclusion	p. 137
6.5 Bibliography	p. 137
Chapter 7 Case Study Modeling Using MARTE	p. 139
7.1 Introduction	p. 139
7.1.1 Hypotheses used in modeling	p. 139
7.1.2 The modeling methodology used	p. 140
7.1.3 Chapter layout	p. 141
7.2 Software analysis	p. 141
7.2.1 Use case and interface characterization	p. 141
7.2.2 The sphere of application	p. 144
7.3 Preliminary software design - the architectural component	p. 145
7.3.1 The candidate architecture	p. 146
7.3.2 Identifying the components	p. 146
7.3.3 Presentation of the candidate architecture	p. 148
7.3.4 A presentation of the detailed interfaces	p. 150
7.4 Software preliminary design - behavioral component	p. 151
7.4.1 The controller	p. 151
7.4.2 The cardiologist	p. 153
7.4.3 The operating modes of the cardiologist	p. 153
7.5 Conclusion	p. 155
7.6 Bibliography	p. 156
Chapter 8 Model-Based Analysis	p. 157
8.1 Introduction	p. 157
8.2 Model and requirements to be verified	p. 161
8.2.1 The UML-MARTE model that needs to be translated in Fiacre	p. 161
8.2.2 Fiacre language	p. 162
8.2.3 The translation principles of the UML model in Fiacre	p. 163
8.2.4 Requirements	p. 165
8.3 Model-checking of the requirements	p. 166
8.3.1 Use case	p. 166
8.3.2 Properties	p. 167
8.3.3 Property check	p. 170
8.3.4 First assessment	p. 172
8.4 Context exploitation	p. 172
8.4.1 Identifying the context scenarios	p. 173
8.4.2 Automatic partitioning of the context graphs	p. 174
8.4.3 CDL language	p. 175
8.4.4 CDL model exploitation in a model-checker	p. 177
8.4.5 Description of a CDL context	p. 178
8.4.6 Results	p. 179
8.5 Assessment	p. 180
8.6 Conclusion	p. 181
8.7 Bibliography	p. 182
Chapter 9 Model-Based Deployment and Code Generation	p. 185
9.1 Introduction	p. 185
9.2 Input models	p. 187
9.2.1 Description of the executable component-based model	p. 187
9.2.2 Description of the platform model	p. 188
9.2.3 Description of the deployment model	p. 189
9.3 Generation of the implementation model	p. 190
9.3.1 Main concepts	p. 191
9.3.2 Connector pattern	p. 191
9.3.3 Container pattern	p. 193
9.3.4 Implementation of the components	p. 195
9.3.5 Resulting implementation components	p. 197
9.4 Code generation	p. 197
9.4.1 Deployment of the components	p. 198
9.4.2 Transformation into an object-oriented model	p. 199
9.4.3 Generating code	p. 200
9.5 Support tools	p. 201
9.6 Conclusion	p. 202
9.7 Bibliography	p. 202
Part 4 AADL	p. 205
Chapter 10 Presentation of the AADL Concepts	p. 207
10.1 Introduction	p. 207
10.2 General ADL concepts	p. 207
10.3 AADLv2, an ADL for design and analysis	p. 208
10.3.1 A history of the AADL	p. 208
10.3.2 A brief introduction to AADL	p. 209
10.3.3 Tools	p. 211
10.4 Taxonomy of the AADL entities	p. 211
10.4.1 Language elements: the components	p. 212
10.4.2 Connections between the components	p. 214
10.4.3 Language elements: attributes	p. 215
10.4.4 Language elements: extensions and refinements	p. 219
10.5 AADL annexes	p. 220
10.5.1 Data modeling annex	p. 220
10.6 Analysis of AADL models	p. 221
10.6.1 Structural properties	p. 222
10.6.2 Qualitative properties	p. 222
10.6.3 Quantitative properties	p. 223
10.7 Conclusion	p. 224
10.8 Bibliography	p. 225
Chapter 11 Case Study Modeling Using AADL	p. 227
11.1 Introduction	p. 227
11.2 Review of the structure of a pacemaker	p. 229
11.3 AADL modeling of the structure of the pacemaker	p. 230
11.3.1 Decomposition of the system into several subsystems	p. 230
11.3.2 Execution and communication infrastructure	p. 233
11.4 Overview of the functioning of the pacemaker	p. 235
11.4.1 The operational modes of the pacemaker	p. 235
11.4.2 The operational sub-modes of the pacemaker	p. 235
11.4.3 Some functionalities of the pacemaker	p. 237
11.5 AADL modeling of the software architecture of the pulse generator	p. 240
11.5.1 AADL modeling of the operational modes of the pulse generator	p. 240
11.5.2 AADL modeling of the features of the pulse generator in the permanent mode	p. 242
11.6 Modeling of the deployment of the pacemaker	p. 247
11.7 Conclusion	p. 249
11.8 Bibliography	p. 250
Chapter 12 Model-Based Analysis	p. 251
12.1 Introduction	p. 251
12.2 Behavioral validation, per mode and global	p. 252
12.2.1 Validation context and fine toning of the requirements	p. 253
12.2.2 Translation of the behavioral automata into UPPAAL	p. 253
12.2.3 Refining requirements 22-23/P	p. 258
12.2.4 Study of the permanent/VVT mode	p. 260
12.2.5 Study of the changing of the permanent/VVT→Magnet/VOO mode	p. 261
12.3 Conclusion	p. 262
12.4 Bibliography	p. 263
Chapter 13 Model-Based Code Generation	p. 265
13.1 Introduction	p. 265
13.2 Software component generation	p. 268
13.2.1 Data conversion	p. 269
13.2.2 Conversion of subprograms	p. 272
13.2.3 Conversion of execution threads	p. 275
13.2.4 Conversion of the instances of shared data	p. 283
13.3 Middleware components generation	p. 283
13.4 Configuration and deployment of middleware components	p. 284
13.4.1 Deployment	p. 284
13.5 Integration of the compilation chain	p. 285
13.6 Conclusion	p. 287
13.7 Bibliography	p. 287
List of Authors	p. 289
Index	p. 291

Available:*

On Order

Summary

Summary

Author Notes

Table of Contents