NDLI: Specification of real-time systems using a timed automata model with shared variables and verification of partial-deadlock freeness

Content Provider	IEEE Xplore Digital Library
Author	Okano, K. Hattori, S. Yamamoto, A. Higashino, T. Taniguchi, K.
Copyright Year	1999
Description	Author affiliation: Graduate Sch. of Eng., Osaka Univ., Japan (Okano, K.)
Abstract	We propose a timed automata model with shared variables (TASV). A TASV is a set of extended timed automata (ETAs) with shared boolean variables. For this model, we propose (I) an algorithm which decides whether a given TASV is partial-deadlock free, and (2) a sufficient condition that we can efficiently prove a given TASV is partial-deadlock free. Each ETA in a TASV can access to /modify, shared boolean variables independently. By constructing a tuple automaton for all ETAs in a given TASV we can decide the existence of deadlocks. However, such an approach causes the state explosion problem. Our algorithm and our proposed sufficient condition reduce the possibility of the state explosion by dividing the ETAs into some sets and proving their partial-deadlock freeness independently.
Starting Page	576
Ending Page	581
File Size	100112
Page Count	6
File Format	PDF
ISBN	0769503535
DOI	10.1109/ICPPW.1999.800118
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1999-09-24
Publisher Place	Japan
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Real time systems Automata Time of arrival estimation Timing Formal specifications Sufficient conditions System recovery Explosions
Content Type	Text
Resource Type	Article

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

The specification and verification of Real-Time system based on the temporal logic of action

Model-driven specification of component-based distributed real-time and embedded systems for verification of systemic QoS properties

Specification and verification of real-time properties using LOTOS and SQTL

Timed Automata Patterns

Formal Specification and Verification of Real-Time Systems using Graph Grammars

Testing Deadlock-freeness in Real-time Systems; A Formal Approach

On the verification of nondeterministic automata specifications of probabilistic real-time systems (1999).

Formal specification and verification of components' real-time behavior

Timed Component-Interaction Automata for Specification and Verification of Real-Time Reactive Systems

Specification of real-time systems using a timed automata model with shared variables and verification of partial-deadlock freeness

Similar Documents

The specification and verification of Real-Time system based on the temporal logic of action

Model-driven specification of component-based distributed real-time and embedded systems for verification of systemic QoS properties

Specification and verification of real-time properties using LOTOS and SQTL

Timed Automata Patterns

Formal Specification and Verification of Real-Time Systems using Graph Grammars

Testing Deadlock-freeness in Real-time Systems; A Formal Approach

On the verification of nondeterministic automata specifications of probabilistic real-time systems (1999).

Formal specification and verification of components' real-time behavior

Timed Component-Interaction Automata for Specification and Verification of Real-Time Reactive Systems

Specification of real-time systems using a timed automata model with shared variables and verification of partial-deadlock freeness