The Pattern Based Visual Property Specification Language and Supporting System for Software Verifications

Abstract:

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.Keywords: Patterns, Property specifications, model checking, Software verification

• Periodical: Applied Mechanics and Materials (Volumes 752-753)
• Pages: 1090-1096
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.752-753.1090
• Online since: April 2015
• Authors: Seung Su Chun*
• Keywords: Model Checking, Pattern, Property Specifications, Software Verification

References

[1] E.M. Clarke, Model Checking, MIT Press, Cambridge MA, (1999).

[2] E.A. Emerson, Model Checking and the Mu-Calculus, DIMACS. 31 (1997) 185-195.

[3] J.C. Corbett, A Language Framework For Expressing Checkable Properties of Dynamic Software, SPIN Software Model Checking Workshop LNCS. 1885 (2000) 205-223.

DOI: 10.1007/10722468_13

[4] M.B. Dwyer, Property Specification Patterns for Finite-State Verification, Proceedings of the Workshop on Formal Methods in Software Practice, (1998) 7-15.

DOI: 10.1145/298595.298598

[5] A.D. Bimbo, Visual Specification of Branching Time Temporal Logic, Proceedings of the 11th IEEE Symposium on Visual Languages, (1995), 61-68.

DOI: 10.1109/vl.1995.520786

[6] D. Harel, The STATEMATE Semantics of State-charts, ACM Trans. on Software Eng. Methodology, 5 (1996) 293-333.

DOI: 10.1145/235321.235322

[7] R. Alur, Model Checking of Hierarchical State Machines, Proceedings of the 6th ACM Symposium on Foundations, 23 (1998) 175-188.

DOI: 10.1145/288195.288305

[8] A. Cimatti and Edmund Clarke, Nu SMV 2: An OpenSource Tool for Symbolic Model Checking, CAV LNCS 2404, (2002) 359-364.

[9] A. Neuser, A GUI for Real-time Visualization of On-line Model Checking with UPPAAL, Institute for Software Systems, Hamburg University of Technology TUHH, (2014).

[10] S. Konur, Towards Light-Weight Probabilistic Model Checking, Hindawi publishing corporation, J. Appl. Math. Article, 814159 (2014) 1-15.

[11] D. Wei, A Model-Driven Approach to Trace Checking of Temporal Properties with OCL, Open Repository and Bibliography, S&T Centre, University of Luxembourg, (2014).

[12] J. Campos, C. Machado, A specification patterns system for discrete event systems analysis, InTech, repositorium. sdum. uminho. pt, (2013).

[13] DR Kulkarni. Improved model generation and property specification for analog/mixed-signal circuits, async. ece. utah. edu, (2013).

[14] S. Steinhorst and L. Hedrich, A formal approach to complete state space-covering input stimuli generation for verification of analog systems, GMM-Fachbericht-ANALOG, vde-verlag. de, (2008).

[15] M.H. Zaki and S. Tahar, Formal verification of analog and mixed signal designs: A survey, J. Microelectron. 37 (2008) 1395-1404.

DOI: 10.1016/j.mejo.2008.05.013