[go: up one dir, main page]

Tripakis et al., 2001 - Google Patents

Analysis of timed systems using time-abstracting bisimulations

Tripakis et al., 2001

View PDF
Document ID
1399870573708999314
Author
Tripakis S
Yovine S
Publication year
Publication venue
Formal Methods in System Design

External Links

Snippet

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 …
Continue reading at www.researchgate.net (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/504—Formal methods
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/362—Software debugging
    • G06F11/3636—Software debugging by tracing the execution of the program
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3612—Software analysis for verifying properties of programs by runtime analysis
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/46—Multiprogramming arrangements
    • G06F9/54—Interprogramme communication; Intertask communication
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3668—Software testing
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/445—Programme loading or initiating
    • G06F9/44589—Programme code verification, e.g. Java bytecode verification, proof-carrying code
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5045—Circuit design
    • G06F17/505—Logic synthesis, e.g. technology mapping, optimisation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/30—Monitoring
    • G06F11/34—Recording or statistical evaluation of computer activity, e.g. of down time, of input/output operation; Recording or statistical evaluation of user activity, e.g. usability assessment
    • G06F11/3466—Performance evaluation by tracing or monitoring
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2201/00—Indexing scheme relating to error detection, to error correction, and to monitoring

Similar Documents

Publication Publication Date Title
Tripakis et al. Analysis of timed systems using time-abstracting bisimulations
Tripakis et al. Checking timed Büchi automata emptiness efficiently
Hance et al. Finding invariants of distributed systems: It's a small (enough) world after all
Cleaveland et al. The concurrency workbench
Laroussinie et al. CMC: A tool for compositional model-checking of real-time systems
Bouajjani et al. On-the-fly symbolic model checking for real-time systems
Pnueli et al. Liveness and acceleration in parameterized verification
Cordy et al. Behavioural modelling and verification of real-time software product lines
Constant et al. Integrating formal verification and conformance testing for reactive systems
Lomuscio et al. Bounded model checking for knowledge and real time
Bozga et al. Using static analysis to improve automatic test generation
Stengel et al. Analyzing singularity channel contracts
Abdulla et al. Constrained monotonic abstraction: A CEGAR for parameterized verification
Duret-Lutz Contributions to LTL and ω-Automata for Model Checking
Janowska et al. Slicing of timed automata with discrete data
Feautrier et al. Enhancing the compilation of synchronous dataflow programs with a combined numerical-boolean abstraction
Peled et al. Relaxed visibility enhances partial order reduction
Bensalem et al. A transformational approach for generating non-linear invariants
Dobrikov et al. Optimising the ProB model checker for B using partial order reduction
De Francesco et al. Abstract interpretation and model checking for checking secure information flow in concurrent systems
Egolf et al. Efficient synthesis of symbolic distributed protocols by sketching
Bošnački et al. Partial-order reduction for general state exploring algorithms
Ogata et al. Modeling and verification of real-time systems based on equations
van de Pol et al. Modal Abstractions in μ CRL
Corradini et al. Closed interval process algebra’versus ‘interval process algebra