Research On Interface Automata Based Embedded Software Verification Techniques And Supporting Tools

High reliability requirements of modern embedded software system need effective model-based techniques for system designs and analysis. As a result of the requirements of high reliability, real-time constraints, resource and energy restriction, how to make the system design consistent with the function specification and the non-function restriction is becoming one of the active research issues in embedded computing domain currently. Traditional methods in embedded computing domain 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, interface automata and its extension models are used as the design model of the component-based embedded software, and UML sequence diagram is used as the scenario-based specification. Several abstract verification algorithms based on interface automata and its extension models have been analyzed, then the implementation frames have been designed. On this foundation, a prototype T-CBESD (Tool for Component-Based Embedded Software Designs) has been designed, which is based on the theory of interface automata and is implemented as a plug-in module on the open-source platform Eclipse. The tool accepts UML sequence diagrams as the input system specification directly, checking several different kinds of behavioral consistency problems between the system design models and scenario-based specifications. By using timing constraint inequality of message events, the tool can verify whether the behaviors in real-time interface networks satisfy the sequence diagrams with real-time limitations. In addition, the tool can analyze and verify the non-realtime resource usage characterization and realtime energy usage characterization. The design and implementation of this work include the input/output mechanisms, the pre-translation from sequence diagrams to a set of message event sequences, the state space data structure designs, detail implementation issues of several verification algorithms and lastly ,through two case studies, this model checking tool is demonstrated on application to embedded software system design.