Name
Abstract | ||
|---|---|---|
This paper presents a complete example of the use of the synchronous declarative language LUSTRE for the specification, description and verification of a resource arbiter, which is a regular network of hardware devices. The fact that both programs and properties may be expressed in LUSTRE is used to perform an inductive verification. An invariant property of the network is found, and merged with the description program. Verification is performed by model checking. |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1007/BF01185559 | Acta Inf. |
Keywords | Field | DocType |
Information System,Operating System,Data Structure,Communication Network,Information Theory | Specification language,Arbiter,Programming language,Model checking,Intelligent verification,Computer science,Theoretical computer science,Verification,Lustre (programming language),Declarative programming,Modular design | Journal |
Volume | Issue | ISSN |
29 | 6-7 | 0001-5903 |
Citations | PageRank | References |
26 | 6.45 | 22 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nicolas Halbwachs | 1 | 3957 | 426.43 |
| Fabienne Lagnier | 2 | 313 | 26.77 |
| Christophe Ratel | 3 | 209 | 18.84 |