Shukla / Talpin Synthesis of Embedded Software

Frameworks and Methodologies for Correctness by Construction
1. Auflage 2010
ISBN: 978-1-4419-6400-7
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 266 Seiten

Embedded software is ubiquitous today. There are millions of lines of embedded code in smart phones, and even more in systems responsible for automotive control, avionics control, weapons control and space missions. Some of these are safety-critical systems whose correctness, timely response, and reliability are of paramount importance. These requirement pose new challenges to system designers. This necessitates that a proper design science, based on 'constructive correctness' be developed. Correct-by-construction design and synthesis of embedded software is done in a way so that post-development verification is minimized, and correct operation of embedded systems is maximized. This book presents the state of the art in the design of safety-critical, embedded software. It introduced readers to three major approaches to specification driven, embedded software synthesis/construction: synchronous programming based approaches, models of computation based approaches, and an approach based on concurrent programming with a co-design focused language. It is an invaluable reference for practitioners and researchers concerned with improving the product development life-cycle.

Autoren/Hrsg.

Talpin, Jean-Pierre

Shukla, Sandeep Kumar

Inhaltsverzeichnis

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