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 Dive into the research topics of 'Property Based Verification of Evolving Petri Nets'. Together they form a unique fingerprint.

  • 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