Formal Analysis And Verification For Component-based Embedded Software Designs

In recent years, due to the widespread use of more powerful hardware in embeddedsystems, the size and complexity of embedded software are increasing rapidly, and theembedded software has been regarded as one of the most dominate factors in?uencingthe functionality and quality of the whole system. As a result of the requirements ofhigh reliability, real-time constraints, resource restrictions, and domain-specific adap-tation, embedded software presents many challenges, such as: how to check the timingand untiming consistency between the design models and the specifications, the com-patibility verification techniques for resource utilization, and the ways to analysis thesystem power consumption, etc. Therefore, how to design and implement embeddedsoftware e?ectively and reliably is becoming one of the hot research issues in nowadays.The component-based software design methodology has grown up as the main-stream in software engineering. By means of the construction and composition of thereusable software components, more complicated systems can be built e?ectively witha high reliability. Since generally an embedded system is composed of some interac-tive subsystems, the embedded software system shows more component-based featuresthan those general-purpose computing systems, and the system behavioral complexityis mostly exhibited by the scenarios of component interactions. As a formal languageinterface automata is designed to describe the temporal aspects of the component in-terfaces, and capture both the input assumptions and the output guarantees of thesoftware components. Hence, it's suitable for modelling and analyzing the component-based embedded software systems.In this thesis, we use the interface automata to model embedded software systemsand attack the analysis and verification problems of the functional and non-functionalproperties which are mostly concerned during the development of component-basedembedded software systems. The main contributions of our work are as follows:Firstly, for the problem of checking the system designs for scenario-based specifica-tions, we use the interface automaton networks to model the component-based systemdesigns which include a set of interface automata synchronized by shared actions, andthe scenario-based specifications are specified by UML sequence diagrams. Based oninvestigating the reachability graph of the state space of the interface automaton net-works, we develop several algorithms to check the existential consistency and mandatoryconsistency including the forward,backward and bidirectional consistency.Secondly, for real-time embedded software we consider the problem of checking component-based designs for scenario-based timing specifications. By adding time in-tervals on the actions, we extend the interface automata for modelling real-time systems.The component-based designs are modelled by real-time interface automaton networks,and the scenario-based timing specifications are specified by UML sequence diagramswith a set of boolean expressions. Based on analyzing the compatible integer state spaceof a real-time interface automaton networks and its compatible reachability graph, analgorithm is developed to check the consistency between real-time component-baseddesigns and the scenario-based timing specificationsThirdly, for the purpose of checking the compatibility of resource utilization inembedded software, a resource interface model is proposed by extending the interfaceautomata with a set of resource vectors, which indicate that how the resource usage ischanging along with the system behaviors. Through analyzing the reachability graphof the component-based designs which are modelled by resource interface automatonnetworks, we develop an algorithm to check wether the system resource constraints aremet or not. Moreover, we also give a solution to check the system designs for somespecific scenario-based specifications, which means that in some cases even the amountof resources are not enough, those special system functions could be still maintained.Fourthly, in order to analysis and make an estimation of the system energy con-sumption e?ectively, which are very important in the power limited system designs, weestablish an energy interface model by introducing the energy consumption rates intothe real-time interface automata. For the problems of minimum consumption estima-tion and maximum consumption verification, two algorithms are proposed respectivelybased on checking the state space of the energy interface automaton networks.Lastly, a prototype is designed to implement the algorithms presented in aboveresearch work. It can be used as an automatic validation tool in the component-basedembedded software system designs.