氏名: 篠原 加奈子 (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
synchronously.
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
asynchronously.
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
happen.
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.
目次に戻る