MECHANIZATION OF REAL-TIME LINEAR CSP WITH HIGHER ORDER LOGIC

Abstract

A linear form of Reed-Roscoe Timed Communicating Sequential Processes mechanized with the Higher Order Logic Proof System is presented. The syntax for the Real-Time Linear CSP (RTLCSP) language is sufficient to describe the behavior of time-constrained communicating processes in real-time systems. The operational semantics of RTLCSP is expressed in terms of inference rules and Coloured Hierarchical Petri nets for a transition system for real-time programs. RTLCSP processes are characterized in terms of an extension of the Lynch-Tuttle signature for communicating processes. The signature of a process is helpful in reasoning about process behavior and in defining the semantics of empty processes or processes with hidden actions. The linear character of RTLCSP stems from its resource consciousness inasmuch as restrictions are placed on the number of times that a process can be restarted. The complete mechanization of RTLCSP in HOL (called RTLCSP-HOL) is presented in detail. The presentation includes a brief introduction to HOL itself to permit experimentation with RTLCSP-HOL. Sample HOL proofs relative to RTLCSP constructs are also given.