Grimm Languages for System Specification

Selected Contributions on UML, SystemC, System Verilog, Mixed-Signal Systems, and Property Specification from FDL'03
1. Auflage 2007
ISBN: 978-1-4020-7991-7
Verlag: Springer US
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 353 Seiten

Contributions on UML address the application of UML in the specification of embedded HW/SW systems. C-Based System Design embraces the modeling of operating systems, modeling with different models of computation, generation of test patterns, and experiences from case studies with SystemC. Analog and Mixed-Signal Systems covers rules for solving general modeling problems in VHDL-AMS, modeling of multi-nature systems, synthesis, and modeling of Mixed-Signal Systems with SystemC.

Languages for formal methods are addressed by contributions on formal specification and refinement of hybrid, embedded and real-time stems. Together with articles on new languages such as SystemVerilog and Software Engineering in Automotive Systems the contributions selected for this book embrace all aspects of languages and models for specification, design, modeling and verification of systems. Therefore, the book gives an excellent overview of the actual state-of-the-art and the latest research results.

Written for:
Researchers, scientists

Autoren/Hrsg.

Grimm, Christoph

Inhaltsverzeichnis

1;Contents;5
2;Preface;8
3;I UML-BASED SYSTEM SPECIFICATION & DESIGN;10
3.1;Chapter 1 UML-BASED CO-DESIGN FOR RUN-TIME RECONFIGURABLE ARCHITECTURES;13
3.1.1;1. Introduction;13
3.1.2;2. UML-Based Co-Design Approach;15
3.1.2.1;2.1 Motivation;15
3.1.2.2;2.2 Activities and Artifacts;16
3.1.3;3. System Specification;17
3.1.3.1;3.1 Platform Independent Model;17
3.1.3.2;3.2 MOCCA Action Language;18
3.1.4;4. Platform Mapping;19
3.1.4.1;4.1 Activities and Artifacts;19
3.1.4.2;4.2 Target Platform Model;20
3.1.4.3;4.3 Hardware Platform Mapping;20
3.1.4.4;4.4 Software Platform Mapping;23
3.1.5;5. Synthesis;24
3.1.6;6. Conclusions and Future Work;25
3.1.7;References;26
3.2;Chapter 2 A UNIFIED APPROACH TO CODE GENERATION FROM BEHAVIORAL DIAGRAMS;28
3.2.1;1. Introduction;28
3.2.2;2. The Rialto Intermediate Language;30
3.2.2.1;2.1 Syntax;30
3.2.2.2;2.2 Operational Semantics;32
3.2.2.3;2.3 Scheduling Semantics;33
3.2.3;3. Representing UML models in Rialto;34
3.2.3.1;3.1 Statecharts;34
3.2.3.2;3.2 Activity Diagrams;36
3.2.3.3;3.3 Collaboration Diagrams;36
3.2.3.4;3.4 Automatic UML to Rialto Translation;38
3.2.4;4. Animation and Code generation;39
3.2.5;5. Conclusions;40
3.2.6;References;40
3.3;Chapter 3 PLATFORM-INDEPENDENT DESIGN FOR EMBEDDED REAL-TIME SYSTEMS;42
3.3.1;1. Introduction;43
3.3.2;2. The Dream: Platform-Independent Design;44
3.3.3;3. Comparison of several design approaches for embedded RT systems;46
3.3.3.1;3.1 Expressive power;47
3.3.3.2;3.2 Platform-independent semantics;47
3.3.3.3;3.3 Modularity support;48
3.3.3.4;3.4 Correctness-preserving transformation;49
3.3.4;4. Towards Platform-independent Design;51
3.3.4.1;4.1 POOSL;52
3.3.4.2;4.2 Rotalumis;52
3.3.5;5. Conclusions;54
3.3.6;Notes;55
3.3.7;References;55
3.4;Chapter 4 REAL-TIME SYSTEM MODELING WITH ACCORD/UML METHODOLOGY;58
3.4.1;1. Introduction;58
3.4.2;2. Case study;60
3.4.3;3. Preliminary Analysis Model (PAM);61
3.4.4;4. Detailed Analysis Model (DAM);66
3.4.5;5. Validation by Prototyping (PrM) and Testing (TeM);73
3.4.6;6. Conclusion and ongoing research projects;74
3.4.7;References;76
3.5;Chapter 5 UML-BASED SPECIFICATIONS OF AN EMBEDDED SYSTEM ORIENTED TO HW/SW PARTITIONING;78
3.5.1;1. Introduction;78
3.5.2;2. Why Hardware and Software Co-design starting from UML;79
3.5.3;3. Case Study: Problem description;81
3.5.3.1;3.1 Objective;81
3.5.3.2;3.2 The operational scenario;81
3.5.3.3;3.3 The project constraints;83
3.5.4;4. WMR System-level Specification with UML;84
3.5.4.1;4.1 Use Case diagrams;84
3.5.4.2;4.2 Sequence Diagrams;85
3.5.4.3;4.3 Object Model Diagram;87
3.5.5;5. UML-based Hardware and Software Partitioning Approach;88
3.5.5.1;5.1 STEP 1: Assign the "Partitionable" stereotype to desired objects, object types and packages;88
3.5.5.2;5.2 STEP 2: Assign parameter’s constraints;89
3.5.5.3;5.3 STEP 3: Parse the UML saved files;89
3.5.5.4;5.4 STEP 4: Assign parameters to components from a repository or attribute parameters by hand;90
3.5.5.5;5.5 STEP 5: Decide cost function to give weights to parameters;90
3.5.5.6;5.6 STEP 6: Run the partitioning tool;90
3.5.6;6. Concluding Remarks;90
3.5.7;References;91
4;II C-BASED SYSTEM DESIGN;92
4.1;Chapter 6 SPACE: A HARDWARE/SOFTWARE SYSTEMC MODELING PLATFORM INCLUDING AN RTOS;96
4.1.1;1. Introduction;96
4.1.2;2. RelatedWorks and objectives;98
4.1.3;3. SPACE and its methodology;100
4.1.4;4. Embedded Software environment;101
4.1.4.1;4.1 SystemC API;102
4.1.4.2;4.2 The RTOS;103
4.1.5;5. Hardware support;103
4.1.5.1;5.1 Abstraction level;103
4.1.5.2;5.2 UTF Channel;104
4.1.5.3;5.3 TF Channel;104
4.1.6;6. An example and its simulation results;106
4.1.7;7. Conclusion and future works;107
4.1.8;References;108
4.2;Chapter 7 LAERTE++: AN OBJECT ORIENTED HIGH-LEVEL TPG FOR SYSTEMC DESIGNS;110
4.2.1;1. Introduction;110
4.2.2;2. Laerte++ Philosophy;112
4.2.2.1;2.1 Laerte++ architecture;113
4.2.2.2;2.2 Testing procedure set-up;113
4.2.2.3;2.3 Additional features;114
4.2.3;3. Fault Injector;115
4.2.4;3.1 Definition of new fault models;115
4.2.5;4. TPG Engine;116
4.2.6;5. Applicability Example;120
4.2.7;6. Concluding Remarks;121
4.2.8;References;121
4.3;Chapter 8 A CASE STUDY: SYSTEMC-BASED DESIGN OF AN INDUSTRIAL EXPOSURE CONTROL UNIT;123
4.3.1;1. Introduction;124
4.3.2;2. Exposure Control Unit;125
4.3.3;3. SystemC Modeling and Refinement Process;127
4.3.4;4. Automated Fixed-Point to Integer Conversion;132
4.3.5;5. Experimental Results and Experiences;134
4.3.6;6. Conclusion;135
4.3.7;References;136
4.4;Chapter 9 MODELING OF CSP, KPN AND SR SYSTEMS WITH SYSTEMC;137
4.4.1;Introduction;137
4.4.2;1. Embedded system speci.cation in SystemC;139
4.4.2.1;1.1 Specification Structure;139
4.4.2.2;1.2 System specification;140
4.4.3;2. Modeling of CSP, KPN and SR systems;143
4.4.3.1;2.1 Modeling of CSP systems;143
4.4.3.2;2.2 Modeling of KPN systems;146
4.4.3.3;2.3 Modeling of SR systems;148
4.4.4;3. Conclusions;150
4.4.5;References;151
4.5;Chapter 10 ON HARDWARE DESCRIPTION IN ECL;153
4.5.1;1. Introduction;153
4.5.2;2. Overview of ECL;156
4.5.3;3. HW/SW Co-Design Flow with ECL;156
4.5.3.1;3.1 Specification and Refinement;157
4.5.3.2;3.2 Hardware Synthesis;159
4.5.4;4. Case Study: A Simple Processor;161
4.5.4.1;4.1 Processor Description;161
4.5.4.2;4.2 ECL Module Structure;162
4.5.4.3;4.3 Processor Synthesis Results;164
4.5.5;5. Conclusion;164
4.5.6;References;166
5;III ANALOG AND MIXED-SIGNAL SYSTEMS;167
5.1;Chapter 11 RULES FOR ANALOG AND MIXED-SIGNAL VHDL-AMS MODELING;171
5.1.1;1. Introduction;171
5.1.2;2. Simulation problem;172
5.1.2.1;2.1 Elaboration of the analog part;172
5.1.2.2;2.2 Characterization of solutions;174
5.1.3;3. Modeling rules;176
5.1.3.1;3.1 General rules;176
5.1.3.2;3.2 Initialization phase;177
5.1.3.3;3.3 Time domain simulation;180
5.1.3.4;3.4 Rules for mixed-signal models;181
5.1.4;4. Conclusion;183
5.1.5;References;183
5.2;Chapter 12 A VHDL-AMS LIBRARY OF HIERARCHICAL OPTOELECTRONIC DEVICE MODELS;185
5.2.1;Introduction;185
5.2.2;1. FromWAN to SAN;186
5.2.3;2. CAD tools for optoelectronic systems;186
5.2.3.1;2.1 Behavioral modelling;187
5.2.4;3. A hierarchical library;188
5.2.5;4. Optoelectronic devices;188
5.2.5.1;4.1 Laser and MQW laser;188
5.2.5.2;4.2 Vertical Cavity Surface Emitting Laser : VCSEL;190
5.2.5.3;4.3 The optical fiber;192
5.2.5.4;4.4 The PIN photodiode;195
5.2.6;5. An optical link;196
5.2.6.1;5.1 Simulation results;197
5.2.6.2;5.2 Exploiting results;197
5.2.7;6. Conclusion and perspectives;198
5.2.7.1;6.1 Library development;199
5.2.7.2;6.2 VHDL-AMS limitations;199
5.2.7.3;6.3 Methodology conclusion;199
5.2.8;References;200
5.3;Chapter 13 TOWARDS HIGH-LEVEL ANALOG AND MIXED-SIGNAL SYNTHESIS FROM VHDL-AMS SPECIFICATIONS;202
5.3.1;1. Introduction;202
5.3.2;2. VHDL-AMS Subset for Synthesis;205
5.3.3;3. High-Level Analog Synthesis;207
5.3.4;3.1 Tile Representation;209
5.3.5;4. Case Study;212
5.3.6;5. Conclusion;214
5.3.7;References;215
5.4;Chapter 14 RELIABILITY SIMULATION OF ELECTRONIC CIRCUITS WITH VHDL-AMS;218
5.4.1;1. Introduction;218
5.4.2;2. A degradation mechanism: hot carrier degradations;219
5.4.3;3. The reliability simulation today;220
5.4.4;4. Behavioural modelling for ageing simulation;222
5.4.5;5. Construction of the behavioural ageing model of a circuit;224
5.4.6;5.1 Organisation of the behavioural ageing model;224
5.4.7;5.2 Principle of the construction of the degradation model of circuit;225
5.4.8;5.3 Bias conditions analysis;225
5.4.9;5.4 The transistor ageing model;225
5.4.10;5.5 Sensitivity analysis;226
5.4.11;5.6 An OTA ageing behavioural model;228
5.4.12;5.7 Using the model for simulation;228
5.4.13;6. Conclusion;228
5.4.14;References;229
5.5;Chapter 15 EXTENDING SYSTEMC TO ANALOG MODELLING AND SIMULATION;230
5.5.1;1. Introduction;230
5.5.2;2. Description of Analog Modules in SystemC;231
5.5.3;3. Application Examples;236
5.5.3.1;3.1 RF transceiver;236
5.5.3.2;3.2 Mixed-Signal Fuzzy Controller;239
5.5.4;4. Conclusion;242
5.5.5;References;243
6;IV LANGUAGES FOR FORMAL METHODS;244
6.1;Chapter 16 LINKING ARCHITECTURAL AND COMPONENT LEVEL SYSTEM VIEWS BY ABSTRACT STATE MACHINES;247
6.1.1;1. Introduction;247
6.1.2;2. Relating high-level and component-level system views;249
6.1.2.1;2.1 The language of ASMs;250
6.1.2.2;2.2 Navigation between levels of detail;254
6.1.3;3. Submachine-based component concept;258
6.1.3.1;3.1 Operators for the Composition of Components;259
6.1.3.2;3.2 Speci.c ASM component concepts;262
6.1.3.3;3.3 Componentwise system development: an example;263
6.1.4;4. Conclusion;265
6.1.5;Notes;265
6.1.6;References;265
6.2;Chapter 17 A NEW TIME EXTENSION TO ?-CALCULUS BASED ON TIME CONSUMING TRANSITION SEMANTICS;270
6.2.1;1. Introduction;270
6.2.2;2. RelatedWork;271
6.2.3;3. Brief introduction to calculus;272
6.2.4;4. Time Consuming Transitions;273
6.2.5;5. Temporal properties of TLTS;278
6.2.6;6. Conclusion and Future Work;280
6.2.7;Notes;281
6.2.8;References;281
6.3;Chapter 18 MODELING CHP DESCRIPTIONS IN LABELED TRANSITIONS SYSTEMS FOR AN EFFICIENT FORMAL VALIDATION OF ASYNCHRONOUS CIRCUIT SPECIFICATIONS;283
6.3.1;1. Introduction;283
6.3.2;2. Translation from CHP to Petri Nets and IF;286
6.3.2.1;2.1 The Petri Nets and IF models;286
6.3.2.2;2.2 CHP components;287
6.3.2.3;2.3 CHP processes;288
6.3.2.4;2.4 Inter-process communications and probes;289
6.3.2.5;2.5 Optimizations;290
6.3.3;3. Performance study;291
6.3.4;4. Case study: a four-tap FIR Filter;295
6.3.4.1;4.1 Modeling the Filter in IF;295
6.3.4.2;4.2 Some verified properties;295
6.3.4.3;4.3 Verification by behavior reduction;296
6.3.4.4;4.4 Handling state explosion;297
6.3.5;5. Conclusion;297
6.3.6;References;297
6.4;Chapter 19 COMBINED FORMAL REFINEMENT AND MODEL CHECKING FOR REAL-TIME SYSTEMS VERIFICATION;299
6.4.1;1. Introduction;299
6.4.2;2. RelatedWork;300
6.4.3;3. Real-Time Model Checking with RAVEN;301
6.4.4;4. Refinement with B;302
6.4.5;5. Combined Model Checking and Refinement;303
6.4.5.1;5.1 The Echo Cancellation Unit;305
6.4.5.2;5.2 RIL Code Generation;306
6.4.5.3;5.3 B Generation;307
6.4.5.4;5.4 RIL Refinement;308
6.4.5.5;5.5 BT Generation;309
6.4.5.6;5.6 BT Refinement and C Code Generation;310
6.4.6;6. Experimental Results;310
6.4.7;7. Conclusions;311
6.4.8;References;312
6.5;Chapter 20 REFINEMENT OF HYBRID SYSTEMS;313
6.5.1;1. Introduction;313
6.5.2;2. HyCharts;316
6.5.3;3. Modeling Hybrid Control Systems with SystemC;322
6.5.4;4. Translation of discrete HyCharts to SystemC;324
6.5.5;5. Conclusion and Future Work;327
6.5.6;References;327
7;V APPLICATIONS AND NEW LANGUAGES;329
7.1;Chapter 21 AUTOMOTIVE SOFTWARE ENGINEERING;330
7.1.1;1. Introduction;330
7.1.2;2. Characteristics of Automotive Software Engineering;331
7.1.2.1;2.1 Observable Symptoms;332
7.1.2.2;2.2 Main Characteristics of ASE;335
7.1.3;3. The Demands for an Automotive Software Engineering Discipline;336
7.1.3.1;3.1 Process Paradigm;336
7.1.3.2;3.2 Requirements Engineering;337
7.1.3.3;3.3 Software Architecture & Design;338
7.1.3.4;3.4 Specification;340
7.1.3.5;3.5 Implementation;341
7.1.3.6;3.6 Test;341
7.1.3.7;3.7 Maintenance;342
7.1.4;4. Conclusion;343
7.1.5;References;343
7.2;Chapter 22 SYSTEMVERILOG;345
7.2.1;1. Introduction;345
7.2.2;2. Features of SystemVerilog;349
7.2.3;3. Challenges;351
7.2.4;4. Summary;353
7.2.5;Bibliography and Resources;353
8;More eBooks at www.ciando.com;0