NDLI: Validating objected-oriented prototype of real-time systems with timed automata

Content Provider	IEEE Xplore Digital Library
Author	Guoqiang Shu Chao Li Qing Wang Mingshu Li
Copyright Year	2002
Description	Author affiliation: Inst. of Software, Chinese Acad. of Sci., China (Guoqiang Shu; Chao Li; Qing Wang; Mingshu Li)
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 the constraint 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 at the end of the paper.
Sponsorship	IEEE Comput. Soc. Tech. Committee on Simulation IEEE Comput. Soc. Tech. Committee on Design Autom
Starting Page	99
Ending Page	106
File Size	426827
Page Count	8
File Format	PDF
ISBN	076951703X
ISSN	10746005
DOI	10.1109/IWRSP.2002.1029744
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2002-07-01
Publisher Place	Germany
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Prototypes Real time systems Automata Unified modeling language Object oriented modeling Timing Formal verification Chaos Logic Software prototyping
Content Type	Text
Resource Type	Article
Subject	Computer Science

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Validating objected-oriented prototype of real-time systems with timed automata (2002)

A timed automata semantics for real-time UML specifications

OCL goes real-time

OBSERV-a prototyping language and environment combining object oriented approach, state machines and logic programming

Validating EAST-ADL Timing Constraints Using UPPAAL

A performance prototyping approach to designing concurrent software architectures

An approach towards formal verification of object oriented real-time systems

Prototyping distributed systems using an object-oriented specification language

UPPAAL-based software-defined network verification

Validating objected-oriented prototype of real-time systems with timed automata

Similar Documents

Validating objected-oriented prototype of real-time systems with timed automata (2002)

A timed automata semantics for real-time UML specifications

OCL goes real-time

OBSERV-a prototyping language and environment combining object oriented approach, state machines and logic programming

Validating EAST-ADL Timing Constraints Using UPPAAL

A performance prototyping approach to designing concurrent software architectures

An approach towards formal verification of object oriented real-time systems

Prototyping distributed systems using an object-oriented specification language

UPPAAL-based software-defined network verification

Validating objected-oriented prototype of real-time systems with timed automata