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.展开更多
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.展开更多
Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a...Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a formal method with precise syntax and semantics defined. System modeled by PVS specification could be verified by tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time systems. In this approach, we provide 1) a time-extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from a timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexibility and user friendliness in modeling, extendability in formalization and verification content, and better performance. Time constraints are modeled and verified and is a highlight of this paper.展开更多
Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development for models could be verified. Tools are needed for rigorous modeling of embedded real-time system. UML is an ind...Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development for models could be verified. Tools are needed for rigorous modeling of embedded real-time system. UML is an industrial standard modeling language which provides a powerful expressi-veness, intuitive and easy to use interface to model. UML is widely accepted by software developer. However, for lack of precisely defined semantics, especially on the dynamic diagrams, UML model is hard to be verified. PVS is a general formal method which provides a high-order logic specification language and integrated with model checking and theorem proving tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time system. In this approach, we provide 1) a timed extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexible and friendly in modeling, extendable in forma-lization and verification content, and better performance. Time constraints are modeled and verified and it’s a highlight of this paper.展开更多
A method for modeling crosscutting concerns in the concurrent software system is presented based on the aspect-oriented（A-O） technique and the statechart of unified modeling language （UML）. Modeled with UML statec...A method for modeling crosscutting concerns in the concurrent software system is presented based on the aspect-oriented（A-O） technique and the statechart of unified modeling language （UML）. Modeled with UML statechart diagrams, the primary system functions and corresponding traversal features are enveloped into various orthogonal regions of a composite state. The mutual relationships between orthogonal regions are implied by the orders of broadcast events. Using a modular transition system as a basic computational model, the formalization description of A-O statechart models is proposed. The precise semantics of model elements and modeling procedures is given. The example study indicates that the separation strategy of crosscutting concerns is implemented in the design phase of the concurrent software system with this method. Meanwhile, the software modeling method has advantages of loose coupling, adaptability and traceability.展开更多
基金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.
文摘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.
文摘Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a formal method with precise syntax and semantics defined. System modeled by PVS specification could be verified by tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time systems. In this approach, we provide 1) a time-extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from a timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexibility and user friendliness in modeling, extendability in formalization and verification content, and better performance. Time constraints are modeled and verified and is a highlight of this paper.
文摘Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development for models could be verified. Tools are needed for rigorous modeling of embedded real-time system. UML is an industrial standard modeling language which provides a powerful expressi-veness, intuitive and easy to use interface to model. UML is widely accepted by software developer. However, for lack of precisely defined semantics, especially on the dynamic diagrams, UML model is hard to be verified. PVS is a general formal method which provides a high-order logic specification language and integrated with model checking and theorem proving tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time system. In this approach, we provide 1) a timed extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexible and friendly in modeling, extendable in forma-lization and verification content, and better performance. Time constraints are modeled and verified and it’s a highlight of this paper.
文摘A method for modeling crosscutting concerns in the concurrent software system is presented based on the aspect-oriented（A-O） technique and the statechart of unified modeling language （UML）. Modeled with UML statechart diagrams, the primary system functions and corresponding traversal features are enveloped into various orthogonal regions of a composite state. The mutual relationships between orthogonal regions are implied by the orders of broadcast events. Using a modular transition system as a basic computational model, the formalization description of A-O statechart models is proposed. The precise semantics of model elements and modeling procedures is given. The example study indicates that the separation strategy of crosscutting concerns is implemented in the design phase of the concurrent software system with this method. Meanwhile, the software modeling method has advantages of loose coupling, adaptability and traceability.
