NDLI: Analysis of Timed Systems Using Time-Abstracting Bisimulations

Content Provider	Springer Nature Link
Author	Tripakis, Stavros Yovine, Sergio
Copyright Year	2001
Abstract	The objective of this paper is to show how verification of dense-time systems modeled as timed automata can be effectively performed using untimed verification techniques. In that way, the existing rich infrastructure in algorithms and tools for the verification of untimed systems can be exploited. The paper completes the ideas introduced in (Tripakis and Yovine, 1996, in Proc. 8th Conf. Computer-Aided Verification, CAV'96, Rutgers, NJ. LNCS, Vol. 1102, Springer-Verlag, 1996, pp. 232–243).Our approach consists in two steps. First, given a timed system A, we compute a finite graph G which captures the behavior of A modulo the fact that exact time delays are abstracted away. Then, we apply untimed verification techniques on G to prove properties on A. As property-specification languages, we use both the linear-time formalism of timed Büchi automata (TBA) and the branching-time logic TCTL. Model checking A against properties specified as TBA or TCTL formulae comes down to applying, respectively, automata-emptiness or CTL model-checking algorithms on G.The abstraction of exact delays is formalized under the concept of time-abstracting bisimulations. We define three time-abstracting bisimulations which are strictly ordered with respect to their reduction power. The stronger of them preserves both linear- and branching-time properties whereas the two weaker ones preserve only linear-time properties.The finite graph G is the quotient A with respect to a time-abstracting bisimulation. Generating G is called minimization and can be done by adapting a partition-refinement algorithm to the timed case. The adapted algorithm is symbolic, that is, equivalence classes are represented as simple polyhedra. When these polyhedra are not convex, operations become expensive, therefore, we develop a partition-refinement technique which preserves convexity.We have implemented the minimization algorithm in a prototype module called minim, as part of the real-time verification platform KRONOS (Bozga et al., 1998, in CAV'98). minim connects KRONOS to the CADP tool suite for the verification of untimed graphs (Fernandez et al., 1992, in 14th Int. Conf. on Software Engineering). To demonstrate the practical interest behind our approach, we present two case studies, namely, Fischer's mutual exclusion protocol and the CSMA/CD communication protocol.
Starting Page	25
Ending Page	68
Page Count	44
File Format	PDF
ISSN	09259856
Journal	Formal Methods in System Design
Volume Number	18
Issue Number	1
e-ISSN	15728102
Language	English
Publisher	Kluwer Academic Publishers
Publisher Date	2001-01-01
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Software Engineering/Programming and Operating Systems Computer-Aided Engineering (CAD, CAE) and Design Electronic and Computer Engineering
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Software Hardware and Architecture

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

Forward Analysis of Updatable Timed Automata

Symbolic Verification and Analysis of Discrete Timed Systems

Verification of Real-Time Systems using Linear Relation Analysis

Performance analysis of probabilistic timed automata using digital clocks

On using priced timed automata to achieve optimal scheduling

Robust safety of timed automata

MSO logics for weighted timed automata

Model checking for probabilistic timed automata

Timed verification of the generic architecture of a memory circuit using parametric timed automata

Analysis of Timed Systems Using Time-Abstracting Bisimulations

Similar Documents

Forward Analysis of Updatable Timed Automata

Symbolic Verification and Analysis of Discrete Timed Systems

Verification of Real-Time Systems using Linear Relation Analysis

Performance analysis of probabilistic timed automata using digital clocks

On using priced timed automata to achieve optimal scheduling

Robust safety of timed automata

MSO logics for weighted timed automata

Model checking for probabilistic timed automata

Timed verification of the generic architecture of a memory circuit using parametric timed automata

Analysis of Timed Systems Using Time-Abstracting Bisimulations