The Theory Of Signal Calculus

With the continual development of computer science and IT industry, real-time sys-tems are designed to cater to wide and deep applications from social production to peo-ple's daily life, such as Video on demand(VOD), information acquisition and retrieval sys-tems(ICRS), Cyber-Physical systems(CPS), complex control systems for aerospace, mil-itary and nuclear plants, etc. Compared to general software systems, real-time systems should have more rigid requirements and specifications. Responses to external events should be within strict bounded time limits. The external environment may be greatly terrible and highly nondeterministic. Thus real-time systems are expected to meet the dependability and survivability. Furthermore, real-time systems often consist of asyn-chronous distributed units. In summary, real-time systems tend to be large, complex and extraordinarily hard to test. Since the above characteristics bring serious challenges for the design of real-time systems, the research on the theory of real-time systems facilitates the description, analysis, design, implementation and verification of real-time systems.A theory of programming is intended to support the practice of programming by relating each program to the specification of what it is intended to achieve. The main con-tent of programming theory is to explain the meaning of the notations of the language. In general, the presentation of semantics may be classified into three methods:denotational semantics, operational semantics and algebraic semantics. The denotational method de-fines each notation and formula of the language as denoting some value in a mathematical domain; the operational semantics describes how a program can be executed by a series of steps of some abstract mathematical machine; the algebraic method is subtle and ab-stract, and it does not give the actual meanings of programs, but describes the properties of programs by a set of algebraic equations (inequations). Each of these presentations has its distinctive advantages, thus exploring and understanding the relationship between pre-sentations is an important indicator of the value and maturity of the programming theory.In this paper, we present a signal calculus for event-based synchronous language used for specification and programming of embedded systems. Inspired by the unifying theory of programming, the signal calculus is divided into a set of several sub-calculus characterized by different features. For each signal sub-calculus, we first explore the al-gebraic semantics and the corresponding normal form, and then investigate denotational semantics which is consistent with the algebraic semantics. By demonstrating the equiv-alence of two semantics, it exhibits the importance of algebraic method in the unifying theory of programming and also makes contribution to the development of the theory of programming language for real-time systems and the semantic theory of signal calculus. The main contribution of this paper includes:●We propose a signal calculus for event-based synchronous language which follows the so-called synchronous hypothesis and finite variability hypothesis. It covers several novel features of the specification language for real-time systems, such as instant/delay, finite/infinite, termination/divergence, sequential/concurrent, etc. To reduce the complexity and difficulty of the theory of signal calculus, several signal sub-calculus are characterized by different features.●We explore the algebraic semantics and denotational semantics of all signal sub-calculus respectively. A set of algebraic laws is provided to describe the meaning of the primitives and combinators of signal calculus. The corresponding normal forms are investigated and all reactions can be algebraically reduced to normal forms. For denotational model, the mathematical domains for different sub-calculus are con-structed respectively. Every instantaneous reaction is denoted by a healthiness event input/output function while each delay reaction is modeled by a normal execution tree class.●We also deal with the semantic linking theory. In essential, denotational semantics and algebraic semantics are equivalent, i.e., the equality of two differently written reactions is algebraically provable if and only if the two reactions are equivalent with respect to the denotational semantics. On one hand, all algebraic laws can be established in the framework of denotational method which claims the sound-ness of the algebraic method. On the other hand, reactions which are equivalent from the denotational perspective can be reduced to the same normal form and this demonstrates the relative completeness of algebraic method.