The Pattern based Visual property Specification Language and supporting system for software verifications

摘要

This paper deals with issue of properties specification for software verifications and translation between formal languages. Through this paper, the unique framework of property specifications including most kinds of formal specifications logics, automatic methods are shown by a property specifications guided system and PVSL(The Pattern based Visual property Specification Language). Additionally, a properties to specify and structures, Interconnection of them are also described by property charts. In this study, the pattern based visual property specification language (PVSL) is defined and property specifications method is also designed by convenience specifications of required property. Required properties can be described by its charts and analyzes its meaning and structures as using patterns diagrams and property and-or tree. On the other hands, it also guarantees stability and limitation of utilizations of patterns using much stronger specifying Dwyer`s meaning based property classification. The PVSL and property charts use hierarchical state machine notation to take advantage of knowledge a person who is one of practitioners has as much as possible, and for Nu-SMV, CW-CNC. They can be adapted to describe property charts and analyze into examples of CTL (Computation Tree Logic) and Modal Mu-Calculus logic that have been already used.