Automatic Inference and Effective Application of Temporal Specifications - Mining Software Specifications: Methodologies and Applications - page 282

TABLE 8.6: Results of Checking Daisy Properties with Java PathFinder

JPF Found
Violation?

No Causing Event ( P ) Effect Event ( S or S|T )

1 Daisy.ialloc() DaisyDisk.writeAllocBit(blockno, ...)

2 Daisy.creat() Daisy.ialloc()

3 Daisy.creat() Daisy.ialloc()

4 Daisy.creat() DaisyDisk.writeAllocBit(blockno, ...)

5 Daisy.get_attr(inodeno, ...) Daisy.get_attr(inode, ...)

6 Daisy.ialloc() Daisy.ialloc()

7 Daisy.ialloc() DaisyDisk.writeAllocBit(blockno, ...)



8 Daisy.iget(inodeno) DaisyDisk.readi(inodeno, inode)



9 Daisy.iget(inodeno) DaisyLock.acqi(inodeno)



10 Daisy.iget(inodeno) DaisyLock.reli(inodeno)

11 Daisy.read(inodeno, ...) Daisy.read(inode, ...) 

12 Daisy.write(inodeno, ...) Daisy.write(inode, ...) 

13 DaisyDir.writeLong(inodeno, ...) Utility.longToBytes(...)

14 DaisyDisk.readi(inodeno, inode) DaisyLock.reli(inodeno)

15 DaisyLock.acqb(blockno) DaisyLock.relb(blockno)

16 DaisyLock.acqi(inodeno) DaisyDisk.readi(inodeno, inode) 



17 DaisyLock.acqi(inodeno) DaisyLock.reli(inodeno)

18 LockManager.acq(lockno) LockManager.rel(lockno) 

19 Mutex.acq() Mutex.rel() 

20 Petal.read(location, ...) RAF.length()

21 Petal.write(location, ...) RAF.writeByte(...)

22 RAF.seek(location) RAF.readByte() | RAF.writeByte(...) 