A Flexible Verifier of Temporal Properties for LOTOS

Kaoru TAKAHASHI  Yoshiaki TOKITA  Takehisa TANAKA  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E79-D    No.1    pp.8-21
Publication Date: 1996/01/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Sofware System
Keyword: 
specification,  verification,  protocol,  LOTOS,  software tool,  

Full Text: PDF(1MB)>>
Buy this Article


Summary: 
This paper discusses a software verification support environment Vega which is based on a model-theoretic methodology that enables verification support for the temporal properties of protocol specifications described in the formal description technique LOTOS. In the methodology of Vega, a protocol specification is defined through the LOTOS process reflecting its practical system structure. The temporal properties to be verified are given as the requirement which the protocol needs to satisfy from the viewpoint of events and are formulated by using the branching time temporal logic defined in this paper. Verification is done by determining whether or not the given temporal properties are satisfied by the model, which corresponds to the transition system derived from the LOTOS specification of the protocol. Vega is provided with an effective interface function, as well as the function of simple model checking based on the above methodology, to give some degree of flexibility for the expression of temporal properties to be verified. Specifically, it allows the user to define useful expressions by combining builtin temporal logic formulas and enter them in Vega for use at any time. With the provision of these functions, Vega is expected to serve as a very powerful and flexible verification support tool.

open access publishing via