Home // ICSEA 2015, The Tenth International Conference on Software Engineering Advances // View article

Property Based Verification of Evolving Petri Nets

Authors:
Yasir Imtiaz Khan
Ehab Al-Shaer

Keywords: Software evolution, Re-verification, Model checking, Iterative refinements, Slicing

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.

Pages: 301 to 306

Copyright: Copyright (c) IARIA, 2015

Publication date: November 15, 2015

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-438-1

Location: Barcelona, Spain

Dates: from November 15, 2015 to November 20, 2015