氏名: 篠原 加奈子 (m06739)
論文題目: Verification of Predicative Specifications for
Real-time Communicating Processes
In this paper, we present a predicative specification method with
the real-time constraints where a process communicates
We first define communicating processes and give the semantics
by converting processes into first order formulas.
This approarch has an advantage that a program is verified by
building up a proof if a required property is satisfied
in the first order predicate calculus.
The specification method is originally proposed by Hehner for
untimed communicating processes where a process communicates
We extend Hehner's theory to real-time communicating processes in
order to it can model the causal relation between communication on
different channels by time stamps that indicate when the events
A program is specified by a predicate that characterizes the
behavior of the program. A behavior is modeled as the set of
values of input and output variables, and communication histories
of values, where each value is accompanied by a time-stamp.
Finally, we present a systematic proof technique that
is to prove if the process specification formula implies
the formula describes a property in the first
order predicate calculus, where both of the formulas are transformed
into normal forms we suggest.
We illustrate the use of our method by showing several examples.