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

A A A | Drucken Print | Impressum Impressum | Sitemap Sitemap | Suche Search | Kontakt Contact | Webseitenanalyse: Mehr Informationen
zum Seitenanfangzum Seitenanfang