13th IEEE International Workshop on Rapid System Prototyping (RSP'02) Validating Objected-Oriented Prototype of Real-Time Systems with Timed Automata Darmstadt, Germany July 01-July 03 ISBN: 0-7695-1703-X
Object-oriented development of real-time systems is becoming more and more prevalent. Unified Modeling Language (UML) is a standardized notation for describing object-oriented software design. While using UML to specify real-time systems, the formal validation of certain timing constraints becomes critical for the success of object-oriented development of real-time systems. Current development methods of real-time systems have not provided consistent support for verifying UML models of real-time systems. This paper presents a formal specification & validation method, FORTS, for object-oriented real-time system development using UML. The method presents a real-time extension of UML; describes the formal semantics of the UML extension; provides automatic transformation of UML models into timed automata; and verifies timing assertions presented by UML sequence diagram using model checking and constraints solving technique. With tool support, FORTS conceals the complicated details of formal validation for users, thus providing the benefits of formal methods without bringing additional burden. A case study is presented in the end of the paper.
Citation:
Guoqiang Shu, Chao Li, Qing Wang, Mingshu Li, "Validating Objected-Oriented Prototype of Real-Time Systems with Timed Automata," rsp, pp.99, 13th IEEE International Workshop on Rapid System Prototyping (RSP'02), 2002 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||