Synthesis of Embedded Software (eBook)

Introduction 5
Contents 10
Contributors 12
Acronyms 14
Chapter 1:Compilation of Polychronous Data Flow Equations 15
1.1 Introduction 15
1.2 Signal Language 17
1.2.1 Synchronized Data Flow 18
1.2.2 Signal, Execution, Process in Signal 18
1.2.3 Signal Data Types 19
1.2.4 Signal Elementary Processes 20
1.2.5 Signal Process Operators 22
1.2.6 Parallel Semantic Properties of Signal 23
1.3 Example 24
1.3.1 Signal Modularity Features 25
1.3.2 Full Example with Time Refinement 26
1.4 Formal Context for Code Generation 27
1.4.1 Endochronous Acyclic Process 28
1.4.2 Signal Graph Expressions 29
1.4.3 Synchronization Relation 30
1.4.3.1 Clock Hierarchy 31
1.4.3.2 ``Endochronization' 32
1.4.4 Precedence Relation 32
1.4.4.1 Path Algebra -3mu 32
1.4.4.2 Precedence Refinement 33
1.4.5 Data Control Graph 34
1.4.6 Signal Process Abstraction 34
1.4.7 Clustering 35
1.4.7.1 Data Flow Execution 36
1.4.7.2 Data Clustering 36
1.4.7.3 Phylum 36
1.4.7.4 From Cluster to Scheduling of Actions 37
1.4.8 Building Containers 38
1.5 Code Generation in Polychrony Toolset 39
1.5.1 Code Generation Principle 39
1.5.1.1 Step Function 40
1.5.1.2 IO Container 40
1.5.1.3 Main Program 41
1.5.2 Sequential Code Generation 41
1.5.3 Clustered Code Generation with Static Scheduling 43
1.5.4 Clustered Code Generation with Dynamic Scheduling 44
1.5.5 Modular Code Generation 45
1.5.5.1 Sequential Code Generation for Modular Compilation 46
1.5.5.2 Clustered Code Generation for Modular Compilation 47
1.5.6 Distributed Code Generation 48
1.5.6.1 Topological Annotations 49
1.5.6.2 Communication Annotations 49
1.5.6.3 IO Code Generation 50
1.6 Conclusion 51
References 53
Chapter 2: Formal Modeling of Embedded Systems with Explicit Schedules and Routes 55
2.1 General Presentation 56
2.1.1 Process Networks 56
2.1.2 Pure Dataflow 57
2.1.3 Static Control Preserving Conflict-Freeness 58
2.1.4 Example 59
2.2 Pure Dataflow MoCCs 60
2.2.1 Synchrony 60
2.2.2 Latency-Insensitive Design 62
2.2.3 Marked Graphs 63
2.2.3.1 Static Schedulability and Throughput 65
2.2.3.2 Timed Marked Graphs 66
2.2.3.3 Bounded Capacities on Places 66
2.2.3.4 Place Sizing 68
2.2.3.5 Equalization 69
2.2.4 Synchronous Data Flow 70
2.3 Statically Controlled MoCCs 72
2.3.1 Cyclo-Static Dataflow Graphs 73
2.3.2 K-Periodically Routed Graphs 74
2.3.2.1 Buffer Boundedness Check 76
2.3.2.2 Deadlock-Freedom Check 77
2.3.2.3 Static Schedulability and Throughput 77
2.3.2.4 Dependency Analysis 78
2.3.2.5 Topological Transformations 83
2.4 Conclusion 88
References 89
Chapter 3: Synoptic: A Domain-Specific Modeling Language for Space On-board Application Software 93
3.1 Introduction 93
3.1.1 Context: Embedded Flight Software 93
3.1.2 Domain Specific Requirements 96
3.1.3 Synoptic: A Domain Specific Design Environment 99
3.2 Synoptic: A Domain Specific Modeling Language for Aerospace Systems 101
3.2.1 Synoptic Overview 101
3.2.2 Software Architecture Models 103
3.2.2.1 Block Diagram: Dataflow, Automaton and External Blocks 103
3.2.2.2 Synchronous Islands 107
3.2.2.3 Control and Temporal Properties 108
3.2.2.4 Properties Specification 109
3.2.3 Synoptic Components: Genericity and Modularity 110
3.2.4 Incremental Design and Refinement Features 111
3.3 Semantic and Model of Computation of synoptic Models 113
3.3.1 An Introduction to SIGNAL 113
3.3.2 Interpretation of Blocks 114
3.3.3 Interpretation of Dataflow 114
3.3.4 Interpretation of Actions 116
3.3.5 Interpretation of Automata 118
3.3.6 The Polychronous Model of Computation 121
3.4 Middleware Aspect 124
3.4.1 Architecture of the Execution Platform 125
3.4.2 The Middleware Kernel and External Variables 127
3.4.3 Reconfiguration Service 128
3.5 Conclusion 130
References 132
Chapter 4: Compiling SHIM 134
4.1 Introduction 134
4.2 Shim with Processes and Networks 136
4.3 Tail-Recursive Code Generation 137
4.4 Code Generation from Static Schedules 140
4.5 Shim with Functions, Recursion, and Exceptions 145
4.5.1 Recursion 146
4.5.2 Exceptions 148
4.6 Generating Threaded Code 149
4.6.1 An Example 150
4.6.2 The Static Call-Graph Assumption 150
4.6.3 Implementing Rendezvous Communication 151
4.6.4 Starting and Terminating Tasks 152
4.7 Detecting Deadlocks 154
4.8 Sharing Buffers 156
4.9 Conclusions 156
References 158
Chapter 5: A Module Language for Typing SIGNAL Programsby Contracts 160
5.1 Introduction 160
5.2 A Case Study 162
5.2.1 Description of the Protocol 162
5.2.2 Introduction to the Module Language 164
5.3 An Algebra of Contracts for Assume-Guarantee Reasoning 165
5.3.1 An Algebra of Processes 165
5.3.2 An Algebra of Filters 168
5.3.3 An Algebra of Contracts 169
5.3.4 Contracts: Some Related Approaches 171
5.4 A Module Language for Typing by Contracts 173
5.4.1 Syntax 173
5.4.2 A Type System for Contracts and Processes 174
5.4.3 Subtyping as Refinement 174
5.4.4 Composition of Modules 175
5.5 Application to SIGNAL 176
5.5.1 Implementation of the LTTA 176
5.5.2 Contracts in SIGNAL 178
5.5.3 Salient Properties of Contracts in the Synchronous Context 180
5.5.4 Implementation 182
5.6 Conclusion 182
References 183
Chapter 6: MRICDF: A Polychronous Model for Embedded Software Synthesis 185
6.1 Introduction 185
6.1.1 Motivation for Polychronous Formalism 186
6.1.2 Software Synthesis from Polychronous Formalism 188
6.2 Synchronous Structure Preliminaries 189
6.3 MRICDF Actor Network Model 190
6.3.1 Primitive and Composite Actors for MRICDF 191
6.4 Embedded Software Synthesis from MRICDF 193
6.4.1 Issues in the Transformation from MRICDF Models to Embedded Software 194
6.4.2 Epoch Analysis: Determining Sequential Implementability of MRICDF Models 195
6.4.2.1 Deadlock Detection 195
6.4.2.2 Master Trigger Identification 196
6.4.2.3 Exogenous Constraints for Code Synthesis 197
6.4.3 Case Study of Producer--Consumer Problem 198
6.5 Visual Framework for Code Synthesis from MRICDF Specification 200
6.5.1 Prime Implicates for Master Trigger Computation 201
6.5.2 Sequential Implementability of Multi-rate Specification Using Prime Implicates 202
6.5.2.1 Endochronous Primitive Actors: Buffer and Function 202
6.5.2.2 Non-endochronous Primitive Actors: Sampler and Merge 203
6.5.3 Sequential Code Synthesis 205
6.5.4 Case Study on Implementation of an MRICDF Model using EmCodeSyn 206
6.6 Conclusions and Future Direction 209
References 210
Chapter 7: The Time Model of Logical Clocks Available in the OMG MARTE Profile 212
7.1 Introduction 212
7.2 The UML Profile for MARTE 215
7.2.1 Overview 215
7.2.2 The Time Profile 216
7.3 CCSL Time Model 218
7.3.1 The Clock Constraint Specification Language 218
7.3.1.1 Instant Relations 218
7.3.1.2 Clock Relations 218
7.3.1.3 Clock Expressions 219
7.3.1.4 Clock Constraints 219
7.3.1.5 Temporal Evolutions 219
7.3.1.6 CCSL Libraries 220
7.3.2 TimeSquare 220
7.3.2.1 Summary 220
7.4 MARTE and East-ADL2 221
7.4.1 East-ADL2 221
7.4.1.1 Timing Requirements 221
7.4.1.2 Example 222
7.4.2 A CCSL Library for East-ADL 222
7.4.2.1 Applying the UML Profile for MARTE 223
7.4.2.2 Repetition Rate 223
7.4.2.3 Delay Requirements 224
7.4.3 Analysis of East-ADL Specification 225
7.5 MARTE and AADL 226
7.5.1 AADL 226
7.5.1.1 Modeling Elements 226
7.5.1.2 AADL Application Software Components 227
7.5.1.3 AADL Flows 227
7.5.1.4 AADL Ports 228
7.5.2 Describing AADL Models with MARTE 229
7.5.2.1 AADL Flows with MARTE 229
7.5.2.2 Five Aperiodic Tasks 230
7.5.2.3 Mixing Periodic and Aperiodic Tasks 231
7.6 MARTE and SDF 232
7.6.1 Synchronous Data Flow 233
7.6.2 A CCSL Library for SDF 233
7.6.2.1 Actors 234
7.6.2.2 Tokens 234
7.6.2.3 Inputs 234
7.6.2.4 Outputs 235
7.6.2.5 Arcs 235
7.6.3 Applying the SDF Semantics 235
7.7 Conclusion 237
References 237
Chapter 8: From Synchronous Specifications to Statically Scheduled Hard Real-Time Implementations 239
8.1 Introduction 239
8.2 The Synchronous Hypothesis 241
8.2.1 What For? 241
8.2.2 Basic Notions 243
8.2.3 Mathematical Models 244
8.2.3.1 Synchronous Hypothesis Vs. Neighboring Models 245
8.2.4 Synchronous Languages 245
8.2.5 Implementation Issues 247
8.3 Real-Time Embedded (RT/E) Systems Implementation 248
8.4 The SynDEx Specification Formalism 251
8.4.1 The Architecture 251
8.4.2 Functional Specification 252
8.4.2.1 Syntax 252
8.4.2.2 Operational Semantics 253
8.5 Motivating Example 254
8.5.1 Example of SynDEx Specification 254
8.5.1.1 Dataflow 255
8.5.1.2 Architecture and Timing Information 255
8.5.2 Schedule Generated by SynDEx 256
8.5.3 Optimizing Communications 258
8.6 Execution Conditions 259
8.6.1 Basic Operations 260
8.6.2 Signals 260
8.6.3 Conditioning 261
8.7 Flattened Dataflow 262
8.7.1 Timing Information 262
8.8 Static Schedules 263
8.8.1 Basic Definitions 263
8.8.2 Data Availability 264
8.8.3 Correctness Properties 264
8.8.3.1 Delay Consistency 265
8.8.3.2 Exclusive Resource Use 265
8.8.3.3 Causal Correctness 265
8.9 Scheduling Optimizations 265
8.9.1 Static Dependencies 266
8.9.2 ASAP Scheduling 267
8.9.3 Removal of Redundant Communication 267
8.9.3.1 Removal of Subsequent Emissions of a Same Signal 267
8.9.3.2 Removal of Useless Communication Operations 268
8.10 Related Work 268
8.11 Conclusion and Future Work 270
References 270
Index 273