Embedded Systems

Analysis and Modeling with SysML, UML and AADL

Inbunden, Engelska, 2013

Av Fabrice Kordon, Jérôme Hugues, Agusti Canals, Alain Dohet, France) Kordon, Fabrice (UPMC, Paris, France) Hugues, Jerome (ISAE, Toulouse, France) Canals, Agusti (Paul Sabatier University, Toulouse, France) Dohet, Alain (DGA, French Defense Ministry

2 449 kr

Beställningsvara. Skickas inom 11-20 vardagar

Fri frakt för medlemmar vid köp för minst 249 kr.

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.

Produktinformation

Utgivningsdatum2013-04-16
Mått163 x 241 x 22 mm
Vikt612 g
FormatInbunden
SpråkEngelska
Antal sidor320
FörlagISTE Ltd and John Wiley & Sons Inc
ISBN9781848215009

Tillhör följande kategorier

Fabrice Kordon is Professor at University Pierre and Marie Curie in Paris, France, where he is in charge of the team "Modélisation et vérification" of the LIP6. His research field is at the crossroads of distributed systems, software engineering and formal methods.Jérôme Hugues is lecturer-researcher at the Institut Supérieur de l’Aéronautique et de l'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 Systèmes" 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 Générale pour l'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.

Foreword xiiiBrian R. LARSONForeword xvDominique POTIERIntroduction xixFabrice KORDON, Jérôme HUGUES, Agusti CANALS and Alain DOHETPART 1. General Concepts 1Chapter 1. Elements for the Design of Embedded Computer Systems 3Fabrice KORDON, Jérôme HUGUES, Agusti CANALS and Alain DOHET1.1. Introduction 31.2. System modeling 51.3. A brief presentation of UML 61.3.1. The UML static diagrams 71.3.2. The UML dynamic diagrams 91.4. Model-driven development approaches 101.4.1. The concepts 101.4.2. The technologies 111.4.3. The context of the wider field 121.5. System analysis 141.5.1. Formal verification via proving 151.5.2. Formal verification by model-checking 151.5.3. The languages to express specifications 161.5.4. The actual limits of formal approaches 191.6. Methodological aspects of the development of embedded computer systems 201.6.1. The main technical processes 221.6.2. The importance of the models 231.7. Conclusion 241.8. Bibliography 25Chapter 2. Case Study: Pacemaker 29Fabrice KORDON, Jérôme HUGUES, Agusti CANALS and Alain DOHET2.1. Introduction 292.2. The heart and the pacemaker 302.2.1. The heart 302.2.2. Presentation of a pacemaker 322.3. Case study specification 332.3.1. System definition 342.3.2. System lifecycle 352.3.3. System requirements 362.3.4. Pacemaker behavior 392.4. Conclusion 422.5. Bibliography 43PART 2. SysML 45Chapter 3. Presentation of SysML Concepts 47Jean-Michel BRUEL and Pascal ROQUES3.1. Introduction 473.2. The origins of SysML 483.3. General overview: the nine types of diagrams 493.4. Modeling the requirements 503.4.1. Use case diagram 503.4.2. Requirement diagram 513.5. Structural modeling 533.5.1. Block definition diagram 543.5.2. Internal block diagram 563.5.3. Package diagram 583.6. Dynamic modeling 593.6.1. Sequence diagram 593.6.2. State machine diagram 613.6.3. Activity diagram 633.7. Transverse modeling 653.7.1. Parametric diagram 653.7.2. Allocation and traceability 673.8. Environment and tools 683.9. Conclusion 683.10. Bibliography 68Chapter 4. Modeling of the Case Study Using SysML 71Loïc FEJOZ, Philippe LEBLANC and Agusti CANALS4.1. Introduction 714.2. System specification 734.2.1. Context 734.2.2. Requirements model and operational scenarios 754.2.3. Requirements model 784.3. System design 804.3.1. Functional model 814.3.2. Domain-specific data 834.3.3. Logical architectural model 864.3.4. Physical architectural model 904.4. Traceability and allocations 904.4.1. “Technical needs: divers” traceability diagram 904.4.2. Traceability diagram “technical needs: behavior of the pacemaker” 914.4.3. Allocation diagram 924.5. Test model 934.5.1. Traceability diagram “system test: requirements verification” 934.5.2. Sequence diagram for the test game TC-PM-07 944.5.3. Diagrams presenting a general view of the requirements 944.6. Conclusion 954.7. Bibliography 97Chapter 5. Requirements Analysis 99Ludovic APVRILLE and Pierre DE SAQUI-SANNES5.1. Introduction 995.2. The AVATAR language and the TTool tool 1005.2.1. Method 1015.2.2. AVATAR language and SysML standard 1015.2.3. The TEPE language for expressing properties 1025.2.4. TTool 1035.3. An AVATAR expression of the SysML model of the enhanced pacemaker 1035.3.1. Functioning of the pacemaker and modeling hypotheses 1035.3.2. Requirements diagram 1045.4. Architecture 1055.5. Behavior 1065.6. Formal verification of the VVI mode 1075.6.1. General properties 1085.6.2. Expressing properties using TEPE 1085.6.3. The use of temporal logic 1095.6.4. Observer-guided verification 1115.6.5. Coming back to the model 1125.7. Related work 1135.7.1. Languages 1135.7.2. Tools 1145.8. Conclusion 1155.9. Appendix: TTool 1165.10. Bibliography 116PART 3. MARTE 119Chapter 6. An Introduction to MARTE Concepts 121Sébastien GÉRARD and François TERRIER6.1. Introduction 1216.2. General remarks 1216.2.1. Possible uses of MARTE 1226.2.2. How should we read the norm? 1236.2.3. The MARTE architecture 1246.2.4. MARTE and SysML 1276.2.5. An open source support 1286.3. Several MARTE details 1286.3.1. Modeling non-functional properties 1286.3.2. A components model for the real-time embedded system 1336.4. Conclusion 1376.5. Bibliography 137Chapter 7. Case Study Modeling Using MARTE 139Jérôme DELATOUR and Joël CHAMPEAU7.1. Introduction 1397.1.1. Hypotheses used in modeling 1397.1.2. The modeling methodology used 1407.1.3. Chapter layout 1417.2. Software analysis 1417.2.1. Use case and interface characterization 1417.2.2. The sphere of application 1447.3. Preliminary software design – the architectural component 1457.3.1. The candidate architecture 1467.3.2. Identifying the components 1467.3.3. Presentation of the candidate architecture 1487.3.4. A presentation of the detailed interfaces 1507.4. Software preliminary design – behavioral component 1517.4.1. The controller 1517.4.2. The cardiologist 1537.4.3. The operating modes of the cardiologist 1537.5. Conclusion 1557.6. Bibliography 156Chapter 8. Model-Based Analysis 157Frederic BONIOL, Philippe DHAUSSY, Luka LE ROUX and Jean-Charles ROGER8.1. Introduction 1578.2. Model and requirements to be verified 1618.2.1. The UML-MARTE model that needs to be translated in Fiacre 1618.2.2. Fiacre language 1628.2.3. The translation principles of the UML model in Fiacre 1638.2.4. Requirements 1658.3. Model-checking of the requirements 1668.3.1. Use case 1668.3.2. Properties 1678.3.3. Property check 1708.3.4. First assessment 1728.4. Context exploitation 1728.4.1. Identifying the context scenarios 1738.4.2. Automatic partitioning of the context graphs 1748.4.3. CDL language 1758.4.4. CDL model exploitation in a model-checker 1778.4.5. Description of a CDL context 1788.4.6. Results 1798.5. Assessment 1808.6. Conclusion 1818.7. Bibliography 182Chapter 9. Model-Based Deployment and Code Generation 185Chokri MRAIDHA, Ansgar RADERMACHER and Sébastien GÉRARD9.1. Introduction 1859.2. Input models 1879.2.1. Description of the executable component-based model 1879.2.2. Description of the platform model 1889.2.3. Description of the deployment model 1899.3. Generation of the implementation model 1909.3.1. Main concepts 1919.3.2. Connector pattern 1919.3.3. Container pattern 1939.3.4. Implementation of the components 1959.3.5. Resulting implementation components 1979.4. Code generation 1979.4.1. Deployment of the components 1989.4.2. Transformation into an object-oriented model 1999.4.3. Generating code 2009.5. Support tools 2019.6. Conclusion 2029.7. Bibliography 202PART 4. AADL 205Chapter 10. Presentation of the AADL Concepts 207Jérôme HUGUES and Xavier RENAULT10.1. Introduction 20710.2. General ADL concepts 20710.3. AADLv2, an ADL for design and analysis 20810.3.1. A history of the AADL 20810.3.2. A brief introduction to AADL 20910.3.3. Tools 21110.4. Taxonomy of the AADL entities 21110.4.1. Language elements: the components 21210.4.2. Connections between the components 21410.4.3. Language elements: attributes 21510.4.4. Language elements: extensions and refinements 21910.5. AADL annexes 22010.5.1. Data modeling annex 22010.6. Analysis of AADL models 22110.6.1. Structural properties 22210.6.2. Qualitative properties 22210.6.3. Quantitative properties 22310.7. Conclusion 22410.8. Bibliography 225Chapter 11. Case Study Modeling Using AADL 227Etienne BORDE11.1. Introduction 22711.2. Review of the structure of a pacemaker 22911.3. AADL modeling of the structure of the pacemaker 23011.3.1. Decomposition of the system into several subsystems 23011.3.2. Execution and communication infrastructure 23311.4. Overview of the functioning of the pacemaker 23511.4.1. The operational modes of the pacemaker 23511.4.2. The operational sub-modes of the pacemaker 23511.4.3. Some functionalities of the pacemaker 23711.5. AADL modeling of the software architecture of the pulse generator 24011.5.1. AADL modeling of the operational modes of the pulse generator 24011.5.2. AADL modeling of the features of the pulse generator in the permanent mode 24211.6. Modeling of the deployment of the pacemaker 24711.7. Conclusion 24911.8. Bibliography 250Chapter 12. Model-Based Analysis 251Thomas ROBERT and Jérôme HUGUES12.1. Introduction 25112.2. Behavioral validation, per mode and global 25212.2.1. Validation context and fine tuning of the requirements 25312.2.2. Translation of the behavioral automata into UPPAAL 25312.2.3. Refining requirements 22-23/P 25812.2.4. Study of the permanent/VVT mode 26012.2.5. Study of the changing of the permanent/VVT→Magnet/VOO mode 26112.3. Conclusion 26212.4. Bibliography 263Chapter 13. Model-Based Code Generation 265Laurent PAUTET and Béchir ZALILA13.1. Introduction 26513.2. Software component generation 26813.2.1. Data conversion 26913.2.2. Conversion of subprograms 27213.2.3. Conversion of execution threads 27513.2.4. Conversion of the instances of shared data 28313.3. Middleware components generation 28313.4. Configuration and deployment of middleware components 28413.4.1. Deployment 28413.5. Integration of the compilation chain 28513.6. Conclusion 28713.7. Bibliography 287List of Authors 289Index 291