测试用例生成是软件测试的关键.根据U ML statecharts的层次和并发结构,研究相应的测试用例产生方法.它视复合状态为抽象状态,分别构造主UML statecharts和复合状态所对应的子UML statecharts的测试基,并依据一定的合成规则和Wp-方法生...测试用例生成是软件测试的关键.根据U ML statecharts的层次和并发结构,研究相应的测试用例产生方法.它视复合状态为抽象状态,分别构造主UML statecharts和复合状态所对应的子UML statecharts的测试基,并依据一定的合成规则和Wp-方法生成整个U ML statecharts的测试用例.这种方法能够支持递增式测试用例的生成.理论和实验结果说明,如果满足测试条件,它们保证全故障覆盖,且产生较少的测试用例.这种改进对大型复杂系统尤其有效,也便于构造自动测试工具。展开更多
Formal verification has been widely needed in the development of safety critical systems. In order to introduce the design verification activity in UML developing process, we have developed a verifier of UML Statechar...Formal verification has been widely needed in the development of safety critical systems. In order to introduce the design verification activity in UML developing process, we have developed a verifier of UML Statecharts by using the model checker SMV. The approach is to transform a system model in UML Statecharts to one in SMV input language via an intermediate language and then to verify the system properties specified in CTL by invoking SMV. The current experiences, including the formal verification of a simplified directory based cache coherence protocol in UML Statecharts, show that automatic verification can be integrated as a new step of the software process nicely.展开更多
This paper focuses on the performance analysis of flexible reactive systems. The performance analysis consists of two phases： first system modeling, second performance evalua-tion. The paper models the flexible react...This paper focuses on the performance analysis of flexible reactive systems. The performance analysis consists of two phases： first system modeling, second performance evalua-tion. The paper models the flexible reactive system by the stochas-tic statecharts method, and uses the simulation method to evalu-ate the performance. To make use of the feature of event-triggered state transitions in the statecharts, a new method of simulation is proposed based on the techniques of the discrete-event system simulation. The new method solves the problem of computer imple-mentation of stochastic events, probabilistic transition, concurrent states, paral el actions, and broadcast communication mechanism in the stochastic statecharts. An example of a flexible manufactur-ing system is presented. The simulation result of the example is consistent with the analytical result, which shows the feasibility of the proposed new simulation method.展开更多
The formal modelling and verification method has become an effective way of improving the reliability and correctness of complex,safety-critical embedded systems.Statecharts are widely used to formally model embedded ...The formal modelling and verification method has become an effective way of improving the reliability and correctness of complex,safety-critical embedded systems.Statecharts are widely used to formally model embedded applications,but they do not realise the reasonable separation of system concerns,which would result in code scattering and tangling.Aspect-Oriented Software Development(AOSD)technology could separate crosscutting concerns from core concerns and identify potential problems in the early phase of the software development life cycle.Therefore,the paper proposes aspect-oriented timed statecharts(extended timed statecharts with AOSD)to separately model base functional requirements and other requirements(e.g.,scheduling,error handling),thereby improving the modularity and development efficiency of embedded systems.Furthermore,the dynamic behaviours of embedded systems are simulated and analysed to determine whether the model satisfies certain properties(e.g.,liveness,safety)described by computation tree logic formulae.Finally,a given case demonstrates some desired properties processed with respect to the aspect-oriented timed statecharts model.展开更多
Product data management (PDM) has been accepted as an important tool for the manufacturing industries. In recent years, more and mor e researches have been conducted in the development of PDM. Their research area s in...Product data management (PDM) has been accepted as an important tool for the manufacturing industries. In recent years, more and mor e researches have been conducted in the development of PDM. Their research area s include system design, integration of object-oriented technology, data distri bution, collaborative and distributed manufacturing working environment, secur ity, and web-based integration. However, there are limitations on their rese arches. In particular, they cannot cater for PDM in distributed manufacturing e nvironment. This is especially true in South China, where many Hong Kong (HK) ma nufacturers have moved their production plants to different locations in Pearl R iver Delta for cost reduction. However, they retain their main offices in HK. Development of PDM system is inherently complex. Product related data cover prod uct name, product part number (product identification), drawings, material speci fications, dimension requirement, quality specification, test result, log size, production schedules, product data version and date of release, special tooling (e.g. jig and fixture), mould design, project engineering in charge, cost spread sheets, while process data includes engineering release, engineering change info rmation management, and other workflow related to the process information. Accor ding to Cornelissen et al., the contemporary PDM system should contains manageme nt functions in structure, retrieval, release, change, and workflow. In system design, development and implementation, a formal specification is nece ssary. However, there is no formal representation model for PDM system. Theref ore a graphical representation model is constructed to express the various scena rios of interactions between users and the PDM system. Statechart is then used to model the operations of PDM system, Fig.1. Statechart model bridges the curr ent gap between requirements, scenarios, and the initial design specifications o f PDM system. After properly analyzing the PDM system, a new distributed PDM (DPDM) system is proposed. Both graphical representation and statechart models are constructed f or the new DPDM system, Fig.2. New product data of DPDM and new system function s are then investigated to support product information flow in the new distribut ed environment. It is found that statecharts allow formal representations to capture the informa tion and control flows of both PDM and DPDM. In particular, statechart offers a dditional expressive power, when compared to conventional state transition diagr am, in terms of hierarchy, concurrency, history, and timing for DPDM behavioral modeling.展开更多
Unified modeling language （UML） is a powerful graphical modeling language with intuitional meaning. It provides various diagrams to depict system characteristics and complex environment from different viewpoints and...Unified modeling language （UML） is a powerful graphical modeling language with intuitional meaning. It provides various diagrams to depict system characteristics and complex environment from different viewpoints and different application layers. UML-based software development and modeling environments have been widely accepted in industry, including areas in which safety is an important issue such as spaceflight, defense, automobile, etc. To ensure and improve software quality becomes a main concern in the field. As one of the key techniques for software quality, software testing can effectively detect system faults. UML based software testing based is an important research direction in software engineering. The key to software testing is the generation of test cases. This dissertation studies an approach to generating test cases from UML statecharts.展开更多
文摘测试用例生成是软件测试的关键.根据U ML statecharts的层次和并发结构,研究相应的测试用例产生方法.它视复合状态为抽象状态,分别构造主UML statecharts和复合状态所对应的子UML statecharts的测试基,并依据一定的合成规则和Wp-方法生成整个U ML statecharts的测试用例.这种方法能够支持递增式测试用例的生成.理论和实验结果说明,如果满足测试条件,它们保证全故障覆盖,且产生较少的测试用例.这种改进对大型复杂系统尤其有效,也便于构造自动测试工具。
基金supported by National Natural Science Foundation of China(6 99730 5 1) 86 3Project of China(86 3-30 6 -ZT0 6 -0 4-1) Huo Y
文摘Formal verification has been widely needed in the development of safety critical systems. In order to introduce the design verification activity in UML developing process, we have developed a verifier of UML Statecharts by using the model checker SMV. The approach is to transform a system model in UML Statecharts to one in SMV input language via an intermediate language and then to verify the system properties specified in CTL by invoking SMV. The current experiences, including the formal verification of a simplified directory based cache coherence protocol in UML Statecharts, show that automatic verification can be integrated as a new step of the software process nicely.
基金supported by the National Natural Science Foundation of China(61171120)
文摘This paper focuses on the performance analysis of flexible reactive systems. The performance analysis consists of two phases： first system modeling, second performance evalua-tion. The paper models the flexible reactive system by the stochas-tic statecharts method, and uses the simulation method to evalu-ate the performance. To make use of the feature of event-triggered state transitions in the statecharts, a new method of simulation is proposed based on the techniques of the discrete-event system simulation. The new method solves the problem of computer imple-mentation of stochastic events, probabilistic transition, concurrent states, paral el actions, and broadcast communication mechanism in the stochastic statecharts. An example of a flexible manufactur-ing system is presented. The simulation result of the example is consistent with the analytical result, which shows the feasibility of the proposed new simulation method.
基金supported by the National Natural Science Foundation of China under GrantsNo.61173048,No.61103115
文摘The formal modelling and verification method has become an effective way of improving the reliability and correctness of complex,safety-critical embedded systems.Statecharts are widely used to formally model embedded applications,but they do not realise the reasonable separation of system concerns,which would result in code scattering and tangling.Aspect-Oriented Software Development(AOSD)technology could separate crosscutting concerns from core concerns and identify potential problems in the early phase of the software development life cycle.Therefore,the paper proposes aspect-oriented timed statecharts(extended timed statecharts with AOSD)to separately model base functional requirements and other requirements(e.g.,scheduling,error handling),thereby improving the modularity and development efficiency of embedded systems.Furthermore,the dynamic behaviours of embedded systems are simulated and analysed to determine whether the model satisfies certain properties(e.g.,liveness,safety)described by computation tree logic formulae.Finally,a given case demonstrates some desired properties processed with respect to the aspect-oriented timed statecharts model.
文摘Product data management (PDM) has been accepted as an important tool for the manufacturing industries. In recent years, more and mor e researches have been conducted in the development of PDM. Their research area s include system design, integration of object-oriented technology, data distri bution, collaborative and distributed manufacturing working environment, secur ity, and web-based integration. However, there are limitations on their rese arches. In particular, they cannot cater for PDM in distributed manufacturing e nvironment. This is especially true in South China, where many Hong Kong (HK) ma nufacturers have moved their production plants to different locations in Pearl R iver Delta for cost reduction. However, they retain their main offices in HK. Development of PDM system is inherently complex. Product related data cover prod uct name, product part number (product identification), drawings, material speci fications, dimension requirement, quality specification, test result, log size, production schedules, product data version and date of release, special tooling (e.g. jig and fixture), mould design, project engineering in charge, cost spread sheets, while process data includes engineering release, engineering change info rmation management, and other workflow related to the process information. Accor ding to Cornelissen et al., the contemporary PDM system should contains manageme nt functions in structure, retrieval, release, change, and workflow. In system design, development and implementation, a formal specification is nece ssary. However, there is no formal representation model for PDM system. Theref ore a graphical representation model is constructed to express the various scena rios of interactions between users and the PDM system. Statechart is then used to model the operations of PDM system, Fig.1. Statechart model bridges the curr ent gap between requirements, scenarios, and the initial design specifications o f PDM system. After properly analyzing the PDM system, a new distributed PDM (DPDM) system is proposed. Both graphical representation and statechart models are constructed f or the new DPDM system, Fig.2. New product data of DPDM and new system function s are then investigated to support product information flow in the new distribut ed environment. It is found that statecharts allow formal representations to capture the informa tion and control flows of both PDM and DPDM. In particular, statechart offers a dditional expressive power, when compared to conventional state transition diagr am, in terms of hierarchy, concurrency, history, and timing for DPDM behavioral modeling.
文摘Unified modeling language （UML） is a powerful graphical modeling language with intuitional meaning. It provides various diagrams to depict system characteristics and complex environment from different viewpoints and different application layers. UML-based software development and modeling environments have been widely accepted in industry, including areas in which safety is an important issue such as spaceflight, defense, automobile, etc. To ensure and improve software quality becomes a main concern in the field. As one of the key techniques for software quality, software testing can effectively detect system faults. UML based software testing based is an important research direction in software engineering. The key to software testing is the generation of test cases. This dissertation studies an approach to generating test cases from UML statecharts.
