VDM to HOL model and proof obligation translation

One recent addition to the Overture project is an Automatic Proof Support system, developed by Sander Vermolen.

In our work we make much use of this system's translator, as well as the proof tactics.

We have contributed in widening the translator VDM++ syntax knowledge, implementing some basic (but essential to have recursive functions translated) operators like hd (head), tl (tail), len (length) and ^(concatenation).

Another contribution is the pre-processing script and parsers, that allow us to automaticaly pre process a VDM++ model to be translated (including its proof obligations), the complete package with source can be found here.

Verifiable Filesystem

The formal methods community has decided to challenge software developers to use formal methods techniques, in order to specify/model "big" software systems. Such software artifacts would then be a part of the Verifiable Software Repository.

One of the challenges released intended to specify the standard POSIX 1003.1, which is in fact an enormous task. So, Rajeev Joshi and Gerard J. Holzmann have proposed a so-called mini-challenge that focus on building a verifiable file system that follows the POSIX guide lines. Furthermore, the proponents of the mini-challenge have also introduced a project carried out at NASA Jet Propulsion Laboratory, whose goal is to build such a verifiable file system but designed for use directly in Flash Memories.

The main goal of this project is to respond to such a mini-challenge, taking in account the Flash Memory specific aspects including hardware support for the file system, following established techniques as well as new insights on how to use and apply formal methods in a system wide development.

Publications

• (pdf) Presentation on the VDM-Overture Workshop, FM08, Turku, 26 May 2008
• M.A. Ferreira, J.N. Oliveira: An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model. SBMF 2009: 153-169
• M.A. Ferreira: Verifying Intel (R) Flash File System Core. Master Thesis, Minho University, 2009.
• J.N. Oliveira. Hands on a Verification Challenge: Proving a Journaled File System Correct. Inforum 2010 (invited talk), 10-Sep 2010.
• J.N. Oliveira and M.A. Ferreira. Alloy Meets the Algebra of Programming: a Case Study. Journal paper. IEEE Trans. on Soft. Engineering, 2012 (in print).

Modeling and Verifying a File System with Journaling

In a simplified approach, we used Alloy and point free manual proofs to build and verify a file system model with journaling functionality. We started with a high level file system model and refined it into a low-level implementation over an array of nodes. See J.N. Oliveira and M.A. Ferreira. Alloy Meets the Algebra of Programming: a Case Study. Journal paper. IEEE Trans. on Soft. Engineering, 2012 (in print) for a full explanation of the Alloy model.

All-in-one Verification Life-cycle

Our approach resorts to the VDMTools proof obligation generator and the VDM to HOL translator developed by Sander Vermolen. The VDM to Alloy conversion is manual. In this "all-in-one" approach, modeling and testing takes place in the VDM phase. Alloy is particularly helpful in finding counter examples to proof obligations.

• First approach
  

• Translation diagram:
  
  
  

• Second approach
  In the second approach to the project we decided to reduce the complexity of the tool-chain and focus on the two bottom blocks --- Alloy model written in the "navigation-syle" so as to match with PF relation algebraic proofs. This implied that a focus on particular aspects of the problem, namely the journaling mechanism.

Verifying Intel Flash File System Core

File System Layer Models

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++

• src_vdm.tar.bz: FileSystemLayer (VDM++)
  • Implemented Operations:
    • FS_DeleteFileDir
    • FS_OpenFileDir
    • FS_WriteFile
  • Operations to be implemented:
    • FS_ReadFileDir
    • FS_Init

Alloy

• src_alloy.tar.bz: FileSystemLayer (Alloy)
  • Implemented Operations:
    • FS_DeleteFileDir
  • Operations to be implemented:
    • FS_OpenFileDir
    • FS_WriteFile
    • FS_ReadFileDir
    • FS_Init

VDM++ adapted for VdmHolTranslator and HOL translation

Model

• src_vdm2hol.tar.gz: FileSystemLayer (VDM2HOL)
  • Implemented Operations:
    • FS_DeleteFileDir
  • Operations to be implemented:
    • FS_OpenFileDir
    • FS_WriteFile
    • FS_ReadFileDir
    • FS_Init

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)

HOL (hand written)

• Will be published soon

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).

VDM to HOL model and proof obligation translation

One recent addition to the Overture project is an Automatic Proof Support system, developed by Sander Vermolen.

In our work we make much use of this system's translator, as well as the proof tactics.

We have contributed in widening the translator VDM++ syntax knowledge, implementing some basic (but essential to have recursive functions translated) operators like hd (head), tl (tail), len (length) and ^(concatenation).

Another contribution is the pre-processing script and parsers, that allow us to automaticaly pre process a VDM++ model to be translated (including its proof obligations), the complete package with source can be found here.

Team

• JoseNunoOliveira
• MiguelFerreira [ miguel(at)di(dot)uminho(dot)pt ]
• SamuelSilva [ silva(dot)samuel(at)alumni(dot)uminho(dot)pt ]

Web References

Flash File System

• (pdf) Intel Flash File System Core Reference Guide (Version 1)

POSIX File Store (GC)

• (pdf) Morgan and Sufrin's paper on the Unix filing system. (Z)
• (pdf) POSIX file store in Z/Eves: an experiment in the verified software repository
• (ppt) Formal Modeling and Analysis of a Flash Filesystem in Alloy.
• (pdf) Verifiable POSIX file store, technical report. (VDM)
• (pdf) Open Nand Flash Interface, technical report. (VDM)

Formal Methods Projects and Tools

• Overture - Open-source Tools for Formal Modelling
• VDMTools
• Alloy
• HOL

Conferences and Workshops

• ABZ call for papers on the POSIX pilot project in the Grand Challenge
• VDM-Overture 4th Workshop, FM08, Turku, 26 May 2008
• Pilot Projects for the Grand Challenge in Verified Software, FM08, Turku, 27 May 2008
• Workshop on the Verifiable File Store Mini-Challenge, BCS offices, London, 18 Dec 2007

Other

• Verified File-System
• OLVER (Open Linux VERification)
• Linux

Project Activities

• ProjectFiles at Trac

Research/VFS Web Utilities

-- MiguelFerreira - 15 Nov 2007

• Research/VFS Web
• Create New Topic
• Index
• Search
• Changes
• Notifications
• Statistics
• Preferences

• Main Webs

•  DI
•  EL
•  Education
•  Events
•  JoseLuisSilva
•  Personal
•  Research

Research/VFS Web Preferences

The following settings are web preferences of the Research.VFS web. These preferences overwrite the site-level preferences in TWiki.TWikiPreferences and Main.TWikiPreferences, and can be overwritten by user preferences (your personal topic, eg: TWikiGuest in the Main web).

Web Preferences Settings

These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.

• List of topics of the Research/VFS web:
  • #Set WEBTOPICLIST = Changes | Index | Search | Go

• Web-specific background color: (Pick a lighter one of the StandardColors).
  • Set WEBBGCOLOR = #D0D0D0
  • Note: This setting is automatically configured when you create a web

• Image, URL and alternate tooltip text of web's logo.
  Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.
  • #Set WEBLOGOIMG = /twiki/pub/Main/LocalLogos/um_eengP.jpg
  • #Set WEBLOGOURL = http://di.uminho.pt/
  • #Set WEBLOGOALT = DIUM

• List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Research/VFS.Topic links.
  Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
  
  • Set SITEMAPLIST = on
  • Set SITEMAPWHAT = Verifiable File System
  • Set SITEMAPUSETO =
  • Note: Above settings are automatically configured when you create a web

• Exclude web from a web="all" search: (Set to on for hidden webs).
  • Set NOSEARCHALL =
  • Note: This setting is automatically configured when you create a web

• Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
  • #Set NOAUTOLINK =
  • Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.

• Default template for new topics for this web:
  • WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
  • TWiki.WebTopicEditTemplate: Site-level default topic template

• Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
  • Set WEBFORMS =

• Users or groups who are not / are allowed to view / change / rename topics in the Research/VFS web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
  • #Set DENYWEBVIEW =
  • #Set ALLOWWEBVIEW =
  • #Set DENYWEBCHANGE =
  • Set ALLOWWEBCHANGE = TWikiAdminGroup, JoseNunoOliveira, MiguelFerreira, SamuelSilva, ClaudiaNecco
  • #Set DENYWEBRENAME =
  • #Set ALLOWWEBRENAME = TWikiAdminGroup

• Users or groups allowed to change or rename this WebPreferences topic: (e.g., TWikiAdminGroup)
  • #Set ALLOWTOPICCHANGE = TWikiAdminGroup
  • Set ALLOWTOPICRENAME = TWikiAdminGroup

• Web preferences that are not allowed to be overridden by user or topic preferences:
  • Set FINALPREFERENCES = NOSEARCHALL, ATTACHFILESIZELIMIT, WIKIWEBMASTER, WEBCOPYRIGHT, WEBTOPICLIST, DENYWEBVIEW, ALLOWWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME

Web Style

• • Set SKINSTYLE = Squash
  • Set STYLEVARIATION = subway
  • Set STYLEBORDER = thin
  • Set STYLEBUTTONS = on
  • Set STYLESIDEBAR = right
  • Set STYLESEARCHBOX = off

Help on Preferences

• A preference setting is defined by:
  3 or 6 spaces * Set NAME = value
  Example:
  • Set WEBBGCOLOR = #FFFFC0
• A preferences setting can be disabled with a # sign. Remove the # sign to enable a local customisation. Example:
  
  • #Set DENYWEBCHANGE = UnknownUser
• Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
  • When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
• The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
• You can introduce your own preferences variables and use them in your topics and templates.

Related Topics

• TWiki.TWikiPreferences, Main.TWikiPreferences - site-level preferences
• TWikiUsers - list of user topics. User topics can have optional user preferences
• TWikiVariables - list of common %VARIABLES%
• TWikiAccessControl - explains how to restrict access by users or groups

Tools

• Rename, move or delete this web:
  • Rename/move/delete web..., looking for references in all public webs - See also: ManagingWebs

Warning

Can't INCLUDE TWiki.WebSearchAdvanced repeatedly, topic is already included.

Statistics for Research/VFS Web

Notes:

• Do not edit this topic, it is updated automatically. (You can also force an update)
• TWikiDocumentation tells you how to enable the automatic updates of the statistics.
• Suggestion: You could archive this topic once a year and delete the previous year's statistics from the table.

• MeetingsSummary
• NewsFlash
• ProjectFiles
• ResearchStudies
• VdmHolTranslation
• VerifingIntelFlashFilesystemCore
• WebAtom
• WebChanges
• WebHome
• WebIndex
• WebLeftBar
• WebNotify
• WebPreferences
• WebReferences
• WebRss
• WebSearch
• WebSearchAdvanced
• WebSideBar
• WebStatistics
• WebTopicCreator
• WebTopicList

See also the verbose WebIndex.