Property Based Verification of Evolving Petri Nets

Yasir Imtiaz Khan, Ehab Al-shaer

Research output: Contribution to journalArticle

Abstract

Software evolution is inevitable in the field of information and communication technology systems. Existing software systems continue to evolve to progressively reach important qualities such as completeness and correctness. Iterative refinements and incremental developments are considered to be
well suitable for the development of evolving systems among other approaches. The problem with iterative refinements and incremental development is the lack of support of an adequate verification process. In general, all the proofs are redone after every evolution, which is very expensive in terms of cost and time. In this work, we propose a slicing based solution to add an adequate verification process to iterative refinements and incremental development technique. Our proposal has two objectives, the first is to perform verification only on those parts that may influence the property satisfaction by the analyzed model. The second is to classify the evolutions and properties to identify which evolutions require re-verification. We argue that for the class of evolutions that requires re-verification, instead of verifying the whole system only a part that is concerned by the property would be sufficient. We use Petri nets as a modeling formalism and model checking as a verification approach to show the viability of the proposed approach.
Original languageEnglish
JournalInternational Conference on Software Engineering Advances, ICSEA
Publication statusPublished - 2015
EventThe Tenth International Conference on Software Engineering Advances - Barcelona, Spain
Duration: 15 Nov 201520 Nov 2015
Conference number: 10
https://www.iaria.org/conferences2015/ICSEA15.html

Fingerprint

Petri nets
Model checking
Communication
Costs

Cite this

@article{cb1ecf23722f4bf2bf4f03732c24645b,
title = "Property Based Verification of Evolving Petri Nets",
abstract = "Software evolution is inevitable in the field of information and communication technology systems. Existing software systems continue to evolve to progressively reach important qualities such as completeness and correctness. Iterative refinements and incremental developments are considered to bewell suitable for the development of evolving systems among other approaches. The problem with iterative refinements and incremental development is the lack of support of an adequate verification process. In general, all the proofs are redone after every evolution, which is very expensive in terms of cost and time. In this work, we propose a slicing based solution to add an adequate verification process to iterative refinements and incremental development technique. Our proposal has two objectives, the first is to perform verification only on those parts that may influence the property satisfaction by the analyzed model. The second is to classify the evolutions and properties to identify which evolutions require re-verification. We argue that for the class of evolutions that requires re-verification, instead of verifying the whole system only a part that is concerned by the property would be sufficient. We use Petri nets as a modeling formalism and model checking as a verification approach to show the viability of the proposed approach.",
author = "Khan, {Yasir Imtiaz} and Ehab Al-shaer",
year = "2015",
language = "English",
journal = "International Conference on Software Engineering Advances, ICSEA",

}

TY - JOUR

T1 - Property Based Verification of Evolving Petri Nets

AU - Khan, Yasir Imtiaz

AU - Al-shaer, Ehab

PY - 2015

Y1 - 2015

N2 - Software evolution is inevitable in the field of information and communication technology systems. Existing software systems continue to evolve to progressively reach important qualities such as completeness and correctness. Iterative refinements and incremental developments are considered to bewell suitable for the development of evolving systems among other approaches. The problem with iterative refinements and incremental development is the lack of support of an adequate verification process. In general, all the proofs are redone after every evolution, which is very expensive in terms of cost and time. In this work, we propose a slicing based solution to add an adequate verification process to iterative refinements and incremental development technique. Our proposal has two objectives, the first is to perform verification only on those parts that may influence the property satisfaction by the analyzed model. The second is to classify the evolutions and properties to identify which evolutions require re-verification. We argue that for the class of evolutions that requires re-verification, instead of verifying the whole system only a part that is concerned by the property would be sufficient. We use Petri nets as a modeling formalism and model checking as a verification approach to show the viability of the proposed approach.

AB - Software evolution is inevitable in the field of information and communication technology systems. Existing software systems continue to evolve to progressively reach important qualities such as completeness and correctness. Iterative refinements and incremental developments are considered to bewell suitable for the development of evolving systems among other approaches. The problem with iterative refinements and incremental development is the lack of support of an adequate verification process. In general, all the proofs are redone after every evolution, which is very expensive in terms of cost and time. In this work, we propose a slicing based solution to add an adequate verification process to iterative refinements and incremental development technique. Our proposal has two objectives, the first is to perform verification only on those parts that may influence the property satisfaction by the analyzed model. The second is to classify the evolutions and properties to identify which evolutions require re-verification. We argue that for the class of evolutions that requires re-verification, instead of verifying the whole system only a part that is concerned by the property would be sufficient. We use Petri nets as a modeling formalism and model checking as a verification approach to show the viability of the proposed approach.

M3 - Article

JO - International Conference on Software Engineering Advances, ICSEA

JF - International Conference on Software Engineering Advances, ICSEA

ER -