Verification of Procedural Programs via Building their Generalized Nets Models Верификация на процедурни програми чрез изграждане на техни обобщени мрежови модели

Todorova, Magdalina. "Verification of Procedural Programs via Building their Generalized Nets Models Верификация на процедурни програми чрез изграждане на техни обобщени мрежови модели." Union of Bulgarian Mathematicians 41.1 (2012): 259-265. <http://eudml.org/doc/250984>.

@article{Todorova2012,
abstract = {Магдалина Василева Тодорова - В статията е описан подход за верификация на процедурни програми чрез изграждане на техни модели, дефинирани чрез обобщени мрежи. Подходът интегрира концепцията “design by contract” с подходи за верификация от тип доказателство на теореми и проверка на съгласуваност на модели. За целта разделно се верифицират функциите, които изграждат програмата относно спецификации според предназначението им. Изгражда се обобщен мрежов модел, специфициащ връзките между функциите във вид на коректни редици от извиквания. За главната функция на програмата се построява обобщен мрежов модел и се проверява дали той съответства на мрежовия модел на връзките между функциите на програмата. Всяка от функциите на програмата, която използва други функции се верифицира и относно спецификацията, зададена чрез мрежовия модел на връзките между функциите на програмата.In the article an approach for verification of procedural programs via building their corresponding generalized nets models is described. This approach integrates the concept of “design by contract” with approaches for verification of type theorem proofs and models consistency check. For this purpose, functions which compose the program, are verified separately according to their specifications. A generalized net model is built, specifying the relationships between functions in the form of correct sequences of calls. For the main function of the program, a generalized net model is built and it is checked whether it complies with the net model of relations between the functions of the program. Each function of the program, which uses other functions defined in the program, is verified also according to the specification set by the net model of relations between the functions of the program. *ACM Classification: D.2.4 Software Engineering: Software/Program Verification – Formal meth-ods, Model checking.The paper is supported by Grant 182/2011 from Sofia University Research Fund.},
author = {Todorova, Magdalina},
journal = {Union of Bulgarian Mathematicians},
keywords = {Generalized Nets; Modeling; Verification; Formal Verification Methods; Procedural Programming},
language = {eng},
number = {1},
pages = {259-265},
publisher = {Union of Bulgarian Mathematicians},
title = {Verification of Procedural Programs via Building their Generalized Nets Models Верификация на процедурни програми чрез изграждане на техни обобщени мрежови модели},
url = {http://eudml.org/doc/250984},
volume = {41},
year = {2012},
}

TY - JOUR
AU - Todorova, Magdalina
TI - Verification of Procedural Programs via Building their Generalized Nets Models Верификация на процедурни програми чрез изграждане на техни обобщени мрежови модели
JO - Union of Bulgarian Mathematicians
PY - 2012
PB - Union of Bulgarian Mathematicians
VL - 41
IS - 1
SP - 259
EP - 265
AB - Магдалина Василева Тодорова - В статията е описан подход за верификация на процедурни програми чрез изграждане на техни модели, дефинирани чрез обобщени мрежи. Подходът интегрира концепцията “design by contract” с подходи за верификация от тип доказателство на теореми и проверка на съгласуваност на модели. За целта разделно се верифицират функциите, които изграждат програмата относно спецификации според предназначението им. Изгражда се обобщен мрежов модел, специфициащ връзките между функциите във вид на коректни редици от извиквания. За главната функция на програмата се построява обобщен мрежов модел и се проверява дали той съответства на мрежовия модел на връзките между функциите на програмата. Всяка от функциите на програмата, която използва други функции се верифицира и относно спецификацията, зададена чрез мрежовия модел на връзките между функциите на програмата.In the article an approach for verification of procedural programs via building their corresponding generalized nets models is described. This approach integrates the concept of “design by contract” with approaches for verification of type theorem proofs and models consistency check. For this purpose, functions which compose the program, are verified separately according to their specifications. A generalized net model is built, specifying the relationships between functions in the form of correct sequences of calls. For the main function of the program, a generalized net model is built and it is checked whether it complies with the net model of relations between the functions of the program. Each function of the program, which uses other functions defined in the program, is verified also according to the specification set by the net model of relations between the functions of the program. *ACM Classification: D.2.4 Software Engineering: Software/Program Verification – Formal meth-ods, Model checking.The paper is supported by Grant 182/2011 from Sofia University Research Fund.
LA - eng
KW - Generalized Nets; Modeling; Verification; Formal Verification Methods; Procedural Programming
UR - http://eudml.org/doc/250984
ER -