A Statechart Verification Tool For Automotive Electronics-Smart Automata

In the development work of automotive electronics software, the use of method based model is surprisingly increasing. Considered as the important part of the method based model, Verification become the most concerned technical problem by the software engineer. The main focus of this thesis is how to validate the statechart to increase the efficiency and safety of the automotive electronics software development.The main research purpose of this thesis is to provide users of statechart with a visual modeling, simulation and verification tool, which can help users efficiently model statechart to communicate with the other engineers, simulate the statechart to position the logic error, validate the statechart to check the system design. With the aid of this tool, users can concentrate on the modeling, found error of design problem as soon as possible, and thus can highly improve the efficiency of development work of automotive electronics software.The main work of this thesis can be generalized as following:Firstly, it designs and implements a statechart modeling environment in the framework of SmartOSEK IDE, which can support the statechart model from the SmartOSEK IDE;Secondly, in order to implement the simulation of the statechart, it designs and implements a simulator, which can keep the result of the simulation by executing the action of the statechart dynamically. it also can check the languages of the statechart before the simulation;At last, base on the simulation of the statechart, it designs and implements a verification engine of the statechart, which can help the user to find error of design and refine it as soon as possible.