Semantics of DFCharts

Abstract

In this chapter we present the formal semantics of DFCharts. Section 4.1 discusses the automata semantics, introduced first in [88], where the behaviour of a complete specification is expressed as an FSM. This section is divided into seven sub-sections Section 4.1.1 introduces multiclock FSMs that are used as inputs to DFCharts operators. Sections 4.1.2–4.1.5 define the semantics of four DFCharts operators: synchronous parallel, asynchronous parallel, localization\hiding and refinement. DFCharts operators are defined in a similar style as Argos [24] operators. However, because of the use of multiclock FSMs, their operation is quite different. Section 4.1.6 defines with a simple language how the operators may be applied on multiclock FSMs. As seen in Chap. 3, an SDFG and an FSM are connected with the asynchronous parallel operator. According to the semantics of the asynchronous parallel operator in Sect. 4.1.3, it operates only on FSMs like all other operators. For this reason, an SDFG is represented as an FSM so that it can be combined with “real FSMs”. This is the topic of Sect. 4.1.7. Since an SDFG proceeds at its own speeds, an FSM that represents an SDFG (“SDF FSM”) is triggered by a clock that is different from the clock of real FSMs. Thus, when a “real FSM” and “SDF FSM” are combined, a multiclock FSM results. In the definitions of operators, which comprise DFCharts automata semantics, rendezvous is treated simply as an event that triggers a transition. What exactly happens on the channel is irrelevant. This is the topic of Sect. 4.2. It examines in detail the ordering of events on a channel within the Tagged Signal Model (TSM) framework. The analysis leads to understanding of how an array variable produces multiple SDF tokens and vice versa. Data transfer from SDF to FSM is the topic of Sect. 4.2.1, while Sect. 4.2.2. deals with data transfer from FSM to SDF. The TSM semantics of DFCharts was previously described in [89]. Finally, Sect. 4.3 examines the effect of clock speeds on DFCharts behaviour.