← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2009/pierre-clavel-leveugle/Fault-tolerance/README.txt

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2009/pierre-clavel-leveugle/Fault-tolerance/README.txt
 
1
 
 
2
TIMA Laboratory, Grenoble, France
 
3
March 2009
 
4
--------------------------------
 
5
 
 
6
The books of this directory are associated with the ATM example given in 
 
7
section 5.2 of the paper:
 
8
"ACL2 for the Verification of Fault-Tolerance Properties: First Results",
 
9
L.Pierre, R.Clavel, R.Leveugle,
 
10
Proc. International Workshop On The ACL2 Theorem Prover and Its 
 
11
Applications, Boston (MA), May 2009.
 
12
 
 
13
Files:
 
14
 
 
15
- error-model.lisp: error model of section 4.1
 
16
 
 
17
- register.lisp: simple architecture for the component REG (neither 
 
18
detection nor correction mechanism)
 
19
 
 
20
- register-det.lisp: second architecture for the component REG (section 
 
21
5.2.1), equipped with an error detection mechanism
 
22
 
 
23
- register-TMR.lisp: third architecture for the component REG (section 
 
24
5.2.1), TMR register
 
25
 
 
26
- ATM-det.lisp: ATM system version 1 (section 5.2.2), all the registers 
 
27
are instances of register-det
 
28
 
 
29
- ATM-TMR.lisp: ATM system version 2 (section 5.2.2), all the registers 
 
30
are instances of register-TMR