Browse ORBi

- What it is and what it isn't
- Green Road / Gold Road?
- Ready to Publish. Now What?
- How can I support the OA movement?
- Where can I learn more?

ORBi

Property based model checking of structurally evolving Algebraic Petri nets Khan, Yasir Imtiaz Doctoral thesis (2015) There are two important challenges in any system development life cycle, the first is to ensure the correctness of a model at the earliest stage possible and the second is to ensure its correctness once ... [more ▼] There are two important challenges in any system development life cycle, the first is to ensure the correctness of a model at the earliest stage possible and the second is to ensure its correctness once it evolves with respect to the emergence of new requirements, performance may need to be improve, business environment is changing. Usual verification techniques such as testing and simulation are used commonly for the verification of a model. The downsides of these techniques are that there is no guarantee of the absence of errors and they need to be repeated after every evolved version. Model checking is an automatic technique for verifying finite state system models. Although, model checking is proved to be a useful technique, the typical drawback of model checking is its limits with respect to the state space explosion problem. As system gets reasonably complex, completely enumerating their states demands increasing amount of resources. Various techniques like symbolic model checking, on the fly model checking and compositional reasoning partially overcome this problem. Petri net is a well-known low-level formalism for modeling and verifying concurrent and distributed systems. The modeling of systems by low-level Petri nets is tedious and therefore various advancements have been created to raise the level of abstraction of Petri nets. Among others, Algebraic Petri nets raise the level of abstraction of Petri nets by replacing black tokens with the elements of user defined data types i.e., algebraic abstract data types. The first contribution of this thesis is to develop an approach to tackle the state space explosion problem for model checking of Algebraic Petri nets by re-using, adapting and refining state of the art techniques. The proposed approach is based on slicing and the central idea is to perform verification only on those parts that may affect the property the Algebraic Petri net model is analyzed for. We propose several slicing algorithms for Algebraic Petri nets and can be applied to Petri nets by slight modifications. The proposed slicing algorithms can alleviate the state space even for certain strongly connected nets and are proved not to increase the state space. The second contribution is an approach to improving re-verification of structurally evolving Algebraic Petri nets. The idea is to classify evolutions and properties to identify which evolutions require re-verification. We argue that for the class of evolutions that require verification, instead of verifying the whole system, only a part that is concerned by the property can be sufficient. The third contribution is the development of a stand-alone tool i.e., SLAPn. The objective of this tool is to implement proposed slicing algorithms and to show the practical usability of slicing technique. An interesting exploitation of SLAPn is that it can be added to any existing model checker as a pre-processing step. [less ▲] Detailed reference viewed: 234 (18 UL)Slicing High-level Petri nets Khan, Yasir Imtiaz ; Guelfi, Nicolas in International Workshop on Petri Nets and Software Engineering (PNSE'14), Tunis June 2014 (2014, June 23) High-level Petri nets (evolutions of low-level Petri nets) are well suitable formalisms to represent complex data, which influence the behavior of distributed, concurrent systems. However, usual ... [more ▼] High-level Petri nets (evolutions of low-level Petri nets) are well suitable formalisms to represent complex data, which influence the behavior of distributed, concurrent systems. However, usual verification techniques such as model checking and testing remain an open challenge for both (i.e., low-level and high-level Petri nets) because of the state space explosion problem and test case selection. The contribution of this paper is to propose a technique to improve the model checking and test- ing of systems modeled using Algebraic Petri nets (a variant of high-level petri nets). To achieve the objective, we propose different slicing algo- rithms for Algebraic Petri nets. We argue that our slicing algorithms significantly improve the state of the art related to slicing APNs and can also be applied to low-level Petri nets with slight modifications. We exemplify our proposed algorithms through a case study of a car crash management system. [less ▲] Detailed reference viewed: 137 (19 UL)SLAPn: A Tool for slicing Algebraic Petri nets Khan, Yasir Imtiaz ; Guelfi, Nicolas Poster (2014) Algebraic Petri nets is a well suited formalism to represent the behavior of concurrent and distributed systems by handling complex data. For the analysis of systems modelled in Algebraic Petri nets ... [more ▼] Algebraic Petri nets is a well suited formalism to represent the behavior of concurrent and distributed systems by handling complex data. For the analysis of systems modelled in Algebraic Petri nets, model checking and testing are used commonly. Petri nets slicing is getting an attention recently to improve the analysis of systems modelled in Petri nets or Algebraic Petri nets. This work is oriented to define Algebraic Petri nets slicing and implement it in a verification tool. [less ▲] Detailed reference viewed: 103 (11 UL)Optimizing verification of structurally evolving algebraic petri nets Khan, Yasir Imtiaz in Lecture Notes in Computer Science (2013, September 08), 8166 System models are subject to evolve during the development life cycle, along which an initial version goes through a series of evolutions, generally aimed at progressively reaching all the requested ... [more ▼] System models are subject to evolve during the development life cycle, along which an initial version goes through a series of evolutions, generally aimed at progressively reaching all the requested qualities (completeness, correctness etc.). Among the existing development methodologies the iterative and incremental one has been proved to be efficient for system development but lacks of support for an adequate verification process. When considering Algebraic Petri nets (APNs) for modeling and model checking for verification, all the proofs must be redone after each iteration which is impractical both in terms of time and space. In this work, we introduce an Algebraic Petri net slicing technique that optimizes the model checking of static or structurally evolving APN models. Furthermore, our approach is proposing a classification of evolutions dedicated to the improvement of model checking. [less ▲] Detailed reference viewed: 162 (9 UL)Random Cluster Sampling on X-Machines Test Cases Khan, Yasir Imtiaz ; in 11th International Conference on Information Technology : New Generations ITNG 2013 (2013) Software testing is considered one of the most expensive and critical phases of the software development. Formal testing approaches are extensively used for verifying the conformance of implementations to ... [more ▼] Software testing is considered one of the most expensive and critical phases of the software development. Formal testing approaches are extensively used for verifying the conformance of implementations to a given specification. These formal approaches usually generate a large amount of input test data which is costly in terms of time and effort. Techniques for reducing test input data are thus of the utmost importance. The contribution of this paper is to propose a framework for the reduction of test input data generated by a formal testing approach based on X-Machines. To achieve these objectives we have applied a well known statistical approach called Random Cluster Sampling on the test case set generated by a formal approach X-Machines. To exemplify our technique we have generated a test set for an X-Machine Microwave oven specification and then drew a sample from the test set by using the Random Cluster sampling technique. Based on the tolerated fault rate we have extracted conclusion about the accuracy of implementation. [less ▲] Detailed reference viewed: 101 (5 UL)Optimizing algebraic petri net model checking by slicing Khan, Yasir Imtiaz ; in International Workshop on Modeling and Business Environments (ModBE’13) in Milano, Italy, June 24, 2013. (2013) High-level Petri nets make models more concise and read- able as compared to low-level Petri nets. However, usual verification techniques such as state space analysis remain an open challenge for both ... [more ▼] High-level Petri nets make models more concise and read- able as compared to low-level Petri nets. However, usual verification techniques such as state space analysis remain an open challenge for both because of state space explosion. The contribution of this paper is to propose an approach for property based reduction of the state space of Algebraic Petri nets (a variant of high-level Petri nets). To achieve the objective, we propose a slicing algorithm for Algebraic Petri nets (APNSlicing). The proposed algorithm can alleviate state space even for certain strongly connected nets. By construction, it is guaranteed that the state space of sliced net is at most as big as the original net. We exemplify our technique through the running case study of car crash management system. [less ▲] Detailed reference viewed: 57 (8 UL)Survey of Petri nets Slicing Khan, Yasir Imtiaz ; Guelfi, Nicolas Report (2013) Petri nets slicing is a technique that aims to improve the verification of systems modeled in Petri nets. Different Petri nets slicing constructions are studied along with algorithms to compute them ... [more ▼] Petri nets slicing is a technique that aims to improve the verification of systems modeled in Petri nets. Different Petri nets slicing constructions are studied along with algorithms to compute them. Petri nets slicing was first developed to facilitate debugging but then devel- oped for alleviating the state space explosion problem for model checking Petri nets. This article has twofold objectives, the first is to unify all the existing slicing algorithms syntactically by the definition of a standard abstract syntax and rewriting of the studied slicing algorithms using the proposed syntax. The second is to discuss the contribution of each slicing construction and comparing the major differences between them. One of the interesting exploitation of the survey is for the selection and im- provement of slicing techniques for approaches concerned by optimizing verification of state event models. [less ▲] Detailed reference viewed: 262 (10 UL)Optimizing algebraic petri net model checking by slicing Khan, Yasir Imtiaz Report (2013) Detailed reference viewed: 68 (4 UL)Language Enrichment for Resilient MDE Khan, Yasir Imtiaz ; in Lecture Notes in Computer Science (2012, September 27), 7527 n Model-Driven Engineering, as in many engineering approaches, it is desireable to be able to assess the quality of a system or model as it evolves. A resilient engineering practice systematically ... [more ▼] n Model-Driven Engineering, as in many engineering approaches, it is desireable to be able to assess the quality of a system or model as it evolves. A resilient engineering practice systematically assesses whether evolutions improve on the capabilities of a system. We argue that to achieve a systematic resilient model-driven engineering practice, resilience concepts should be first-class citizens in models. This article discusses how DREF, a formal framework defining resilience concepts, can be integrated with other modeling languages in order to pursue a resilient development process. [less ▲] Detailed reference viewed: 170 (5 UL)A formal approach for engineering resilient car crash management system Khan, Yasir Imtiaz Report (2012) Detailed reference viewed: 93 (3 UL) |
||