|
Published Articles >> Table of Contents >> Abstract
13th IEEE International Workshop on Rapid System Prototyping (RSP'02)
p. 99
Validating Objected-Oriented Prototype of Real-Time Systems with Timed Automata
Guoqiang Shu, Chinese Academy of Sciences
Chao Li, Chinese Academy of Sciences
Qing Wang, Chinese Academy of Sciences
Mingshu Li, Chinese Academy of Sciences
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/IWRSP.2002.1029744
Send link to a friend
| Abstract |
|
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.
|
 Additional Information
|
Citation:
Guoqiang Shu, Chao Li, Qing Wang, Mingshu Li,
"Validating Objected-Oriented Prototype of Real-Time Systems with Timed Automata,"
rsp,
p. 99,
13th IEEE International Workshop on Rapid System Prototyping (RSP'02),
2002
|
|
