Name
Abstract | ||
|---|---|---|
Temporal logic model checking is a technique for the auto- matic verification of systems against specifications. Besides the correctness of safety and liveness properties it is often important to determine critical answer and delay times of systems, especially if they are embedded in a real-time envi- ronment. In this paper we present an approach which allows the verification as well as the timing analysis of real- time systems. The systems are described as networks of communicating time-extended finite state machines (I/O- interval structures). We use a compact symbolic representa- tion to obtain efficient analysis algorithms. 1 |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1145/343647.343775 | Design, Automation, and Test in Europe |
Keywords | Field | DocType |
real-time system,extended finite state machine,automata,formal verification,finite state machines,system on a chip,timing analysis,intellectual property,production systems,model checking,real time systems,logic simulation,algorithm design and analysis,cores,temporal logic,real time | Model checking,Computer science,Correctness,Finite-state machine,Real-time computing,Static timing analysis,Logic simulation,Temporal logic,Formal verification,Liveness | Conference |
ISBN | Citations | PageRank |
1-58113-244-1 | 5 | 0.80 |
References | Authors | |
12 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jürgen Ruf | 1 | 122 | 23.04 |
| Thomas Kropf | 2 | 326 | 59.09 |