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 117
- Downloads 0
Implementing and Comparison between Two Algorithms to Make a Decision in a Wireless Sensors Network
The clinical presentation of acute CO poisoning and hydrocarbon gas (Butane CAS 106-97-8) varies depending on terrain, humidity, temperature, duration of exposure and the concentration of gas toxic: From then consciousne...
An Electronic Intelligent Hotel Management System for International Marketplace
To compete with the international market place, it is crucial for hotel industry to be able to continually improve its services for tourism. In order to construct an electronic marketplace (e-market), it is an inherent r...
Finding Non Dominant Electrodes Placed in Electroencephalography (EEG) for Eye State Classification using Rule Mining
Electroencephalography is a measure of brain activity by wave analysis; it consist number of electrodes. Finding most non-dominant electrode positions in Eye state classification is important task for classification. The...
Anonymous Broadcast Messages
The Dining Cryptographer network (or DC-net) is a privacy preserving communication protocol devised by David Chaum for anonymous message publication. A very attractive feature of DC-nets is the strength of its security,...
Methodology for Selecting the Preferred Networked Computer System Solution for Dynamic Continuous Defense Missions
This paper presents a methodology for addressing the challenges and opportunities in defining and selecting the preferred Networked Computer System (NCS) solution in response to specified United States Defense mission pl...