Research On On-the-fly Verification Techniques For Embedded Software Designs

Model-based techniques for system designs and analysis can effectively satisfy high reliability requirements of modern embedded software system. Embedded software has the requirements of high reliability, real-time constraints, resource restrictions, and domain-specific adaptation with respect to general systems. Therefore, how to guarantee system designs meet the given function specification and the non-function restriction is becoming one of the active research issues in embedded computing domain currently.In embedded computing domain, traditional methods mostly concern the implementation and testing phrase, without effective tools supporting the analysis and verification of the system designs in the design phrase. In this thesis, we do research on On-the-fly verification techniques for embedded software designs. We use UML interactive overview diagram as the scenario-based specification and the interface automata and its extension models to model embedded software systems. Then, we develop several algorithms based on On-the-fly verification mechanism to attack the analysis and verication problems of the functional and non-functional properties which are mostly concerned during the development of embedded software systems.Based on the theory, an improved version of prototype T-CBESD (Tool for Component-Based Embedded Software Designs) has been designed and implemented as a plug-in module on the open-source platform Eclipse. The work includes: expanding the input interface, improving the core algorithms, and demonstrating the efficiency and accuracy of the new algorithnms with two examples. The improved version of prototype T-CBESD provides effective model-based On-the-fly verification tool for the designs and analysis of modern embedded software system.