View   r8  >  r7  >  r6  >  r5  >  r4  ...

VerifingIntelFlashFilesystemCore 8 - 03 Jun 2008 - Main.MiguelFerreira
Line: 1 to 1
 

File System Layer Models

There has been a restructuring of all models, and for that, some of them aren't available yet.

Line: 28 to 28
 

VDM++ adapted for VdmHolTranslator and HOL translation

Changed:
<
<
  • [http://wiki.di.uminho.pt/twiki/pub/Research/VFS/VerifingIntelFlashFilesystemCore/src_alloy.tar.bz][src_vdm2hol.tar.gz]]: FileSystemLayer (VDM2HOL? )
>
>
Model
 
    • Implemented Operations:
      • FS_DeleteFileDir
    • Operations to be implemented:
Line: 37 to 38
 
      • FS_ReadFileDir
      • FS_Init
Changed:
<
<

HOL (hand written)

  • Will be published soon
>
>
Proof Obligations
 
Changed:
<
<

Proof Obligations

>
>
  • The VDMTools generated 13 Proof Obligations, from which:
    • 3 aren't translatable to HOL with the VdmHolTranslator. These can be found in the excluded.pog file
    • 10 where translated to HOL by the VdmHolTranslator. These can be found in the FileSystemLayerAlg.vpp.pog file.
      • 7 of these Proof Obligations where discharged in HOL using the Overture Automated Proof Support
      • for the remaining 3 Proof Obligations HOL attempted to prove for more than 5 minutes and was manually interrupted.

  • HOL model and Proof Obligations can be found in the:
    • FileSystemLayerAlg.vpp.pog.hol (for the unmodified version)
    • FileSystemLayerAlg.vpp.pog.hol.mod (for the executable version)
 
Deleted:
<
<
  • Proof obligations regarding invariant preservation and partial functions application:
    • Will be published soon
 
Changed:
<
<

Proof attempts with HOL

>
>

HOL (hand written)

 
  • Will be published soon
Line: 61 to 67
 
META FILEATTACHMENT attachment="src_vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++)" date="1211179529" name="src_vdm.tar.bz" path="src_vdm.tar.bz" size="6409" stream="src_vdm.tar.bz" user="Main.MiguelFerreira" version="2"
META FILEATTACHMENT attachment="src_alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy)" date="1211206760" name="src_alloy.tar.bz" path="src_alloy.tar.bz" size="6436" stream="src_alloy.tar.bz" user="Main.MiguelFerreira" version="3"
META FILEATTACHMENT attachment="ProofObligation_FSL_DeleteFileDir.txt" attr="h" comment="Proof Obligations for operation FS_DeleteFileDir" date="1204857290" name="ProofObligation_FSL_DeleteFileDir.txt" path="ProofObligation_FSL_DeleteFileDir.txt" size="8964" stream="ProofObligation_FSL_DeleteFileDir.txt" user="Main.MiguelFerreira" version="1"
Changed:
<
<
META FILEATTACHMENT attachment="src_vdm2hol.tar.gz" attr="h" comment="FileSystemLayer (VDM2HOL? )" date="1212493098" name="src_vdm2hol.tar.gz" path="src_vdm2hol.tar.gz" size="5885" stream="src_vdm2hol.tar.gz" user="Main.MiguelFerreira" version="1"
>
>
META FILEATTACHMENT attachment="src_vdm2hol.tar.gz" attr="h" comment="FileSystemLayer (VDM2HOL? )" date="1212504366" name="src_vdm2hol.tar.gz" path="src_vdm2hol.tar.gz" size="6551" stream="src_vdm2hol.tar.gz" user="Main.MiguelFerreira" version="2"

VerifingIntelFlashFilesystemCore 7 - 03 Jun 2008 - Main.MiguelFerreira
Line: 1 to 1
 

File System Layer Models

There has been a restructuring of all models, and for that, some of them aren't available yet.

Line: 26 to 26
 
      • FS_ReadFileDir
      • FS_Init
Changed:
<
<

VDM++ adapted for VdmHolTranslator

>
>

VDM++ adapted for VdmHolTranslator and HOL translation

 
Changed:
<
<
  • Will be published soon

HOL (translated from VDM++ model)

  • Will be published soon
>
>
  • [http://wiki.di.uminho.pt/twiki/pub/Research/VFS/VerifingIntelFlashFilesystemCore/src_alloy.tar.bz][src_vdm2hol.tar.gz]]: FileSystemLayer (VDM2HOL? )
    • Implemented Operations:
      • FS_DeleteFileDir
    • Operations to be implemented:
      • FS_OpenFileDir
      • FS_WriteFile
      • FS_ReadFileDir
      • FS_Init
 

HOL (hand written)

Line: 52 to 53
 

Proof attempts by hand (point free style)

  • Calculation of weakest pre-condition for preservation of referential integrity invariant on open files can be found here, on Lecture 5 (page 144).
Deleted:
<
<
  • More will be published soon
 
META FILEATTACHMENT attachment="alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy) sliced" date="1204856795" name="alloy.tar.bz" path="alloy.tar.bz" size="8367" stream="alloy.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="hol.tar.bz" attr="h" comment="FileSystemLayer? (HOL) sliced" date="1204856831" name="hol.tar.bz" path="hol.tar.bz" size="4600" stream="hol.tar.bz" user="Main.MiguelFerreira" version="1"
Line: 61 to 61
 
META FILEATTACHMENT attachment="src_vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++)" date="1211179529" name="src_vdm.tar.bz" path="src_vdm.tar.bz" size="6409" stream="src_vdm.tar.bz" user="Main.MiguelFerreira" version="2"
META FILEATTACHMENT attachment="src_alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy)" date="1211206760" name="src_alloy.tar.bz" path="src_alloy.tar.bz" size="6436" stream="src_alloy.tar.bz" user="Main.MiguelFerreira" version="3"
META FILEATTACHMENT attachment="ProofObligation_FSL_DeleteFileDir.txt" attr="h" comment="Proof Obligations for operation FS_DeleteFileDir" date="1204857290" name="ProofObligation_FSL_DeleteFileDir.txt" path="ProofObligation_FSL_DeleteFileDir.txt" size="8964" stream="ProofObligation_FSL_DeleteFileDir.txt" user="Main.MiguelFerreira" version="1"
Added:
>
>
META FILEATTACHMENT attachment="src_vdm2hol.tar.gz" attr="h" comment="FileSystemLayer (VDM2HOL? )" date="1212493098" name="src_vdm2hol.tar.gz" path="src_vdm2hol.tar.gz" size="5885" stream="src_vdm2hol.tar.gz" user="Main.MiguelFerreira" version="1"

VerifingIntelFlashFilesystemCore 6 - 23 May 2008 - Main.MiguelFerreira
Line: 1 to 1
 

File System Layer Models

Added:
>
>
There has been a restructuring of all models, and for that, some of them aren't available yet. If you are looking for any thing ins specific please contact us.
 

VDM++


VerifingIntelFlashFilesystemCore 5 - 19 May 2008 - Main.MiguelFerreira
Line: 1 to 1
 

File System Layer Models

Line: 57 to 57
 
META FILEATTACHMENT attachment="vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++) sliced" date="1204856873" name="vdm.tar.bz" path="vdm.tar.bz" size="4199" stream="vdm.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="vdm2hol.tar.bz" attr="h" comment="FileSystemLayer (VDM2HOL? ) sliced" date="1204856898" name="vdm2hol.tar.bz" path="vdm2hol.tar.bz" size="3923" stream="vdm2hol.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="src_vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++)" date="1211179529" name="src_vdm.tar.bz" path="src_vdm.tar.bz" size="6409" stream="src_vdm.tar.bz" user="Main.MiguelFerreira" version="2"
Changed:
<
<
META FILEATTACHMENT attachment="src_alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy)" date="1211179501" name="src_alloy.tar.bz" path="src_alloy.tar.bz" size="6370" stream="src_alloy.tar.bz" user="Main.MiguelFerreira" version="2"
>
>
META FILEATTACHMENT attachment="src_alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy)" date="1211206760" name="src_alloy.tar.bz" path="src_alloy.tar.bz" size="6436" stream="src_alloy.tar.bz" user="Main.MiguelFerreira" version="3"
 
META FILEATTACHMENT attachment="ProofObligation_FSL_DeleteFileDir.txt" attr="h" comment="Proof Obligations for operation FS_DeleteFileDir" date="1204857290" name="ProofObligation_FSL_DeleteFileDir.txt" path="ProofObligation_FSL_DeleteFileDir.txt" size="8964" stream="ProofObligation_FSL_DeleteFileDir.txt" user="Main.MiguelFerreira" version="1"

VerifingIntelFlashFilesystemCore 4 - 19 May 2008 - Main.MiguelFerreira
Line: 1 to 1
 

File System Layer Models

VDM++

Changed:
<
<
  • Sliced at FS_DeleteFileDir: vdm.tar.bz: FileSystemLayer (VDM++) sliced
>
>
    • Implemented Operations:
      • FS_DeleteFileDir
      • FS_OpenFileDir
      • FS_WriteFile
    • Operations to be implemented:
      • FS_ReadFileDir
      • FS_Init
 

Alloy

Changed:
<
<
  • Sliced at FS_DeleteFileDir: alloy.tar.bz: FileSystemLayer (Alloy) sliced
>
>
    • Implemented Operations:
      • FS_DeleteFileDir
    • Operations to be implemented:
      • FS_OpenFileDir
      • FS_WriteFile
      • FS_ReadFileDir
      • FS_Init
 

VDM++ adapted for VdmHolTranslator

Changed:
<
<
  • Sliced at FS_DeleteFileDir: vdm2hol.tar.bz: FileSystemLayer (VDM2HOL) sliced
>
>
  • Will be published soon

HOL (translated from VDM++ model)

  • Will be published soon
 
Changed:
<
<

HOL

>
>

HOL (hand written)

 
Changed:
<
<
  • Sliced at FS_DeleteFileDir: hol.tar.bz: FileSystemLayer (HOL) sliced
>
>
  • Will be published soon
 

Proof Obligations

Changed:
<
<
>
>
  • Proof obligations regarding invariant preservation and partial functions application:
    • Will be published soon

Proof attempts with HOL

  • Will be published soon

Proof attempts by hand (point free style)

 
Added:
>
>
  • Calculation of weakest pre-condition for preservation of referential integrity invariant on open files can be found here, on Lecture 5 (page 144).
  • More will be published soon
 
META FILEATTACHMENT attachment="alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy) sliced" date="1204856795" name="alloy.tar.bz" path="alloy.tar.bz" size="8367" stream="alloy.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="hol.tar.bz" attr="h" comment="FileSystemLayer? (HOL) sliced" date="1204856831" name="hol.tar.bz" path="hol.tar.bz" size="4600" stream="hol.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++) sliced" date="1204856873" name="vdm.tar.bz" path="vdm.tar.bz" size="4199" stream="vdm.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="vdm2hol.tar.bz" attr="h" comment="FileSystemLayer (VDM2HOL? ) sliced" date="1204856898" name="vdm2hol.tar.bz" path="vdm2hol.tar.bz" size="3923" stream="vdm2hol.tar.bz" user="Main.MiguelFerreira" version="1"
Changed:
<
<
META FILEATTACHMENT attachment="src_vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++)" date="1204857136" name="src_vdm.tar.bz" path="src_vdm.tar.bz" size="18535" stream="src_vdm.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="src_alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy)" date="1204857159" name="src_alloy.tar.bz" path="src_alloy.tar.bz" size="9568" stream="src_alloy.tar.bz" user="Main.MiguelFerreira" version="1"
>
>
META FILEATTACHMENT attachment="src_vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++)" date="1211179529" name="src_vdm.tar.bz" path="src_vdm.tar.bz" size="6409" stream="src_vdm.tar.bz" user="Main.MiguelFerreira" version="2"
META FILEATTACHMENT attachment="src_alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy)" date="1211179501" name="src_alloy.tar.bz" path="src_alloy.tar.bz" size="6370" stream="src_alloy.tar.bz" user="Main.MiguelFerreira" version="2"
 
META FILEATTACHMENT attachment="ProofObligation_FSL_DeleteFileDir.txt" attr="h" comment="Proof Obligations for operation FS_DeleteFileDir" date="1204857290" name="ProofObligation_FSL_DeleteFileDir.txt" path="ProofObligation_FSL_DeleteFileDir.txt" size="8964" stream="ProofObligation_FSL_DeleteFileDir.txt" user="Main.MiguelFerreira" version="1"

VerifingIntelFlashFilesystemCore 3 - 16 May 2008 - Main.MiguelFerreira
Line: 1 to 1
 

File System Layer Models

Line: 35 to 35
 
META FILEATTACHMENT attachment="src_vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++)" date="1204857136" name="src_vdm.tar.bz" path="src_vdm.tar.bz" size="18535" stream="src_vdm.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="src_alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy)" date="1204857159" name="src_alloy.tar.bz" path="src_alloy.tar.bz" size="9568" stream="src_alloy.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="ProofObligation_FSL_DeleteFileDir.txt" attr="h" comment="Proof Obligations for operation FS_DeleteFileDir" date="1204857290" name="ProofObligation_FSL_DeleteFileDir.txt" path="ProofObligation_FSL_DeleteFileDir.txt" size="8964" stream="ProofObligation_FSL_DeleteFileDir.txt" user="Main.MiguelFerreira" version="1"
Deleted:
<
<
META FILEATTACHMENT attachment="boneco1.png" attr="h" comment="First approach" date="1204857466" name="boneco1.png" path="boneco1.png" size="40551" stream="boneco1.png" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="boneco5.png" attr="h" comment="Point Free structure approach" date="1204858085" name="boneco5.png" path="boneco4.png" size="38692" stream="boneco4.png" user="Main.MiguelFerreira" version="2"
META FILEATTACHMENT attachment="translations_diagram.png" attr="h" comment="Translations diagram" date="1204858034" name="translations_diagram.png" path="translations_diagram.png" size="585517" stream="translations_diagram.png" user="Main.MiguelFerreira" version="1"

VerifingIntelFlashFilesystemCore 2 - 16 May 2008 - Main.JoseNunoOliveira
Line: 1 to 1
 

File System Layer Models

Line: 28 to 28
 
Deleted:
<
<

All-in-one Formal Methods

  • First approach
    boneco1.png

  • Point free structuring approach
    boneco5.png

  • Translation diagram:


    translations_diagram.png
 
META FILEATTACHMENT attachment="alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy) sliced" date="1204856795" name="alloy.tar.bz" path="alloy.tar.bz" size="8367" stream="alloy.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="hol.tar.bz" attr="h" comment="FileSystemLayer? (HOL) sliced" date="1204856831" name="hol.tar.bz" path="hol.tar.bz" size="4600" stream="hol.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++) sliced" date="1204856873" name="vdm.tar.bz" path="vdm.tar.bz" size="4199" stream="vdm.tar.bz" user="Main.MiguelFerreira" version="1"

VerifingIntelFlashFilesystemCore 1 - 07 Mar 2008 - Main.MiguelFerreira
Line: 1 to 1
Added:
>
>

File System Layer Models

VDM++

Alloy

VDM++ adapted for VdmHolTranslator

  • Sliced at FS_DeleteFileDir: vdm2hol.tar.bz: FileSystemLayer (VDM2HOL) sliced

HOL

  • Sliced at FS_DeleteFileDir: hol.tar.bz: FileSystemLayer (HOL) sliced

Proof Obligations

All-in-one Formal Methods

  • First approach
    boneco1.png

  • Point free structuring approach
    boneco5.png

  • Translation diagram:


    translations_diagram.png

META FILEATTACHMENT attachment="alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy) sliced" date="1204856795" name="alloy.tar.bz" path="alloy.tar.bz" size="8367" stream="alloy.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="hol.tar.bz" attr="h" comment="FileSystemLayer? (HOL) sliced" date="1204856831" name="hol.tar.bz" path="hol.tar.bz" size="4600" stream="hol.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++) sliced" date="1204856873" name="vdm.tar.bz" path="vdm.tar.bz" size="4199" stream="vdm.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="vdm2hol.tar.bz" attr="h" comment="FileSystemLayer (VDM2HOL? ) sliced" date="1204856898" name="vdm2hol.tar.bz" path="vdm2hol.tar.bz" size="3923" stream="vdm2hol.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="src_vdm.tar.bz" attr="h" comment="FileSystemLayer (VDM++)" date="1204857136" name="src_vdm.tar.bz" path="src_vdm.tar.bz" size="18535" stream="src_vdm.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="src_alloy.tar.bz" attr="h" comment="FileSystemLayer (Alloy)" date="1204857159" name="src_alloy.tar.bz" path="src_alloy.tar.bz" size="9568" stream="src_alloy.tar.bz" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="ProofObligation_FSL_DeleteFileDir.txt" attr="h" comment="Proof Obligations for operation FS_DeleteFileDir" date="1204857290" name="ProofObligation_FSL_DeleteFileDir.txt" path="ProofObligation_FSL_DeleteFileDir.txt" size="8964" stream="ProofObligation_FSL_DeleteFileDir.txt" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="boneco1.png" attr="h" comment="First approach" date="1204857466" name="boneco1.png" path="boneco1.png" size="40551" stream="boneco1.png" user="Main.MiguelFerreira" version="1"
META FILEATTACHMENT attachment="boneco5.png" attr="h" comment="Point Free structure approach" date="1204858085" name="boneco5.png" path="boneco4.png" size="38692" stream="boneco4.png" user="Main.MiguelFerreira" version="2"
META FILEATTACHMENT attachment="translations_diagram.png" attr="h" comment="Translations diagram" date="1204858034" name="translations_diagram.png" path="translations_diagram.png" size="585517" stream="translations_diagram.png" user="Main.MiguelFerreira" version="1"

Revision 8r8 - 03 Jun 2008 - 14:57:44 - MiguelFerreira
Revision 7r7 - 03 Jun 2008 - 12:35:38 - MiguelFerreira
Revision 6r6 - 23 May 2008 - 20:25:23 - MiguelFerreira
Revision 5r5 - 19 May 2008 - 14:19:20 - MiguelFerreira
Revision 4r4 - 19 May 2008 - 07:10:07 - MiguelFerreira
Revision 3r3 - 16 May 2008 - 08:48:46 - MiguelFerreira
Revision 2r2 - 16 May 2008 - 08:43:52 - JoseNunoOliveira
Revision 1r1 - 07 Mar 2008 - 02:53:53 - MiguelFerreira
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
Syndicate this site RSSATOM