SmartOSEK IDE3.0 And Its Model Checking And Codesign

In automotive industry, software's share is surprisingly increasing. This makes the development of automotive electronics become a important part of automotive industry. The main focus of this thesis is how to accelerate reliable software development process by using Model Based Design methodology and some Integrated Development Tools corresponding.SmartOSEK IDE3.0 is a visual, graphic, hierarchical integrated development environment, which can help users to implement Model Based Design (MBD) during their work. And this MDB method can provide users more software reliability and development enficiency.SmartOSEK IDE3.0 provides 5 layers of modeling environments from system layer to component layer, a whole suit of model confirming and system testing tools, capable of designing models for algorithms, code generation and document generation, design and implement a component-based hierarchical modeling language for automotive electronics—SmartC and a suit of SmartC development tools. The IDE primarily including hierarchical modeling environment, SmartC error detecting system, tracing and debugging system, system schedulability analysis tool, SmartC code auto-generation, C code auto-generation, document auto-generation and SmartC library with sustainable and extensible feature.The main work of this thesis can be generalized as following:Firstly, it brings Model Based Design methodology into Chinese automotive industry and its electronic system design. Design and implement SmartOSEK IDE3.0 based no MBD.Secondly, design and implement SmartVerficator to convert model to Timed Automata. Thus implement the verfication of model state.Thirdly, design and implement a service for cooperative work. Many users can analyze the same code file at the some time by using this service. It improves large efficiency of analysis. This service is implemented as client and server (CS) architecture.At last, it invents a method to get the schedulability of a Real-time system besed on simulating. Implement dynamic and static schedulability Analysis tools for Real-time systems.