QuoteRef: benvA1_2003

topics > all references > ThesaHelp: references a-b

type-safe and secure languages
safety critical systems
parallel programming languages
synchronized processing
program proving
event controlled processing
conditional control by guards
hard real time systems
state machine
static single assignment; SSA
data flow languages
processing a sequence
temporal relationships
event time
conditional control
task scheduling
system builds
metaphysics and epistemology
formal methods and languages
code optimization
constructing proof and program together


Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., De Simone, R., "The synchronous languages 12 years later", Proceedings of the IEEE, 91, 1, January 2003, pp. 64-83. Google

64 ;;Quote: use synchronous languages for real-time, embedded, safety critical applications
64+;;Quote: designers of safety-critical systems must convince themselves, the customer, and certification authorities that the design and implementation are correct
66 ;;Quote: the parallel composition of guarded microsteps has confusing semantics and multiple interpretations; used by VHDL, Verilog, and others
66 ;;Quote: acyclic, embedded control systems do not have zero-delay loops; e.g., sample-driven, compute outputs on each clock tick
66 ;;Quote: fixpoint control treats each reaction as the unique fixpoint for 'state+input -> state+output'; e.g., Esterel; difficult to prove unique
66 ;;Quote: constrained control systems may allow blocked reactions or multiple, nondeterministic reactions; proving uniqueness is difficult; e.g., Signal and Sildex
66 ;;Quote: treat control variables as a flow of values, one per clock tick; system of equations or dataflow network; each variable defined exactly once
66+;;Quote: Lustre extends the usual operators to operate pointwise on flows of values
67 ;;Quote: for any flow x, pre(x) is the previous value; a- >x is initially a then x; e.g., count of rising edges
67 ;;Quote: a node in Lustre is a function of typed input flows; defined by a system of equations and local flows; exactly one definition for each output or local flow
67 ;;Quote: flows can follow slower clocks; e.g., 'x when c' is x's values when c is true; most flow operators use the same clock
67 ;;Quote: flow operators deactivated if an operand clock is false
67+;;Quote: Lustre controls program activation by clocks
67 ;;Quote: if activation condition is false, a flow node's value is either frozen or a default value; deactivation by clocks too restrictive
67 ;;Quote: Lustre scheduling by topological sort; disallows syntactically cyclic definitions
67+;;Quote: Scade requires a pre operator for feedback values; enables separate compilation; i.e., execution order within a node is independent of the node's caller
69 ;;Quote: Esterel's formal semantics is based on constructive causality
69+;;Quote: formal semantics enables compile-time optimization, analysis, and verification

Related Topics up

Topic: type-safe and secure languages (43 items)
Topic: safety critical systems (32 items)
Topic: parallel programming languages (14 items)
Topic: synchronized processing (35 items)
Group: program proving   (10 topics, 311 quotes)
Topic: event controlled processing (46 items)
Topic: conditional control by guards (17 items)
Topic: hard real time systems (64 items)
Topic: state machine (67 items)
Topic: static single assignment; SSA (19 items)
Topic: data flow languages (33 items)
Topic: processing a sequence (17 items)
Topic: temporal relationships (40 items)
Topic: event time (45 items)
Group: conditional control   (7 topics, 142 quotes)
Topic: task scheduling (49 items)
Topic: system builds (43 items)
Topic: metaphysics and epistemology (99 items)
Topic: formal methods and languages (53 items)
Topic: code optimization (54 items)
Topic: constructing proof and program together (22 items)

Collected barberCB 8/04
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.