Methods of dynamic verification of the code based on the interpretation of Petri nets

Authors

  • Богдан Анатолійович Гнесюк Cherkassy National University Cherkassy city, Shevcenko Street, 81, 18031, Ukraine
  • Оксана Олександрівна Супруненко Cherkassy National University Cherkassy city, Shevcenko Street, 81, 18031, Ukraine

DOI:

https://doi.org/10.15587/1729-4061.2013.8926

Keywords:

dynamic verification, parse tree, Petri net, stochastic elements.

Abstract

One of the topical problems in the development of secure applications is the improvement of the quality of the software systems with parallel-sequential code. The verification of a software project is able to solve this problem, subject to the construction of adequate models of functioning of applications and the use of qualitative methods of verification of parallel-sequential programming models. The article considers the methods of static and dynamic verification of applications. The structure of the model for verification was proposed to be build on the basis of an intermediate model that is a complete parse tree. The working model was formed as the control Petri net (SN) with stochastic elements that allowed simulating the functioning of application under different time and communication conditions, and allowed static and dynamic analysis of critical situations. While constructing the model we have implemented the control function of the verifier, which consisted in analysis of the effects of correction of defects in the code, which would help achieve the control of the verification of applications. The article contains the example of the practical implementation of these methods - a verification of the applications written in C ++.

Author Biographies

Богдан Анатолійович Гнесюк, Cherkassy National University Cherkassy city, Shevcenko Street, 81, 18031

Master student

Department of Software of automated systems

Оксана Олександрівна Супруненко, Cherkassy National University Cherkassy city, Shevcenko Street, 81, 18031

Associate professor, docent

Department of Software of automated systems

References

  1. Карпов, Ю.Г. MODEL CHECKING. Верификация параллельных и распределенных программных систем [Текст] / Ю.Г. Карпов. – СПб.: БХВ-Петербург, 2010. – 560 с.
  2. Синицын, С.В. Верификация программного обеспечения (ISBN: 978-5-94774-825-3) [Электронный документ] / С.В. Синицын, Н.Ю. Налютин. Режим доступа: http://www.intuit.ru/department/se/verify/. Проверено 20.12.12.
  3. Data-flow analysis. Available at: http://en.wikipedia.org/wiki/Data-flow_analysis. (accessed 15 January 2013).
  4. Верификация кода и обнаружение ошибок исполнения путем абстрактной интерпретации. [Электронный документ]. Режим доступа: http://sl-matlab.ru/news/detail.php?ID=723. Проверено 17.12.2012.
  5. Steve Cornett. Code Coverage Analysis. Available at: http://www.bullseye.com/coverage.html (accessed 7 December 2012).
  6. Frank Tip. A survey of program slicing techniques. Journal of Programming Languages, Volume 3, Issue 3, pages 121–189, September 1995.
  7. Programming With Assertions. Available at: http://docs.oracle.com/javase/ 1.4.2/docs/guide/lang/assert.html (accessed 9 December 2012).
  8. Rob Smith. J2SE 1.4 Assertion Facility. Available at: http://jnb.ociweb.com/jnb/jnbApr2002.html (accessed 9 December 2012).
  9. Кузьмук, В.В. Модифицированные сети Петри и устройства моделирования параллельных процессов: Монография [Текст] / В.В. Кузьмук О.О. Супруненко. – К.: Маклаут, 2010. – 252 с.

Downloads

Published

2013-02-05

How to Cite

Гнесюк, Б. А., & Супруненко, О. О. (2013). Methods of dynamic verification of the code based on the interpretation of Petri nets. Eastern-European Journal of Enterprise Technologies, 1(2(61), 24–27. https://doi.org/10.15587/1729-4061.2013.8926

Issue

Vol. 1 No. 2(61) (2013): Information technology

Section

Information technology

License

Copyright (c) 2014 Богдан Анатолійович Гнесюк, Оксана Олександрівна Супруненко

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

The consolidation and conditions for the transfer of copyright (identification of authorship) is carried out in the License Agreement. In particular, the authors reserve the right to the authorship of their manuscript and transfer the first publication of this work to the journal under the terms of the Creative Commons CC BY license. At the same time, they have the right to conclude on their own additional agreements concerning the non-exclusive distribution of the work in the form in which it was published by this journal, but provided that the link to the first publication of the article in this journal is preserved.

A license agreement is a document in which the author warrants that he/she owns all copyright for the work (manuscript, article, etc.).
The authors, signing the License Agreement with TECHNOLOGY CENTER PC, have all rights to the further use of their work, provided that they link to our edition in which the work was published.
According to the terms of the License Agreement, the Publisher TECHNOLOGY CENTER PC does not take away your copyrights and receives permission from the authors to use and dissemination of the publication through the world's scientific resources (own electronic resources, scientometric databases, repositories, libraries, etc.).
In the absence of a signed License Agreement or in the absence of this agreement of identifiers allowing to identify the identity of the author, the editors have no right to work with the manuscript.
It is important to remember that there is another type of agreement between authors and publishers – when copyright is transferred from the authors to the publisher. In this case, the authors lose ownership of their work and may not use it in any way.