Issues and Nuances
It is important to note that unlike the automated verification
support for model theoretic approaches, the formal verification
for proof theoretic approaches (such as our IT/DT approach) are
interactive by nature. As the axioms and theory get specified,
the user is required to guide the verification process by
directing the formulation of queries to the formal engine. Once
the query has been posed, the running of the formal engine (PVS in
our case) is an automated process. This follows naturally, as
the intent of the verification process is to deductively ascertain
the correctness (or lack of it) of specific & desired properties
of the protocol of interest. In model theoretic approaches, one
does have the option of specifiying the basic protocol behavior
and allowing the formal engine to automatically generate the
state space for analysis.
Thus, the formulation of the IT and DT follow an interactive process
for (a) posing the queries, (b) feedback of inference conditions
as new conditions, and (c) adding new conditionals (actual or speculative)
to the conditional space. After these conditionals/queries have
been posed, the running of the subsequent verification is automated.
As our test identification process requires query formulation and
adding revised conditionals, the process is interactive to this
extent and automated for the subsequent formal analysis after the
queries/conditionals have been specified.
Given the nature of proof theoretic analysis there are no known
technqiues for complete automation of the formal process.
At this stage, we are looking into developing techniques (similar
to syntactic analysis) for automatically extracting possible
query cases from the formal (as well as informal) protocol
specifications.
The following paper,
``On the Use of Formal Techniques for
Validation'', describes the basic formal approache for V&V. The
sucessive papers in FTCS-29 and RTSS (1999) [which can be found alongside
the specs] provide more details on the approach.
The following set of files detail the specifications for each specific
application domain. The requisite papers can be found therein too.
Formal Specifications for Resource Allocation & Scheduling Protocols
Formal Specifications for Redundancy Management Protocols
Formal Specifications for Group Communication Protocols