Study On The Application Of Formal Method In Component-based Real-time System

With the growth of software scale and complexity, the quality and reliability of the whole real-time system greatly depend on the efficient software development technique. These are strong motivations to apply new software engineering technique—Component-Based Software Development(CBSD).Component-Based Software Development represents a pattern of "reuse instead of reinvention". It shifts the emphasis on software development from scratches to reusing and assembling of ready-made components and has become mainstream in software technique domain due to its lower cost, shorter time and higher reliability. Nowadays, how to describe the dynamic behavior and how to composite ready-made components for application according to the system's function, real-time property and trustworthy attributes have become hot-topics in research domain, and formal method can satisfy the above demands well for its accuracy. Thus, a novel concept to combine CBSD and formal method for constructing trustworthy real-time system is introduce in this paper.Formal verification, adequate test and effective measurement are main trustworthy guarantee technique. So, formal methods, their corresponding model checking techniques and the theories of quality model of trusted component is applied to component modeling, verification of behavioral compatibility, test generation and component selection in thie thesis, aiming to construct a trustworthy component-based real-time system. The main contributions of this thesis are as follows:(1) This thesis gives a formal model of real-time component based on timed automata(TA) named RCM, and also how to construct the product of the RCM is introduced. The behavior of components is modeled by introducing the definition of "Action" and the time property is shown by clock constraint in the RCM. So the model can limit the behavior of real-time components by clock constraint and the set of clock to be reset. RCM can also indicate the composition relation of components. The advantage of the RCM is that it provides description of real-time property, dynamic behavior between components and the architecture information.(2) This thesis proposes a technique for behavioral compatibility analysis of component-based real-time system. The behavioral incompatibility of real-time system is often due to the inconsistency of clock constraints. So, how to describe and verify such behavioral incompatibility in an effective way should be taken more into consideration in real-time system component composition. First, the RCM based on timed automata is used to formally describe the component. In this way, the problem of component behavioral compatibility is equivalent to whether the complementary actions can really synchronize over common channels on the system's models. Then, the formulation of the behavioral compatibility verification is enabled as reachability properties that can be checked by reachability analysis of the model, and the verification function of the UPPAAL tool is used to generate the result. Finally, the method is applied to the composition of the railway level crossing control system, the results demonstrate the effectiveness and performance of the proposal. The obvious advantage of this method is the model of the component is explicit and the method is useful in sizeable component-composition systems, because model checking is often hampered by various state explosion problems, and in UPPAAL these problems are dealt with by a combination of on-the-fly verification together with a new and coarser symbolic technique reducing the verification problem to that of solving simple linear constraint systems.(3) This thesis introduces new coverage criteria and the method to automatically generate length optimal tests for real-time system. On the basis of behavioral compatibility, new coverage criteria concerning safety, time property and key behavioral compatibility for the abstract formal of real-time system are presented and enabled as reachability properties. The method makes use of the RCM to formally describe the real-time system and uses the length optimal reachability feature of UPPAAL to automatically generate length optimal test sequences for the new coverage criteria. Experiment demonstrates how the technique works and performs. In general, testing focusing on particular properties is effective, so tests generated in this method have higher coverage and efficiency than traditional ones.(4) This thesis provides a method for component selection and system reliability calculation. First, according to the hierarchy character of component-based software development, it makes use of the Hierarchical Automata(HA) to describe the component modules and the whole service system. Based on the interaction frequency among component modules, the relation matrix is introduced to calculate the importance factors contributing to the whole system. Wherein, to meet the system design requirement, a many-to-one mapping function is used to rank the importance into difference levels, each level corresponds to different quality criteria, which in return is used to select the appropriate components. Then, it proposes an algorithm to calculate the resulting system reliability. Finally, it studies a case to demonstrate the selection of components and the estimation of resulting reliability. Behavioral compatibility analysis of component-based system instructs component selection from behavior level, further more, this method from quality metrics. The obvious advantage of this method is that the model is easy to understand. Meanwhile, different trustworthy attributes are used as quality parameters, making the component selection and composition of the trustworthy software more effective.