Synchronous Programming of Reactive SystemsSpringer Science & Business Media, 31/12/1992 - 174 من الصفحات This book will attempt to give a first synthesis of recent works con cerning reactive system design. The term "reactive system" has been introduced in order to at'oid the ambiguities often associated with by the term "real-time system," which, although best known and more sugges tive, has been given so many different meanings that it is almost in evitably misunderstood. Industrial process control systems, transporta tion control and supervision systems, signal-processing systems, are ex amples of the systems we have in mind. Although these systems are more and more computerized, it is sur prising to notice that the problem of time in computer science has been studied only recently by "pure" computer scientists. Until the early 1980s, time problems were regarded as the concern of performance evalu ation, or of some (unjustly scorned) "industrial computer engineering," or, at best, of operating systems. A second surprising fact, in contrast, is the growth of research con cerning timed systems during the last decade. The handling of time has suddenly become a fundamental goal for most models of concurrency. In particular, Robin Alilner 's pioneering works about synchronous process algebras gave rise to a school of thought adopting the following abstract point of view: As soon as one admits that a system can instantaneously react to events, i. e. |
المحتوى
Introduction | 8 |
12 Classical approaches | 8 |
13 The synchronous approach | 8 |
14 Complex systems | 8 |
15 Summary of this book | 8 |
Four Synchronous Languages | 9 |
The imperative language Esterel | 11 |
23 Programming primitives | 13 |
52 Causality checking in Argos | 77 |
53 Clock checking in Lustre | 80 |
54 The clock calculus of Signal | 81 |
Sequential code generation | 85 |
612 Example | 86 |
613 Comments | 91 |
62 The Lustre compiler | 93 |
622 Single loop | 94 |
231 Declarations | 14 |
233 Statements | 15 |
24 Programming style and first examples | 21 |
242 Use of broadcasting | 22 |
243 Instantaneous dialogue | 23 |
244 A stopwatch | 25 |
25 Causality problems in Esterel | 29 |
252 Multiple behavior | 30 |
253 Putting right the stopwatch | 31 |
262 Interface | 32 |
263 Computation of the average reflex time | 33 |
264 The program body | 34 |
Graphic formalisms the language Argos | 39 |
31 Automata and operators | 40 |
312 Argos operators | 41 |
32 Causality problems | 45 |
33 Programming style | 46 |
331 Termination by exception | 47 |
333 Interrupt | 49 |
Declarative languages Lustre and Signal | 53 |
42 The language Lustre | 55 |
421 Flows and clocks | 56 |
422 Variables equations expressions and assertions | 57 |
423 Program structure | 60 |
424 Causality in LUSTRE | 62 |
43 The language SIGNAL | 68 |
432 Program structure | 71 |
Compilation | 73 |
Static verifications | 75 |
623 Compiling Lustre into automata | 96 |
63 The OC code and associated tools | 100 |
Distributed code generation | 103 |
72 Code distribution in Signal | 104 |
721 Static dependences | 105 |
722 Dynamic dependences | 107 |
731 Code replication | 109 |
733 Useless emission elimination | 110 |
734 Placement of receiving statements | 111 |
735 Synchronization | 112 |
736 Final processing | 114 |
Circuit generation from synchronous programs | 117 |
on a programmable active memory | 118 |
822 Translation of Boolean Lustre | 120 |
823 Translating full Lustre | 123 |
83 Hardware implementation of pure Esterel | 129 |
832 First example | 130 |
833 Translating Parallel and Exceptions | 133 |
Program Verification | 137 |
Lustre program verification the tool Lesar | 139 |
91 Specification of safety properties | 140 |
92 Verification | 143 |
Using Auto for Esterel program verification | 149 |
Conclusion | 157 |
112 Works in progress | 159 |
Bibliography | 161 |
171 | |
طبعات أخرى - عرض جميع المقتطفات
Synchronous Programming of Reactive Systems <span dir=ltr>Nicolas Halbwachs</span> لا تتوفر معاينة - 2010 |
Synchronous Programming of Reactive Systems <span dir=ltr>Nicolas Halbwachs</span> لا تتوفر معاينة - 2014 |
عبارات ومصطلحات مألوفة
_pre_remaining_delay alarm ARGOS array assertion automata basic clock behavior bisimulation bool BUTTON_2 causality loop cell circuit computed considered constraints coroutine corresponding cycle data-flow declaration defined delay distributed code emission emit LAP end end environment equations ESTEREL compiler ESTEREL program example execution exit false Figure finite FLIP flip-flop formal verification frozen FROZEN_TIME Gérard Berry GO lamp goto S1 goto STATE1 Grenoble halt watching hardware implementation INIT initial input events input signals input/output INRIA instance integer interface internal_time LIFT STOPPED logical loop LUSTRE program millisecond model checking module node nondeterminism occurs OPEN DOOR.COMMAND operator output parallel composition parameters present program verification reaction reactive systems remaining_delay reset running safety properties semantics sequence of values sequential code START_STOP stat STATECHARTS stopwatch STOPWATCH_RUNNING subprocess synchronous languages synchronous programming temporal temporal logic termination timeout transition transition table translation true tuple upto variables watchdog watchdog_is_on wires
مقاطع مشهورة
الصفحة 165 - Coudert, JC Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams.