Applying Floyd’s Inductive Assertions Method for Verification of Generalized Net Models Without Temporal Components
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2018, Vol 9, Issue 9
Abstract
Generalized Nets are extensions of Petri Nets. They are a suitable tool for describing real sequential and parallel processes in different areas. The implementation of correct Generalized Nets models is a task of great importance for the creation of a number of applications such as transportation management, e-business, medical systems, telephone networks, etc. The cost of an error in the models of some of these applications can be very high. The implementation of models of similar applications has to use formal approaches to prove that the developed models are correct. A foundation stone of software verification, which is suitable for verification of Generalized Nets models with transitions without temporal component, is Floyd’s inductive assertion method. This article presents a modification of Floyd’s inductive assertion method for verification of flowcharts, which allows Generalized Nets without temporal component to be verified. Using an illustrative example, we show that the offered adaptation is appropriate for the purpose of training university students in the Informatics and Computer Sciences in formal methods of verification.
Authors and Affiliations
Magdalina Todorova, Nora Angelova
Keywords
Related Articles
- EP ID EP394072
- DOI 10.14569/IJACSA.2018.090958
- Views 119
- Downloads 0
Impact of Different Data Types on Classifier Performance of Random Forest, Naïve Bayes, and K-Nearest Neighbors Algorithms
This study aims to evaluate impact of three different data types (Text only, Numeric Only and Text + Numeric) on classifier performance (Random Forest, k-Nearest Neighbor (kNN) and Naïve Bayes (NB) algorithms). The class...
A Survey of Energy Aware Cloud’s Resource Allocation Techniques for Virtual Machine Consolidation
As the demand for cloud computing environment is increasing, new techniques for making cloud computing more environment-friendly are being proposed with an aim to convert traditional cloud computing into green cloud comp...
Implementation of Binary Search Trees Via Smart Pointers
Study of binary trees has prominent place in the training course of DSA (Data Structures and Algorithms). Their implementation in C++ however is traditionally difficult for students. To a large extent these difficulties...
An Enhanced Concept based Approach for user Centered Health Information Retrieval to Address Readability Issues
Searching for relevant medical guidance has turn out to be a general and notable task executed by internet users. This diversity of quantifiable information explorers indicates the enormous range of information needs and...
A Systematic Literature Review of Success Factors and Barriers of Agile Software Development
Motivator and demotivator plays an important role in software industry. It encompasses software performance and productivity which are necessary for projects of Agile software development (ASD). Existing studies comprise...