Validation of requirements for embedded software using petri nets

Abstract

Embedded systems are utilized as a part of a wide range of spectrum extending from home apparatuses and cell phones to medical apparatus and transport controllers. They are commonly portrayed by their real-time behavior and must satisfy strict requirements on reliability and accuracy. The key challenge in real time system analysis is that proper scheduling strategy needs to be assured. So, the validation of requirements for these systems must be assured. Petri net is a formal and executable modeling technique, most suitably used for analysis of any concurrent system. There are a number of tools based on Petri net theory for analysis of models that help the users to graphically analyze a model, simulate them through an animated sequence and use them to validate the process. In this thesis, the proposed approach makes an attempt to model and analyze a case study on real time system i.e., Elevator Control System. First, the system is modeled using Colored Petri nets which can acquire the essential properties of the system and allow its illustration at different level of granularity. Second, after modeling the system, performance analysis is carried out using Stochastic Petri nets to analyze various aspects of the system. Third, verification and validation of the model is conducted using TAPAAL tool of Petri nets to check the correctness and to prove whether certain properties, demonstrated as computational tree logic formulas, hold concerning the system model. The use of three Petri net tools for analysis of any real time system helps to validate the work flow and subsequently, proper design of software architecture.