Model Checking Based Formal Analysis And Verification For Component Oriented Embedded Software

In recent years, with wide application of embedded systems of which the performance of hardware equipment has been rapidly improved, the scale and complexity of embedded software are expanding rapidly, and the embedded software has been regarded as the most key factor to reliability and quality of the whole system. Therefore, the design methodology and reliability assurance for embedded software has become a hot issue of which software engineers and computer science researchers are common concern in nowadays. As a result of the traditional design approaches can not met the high reliability requirements of the modern high complexity and large scale embedded systems, the typical design mythology for high complexity software in software engineering field should be integrated into modern embedded software design.As one of the prevailing software engineering design approach, the component based design approach has been applied to complex embedded software design, which greatly improved the efficiency of software development and the reusability for software function. Embedded systems are usually composed of multiple domain specific computational sub modules, which are mutually independent and high similar to the component feature.In order to describe component interactive of embedded software, UML sequence diagram is adopted generally in the industry, which has the inherent limitation that is difficult to automatically analyzation and verification. The requirements for component interactive protocol modeling is thoroughly studied, component interactive protocol model based on first-order logic and commitment theory is proposed for database-driven embedded software, and component interactive protocol analyzing and resource constraint target planning means based on modeling checking technologies is given.The main contribution of this paper includes:(1) Proposed a fundamental component interactive protocol model for data-driven embedded software. Besides input-output signature for component actions, first-order logic rules are utilized for input data constraint rules, control flow rules, output rules and state changing rules, providing overall formal descriptions for component based embedded software behavior, making automatic analyzation and verification of component interactive protocols possible.(2) Based on the above fundamental component interactive protocol model, commitment theory based business component protocol model is proposed for giving business semantic to web component interactive protocol. This model labels business effects of component actions with domain business vocabulary. Different from traditional effect labeling, besides direct effects, commitment effects are allowed to be labeled, which models the contracting behavior between component and underlying hardware of embedded systems.(3) For formally describing component interactive protocol effectively, the verification problem of First-Order Linear Temporal Logic(FO-LTL) property of fundamental service protocol model is studied. Complex control and data flow properties of the interaction process of fundamental component interactive protocol can be expressed as FO-LTL formula. It can be proved that under conditions of input boundness, the LTL-FO property verification problem of fundamental component interactive protocol is decidable. The decision algorithm for FO-LTL property of fundamental component protocol is given and corresponding model checker MC4 CIP is implemented. Experimental result shows that MC4 CIP can do effective verification under various scenarios.(4) Towards property verification of business component interactive protocol, an extension of FO-LTL, named FOCT-LTL, is proposed with commitment extension. Commitment expression can be used as atom in property formulas. By reducing the FOCT-LTL property verification of business component protocol into the LTL-FO property verification of fundamental protocol, the decidability of FOCT-LTL verification problem of business component protocol under input boundness condition is also proved and can be directly solved with the FO-LTL property verification algorithm of fundamental protocol.(5) The embedded software resource restricted target planning problem of business component interactive protocol is also addressed. Resource restricted goal can be expressed with combination of LTL-FOSC formula and constraint expressions, allowing service consumer to express functional goal and data. A three-step planning algorithm based on model checking is designed for the above goal. In the first step, bounded model checking techniques are used to quickly rule out business component protocols that are impossible to meet resource restricted requirements. During the second step, the plan of first step is used for reduction the FOCT-LTL of business component protocol for getting a feasible solution that satisfies functional requirements. In the final step, by constraint solving technology the satisfiability of resource restricted goal of embedded software requirement is further verified. Experimental results show that the above three-step approach has practically acceptable verification capability.