Property Based Verification of Evolving Petri Nets

Yasir Imtiaz Khan, Ehab Al-shaer

Research output: Chapter in Book/Report/Conference proceedingConference proceeding

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
Title of host publicationICSEA 2015 - The Tenth International Conference on Software Engineering Advances
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

Conference

ConferenceThe Tenth International Conference on Software Engineering Advances
Abbreviated titleICSEA 2015
CountrySpain
CityBarcelona
Period15/11/1520/11/15
Internet address

Fingerprint

Petri nets
Model checking
Communication
Costs

Cite this

Khan, Y. I., & Al-shaer, E. (2015). Property Based Verification of Evolving Petri Nets. In ICSEA 2015 - The Tenth International Conference on Software Engineering Advances

Property Based Verification of Evolving Petri Nets. / Khan, Yasir Imtiaz; Al-shaer, Ehab.

ICSEA 2015 - The Tenth International Conference on Software Engineering Advances. 2015.

Research output: Chapter in Book/Report/Conference proceedingConference proceeding

Khan, YI & Al-shaer, E 2015, Property Based Verification of Evolving Petri Nets. in ICSEA 2015 - The Tenth International Conference on Software Engineering Advances. The Tenth International Conference on Software Engineering Advances, Barcelona, Spain, 15/11/15.
Khan YI, Al-shaer E. Property Based Verification of Evolving Petri Nets. In ICSEA 2015 - The Tenth International Conference on Software Engineering Advances. 2015
Khan, Yasir Imtiaz ; Al-shaer, Ehab. / Property Based Verification of Evolving Petri Nets. ICSEA 2015 - The Tenth International Conference on Software Engineering Advances. 2015.
@inproceedings{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",
isbn = "978-1-61208-438-1",
booktitle = "ICSEA 2015 - The Tenth International Conference on Software Engineering Advances",

}

TY - GEN

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 - Conference proceeding

SN - 978-1-61208-438-1

BT - ICSEA 2015 - The Tenth International Conference on Software Engineering Advances

ER -