Instrumentation of timed automatic for formal verification of timed properties
Department Of Electronics and Electrical
Project Details: In this thesis, an implementation of time measurement, in an already existing tool for modeling, simulation and verification of PRES+ models has been presented. PRES+, which is an extended timed Petri Net model, is very useful to represent embedded systems. As mentioned in the motivational example it is easy to understand the benefits of verification models. If we return to the example with the car on the road and reflects for a minute on the different components that have to work together, and in a strict order to accomplish the tasks of keeping the car on the road, or if the system fails, try to minimize possible human injuries. The need to be able to verify the embedded system working as predicted is obvious. Eachsystem has to, not only fulfill their own specifications, but also has to work in conjunction with each other. There would not be any meaning if the airbag fired after a crash already had taken place or if the antiskid system didn’t work together with the break control system. A verification tool like this, presented in this thesis can be used to verify each of the components functioning as specified, especially considering the issue of timeliness. Contributions made by this thesis are the added possibility to now measure time as stipulated by a logical formula and enabling translation of the formulas into the TA model. In the verification process the tool needs two inputs, one is the timed automata (TA) model and the other is a query that stipulates the given restrictions. The TA model itself easures
the time restrictions for each transition, while the new implementations that this thesis has presented, measures time from a stipulated start point in a system.
Abstract: Embedded systems are used in many technical products of today. The tendency also points to the fact that they are in many ways becoming more and more complex as technology advances. Systems like advanced avionics, air bags, ABS brakes or any real-time embedded system requires reliability, correctness and timeliness. This puts hard pressure on designers, analyzers and developers. The need for high performance and non failing systems has therefore led to a growing interest in modeling and verification of component-based embedded systems in order to reduce costs and simplify design and development. The solution proposed by the Embedded Systems Lab at Linköping University is the modeling language PRES+, Petri Net based Representation for Embedded Systems. PRES+ models are then translated into timed automata, TA, which is used by the UPPAAL verification tool. To be able to verify timing properties the translated TA model must be instrumented with certain timers, called clocks. These clocks must be reset in a manner reflected by the property to be verified.This thesis will provide a solution to the problem and also give the reader necessary information in order to understand the theoretical background needed. The thesis will also show the reader the importance of modeling and time verification in the development of embedded systems. A simple example is used to describe and visualize the benefit regarding real-time embedded systems as well as the importance of the ability to verify these systems. The conclusion drawn stresses the fact that high development costs, possible gain of human lives and the problems in developing complex systems only emphasize the need for easy-tohandle
and intuitive verification methods.
You can also Subscribe to PROJECTSWORLDS by Email for more Projects, Seminar Topics and Final Year Projects.
