Technical information

The Program Verification System (PVS) is a formal verification system developed by SRI International. PVS provides a rich specification language based on a strongly-typed higher-order logic and a powerful theorem prover for this logic. The PVS type system supports sub-typing and dependent types. The theorem prover includes decision procedures and simplification strategies for a variety of theories.

PVS is a key component of several formal verification projects at NASA Langley. For that reason, NASA Langley supports a PVS Research effort that aims at the advancement of theorem proving techniques for complex safety-critical applications. The Formal Methods group at NASA Langley, in collaboration with the PVS community, develops and maintains the PVS NASA Libraries, a large collection of PVS developments that range from fundamental mathematical theories to frameworks for the verification of air traffic systems and fault-tolerant protocols.

PVS runs on Linux, Solaris, and Mac OS X. Participants of the PVS Class 2012 are expected to have the latest version of PVS, currently 5.0 (Allegro binaries are suggested), and the latest version of the NASA PVS Libraries, currently 5.8, installed in their laptops. Please, follow the provided instructions to install these libraries in your system. Ask the organizers if you have problems installing PVS or the NASA Libraries. The PVS Class 2012 lectures, exercises, and solutions are electronically available as compress files (tgz, zip). An ISO image file (370Mb) of a CD containing all the material prepared for this class is also avialable. Browse the content of the CD through the file pvsclass2012/index.html.

There is not a native Windows version of PVS. However, PVS can be installed in a virtual Linux machine, which can be executed in a Windows platform using a virtualizer tool such a VirtualBox, VMWare, etc. As a convenience to attendants bringing Windows laptops, we have prepared a virtual Ubuntu 12.04 machine, for VirtualBox. See instructions below for downloading and installing the pre-configured virtual machine. The virtual machine already includes everything that is needed for the PVS Class 2012 (you don't need to download these files, they are alreay included in the virtual machine hard drive):

• Ubuntu 12.04,
• PVS 5.0 (Allegro or SBCL binaries),
• NASA PVS Libraries 5.8,
• PVS manuals, and
• PVS Class 2012 lectures, exercises, and solutions.

How to Install Pre-configured Ubuntu 12.04 VirtualBox Machine

The pre-condigured virtual machine is largely platform-independent and can be used under any host supported by Virtual Box, e.g., Windows, Linux, and Mac OS X.

To create the pre-configured virtual machine in your laptop (host), you need to download these files:

1. VirtualBox 4.2 (select the appropriate package depending on your laptop's platform);
2. (optional) VirtualBox 4.2 Oracle VM VirtualBox Extension Pack, only if you want to be able to access from your virtual machine a laptop's USB flash drive;
3. one of the following compressed files containing the virtual hard drive of the pre-configured Ubuntu machine. These files are 1.8G, please be patient.
   • Allegro binaries (recommeded): NASA-NIA_PVS_Class_2012.vdi.zip. It is faster and more thoroughly tested. However, it requires a click-through licence.
   • SBCL binaries: NASA-NIA_PVS_Class_2012_SBCL.vdi.zip or NASA-NIA_PVS_Class_2012_SBCL.vdi.gz. These machines are freely available.

Once you have installed VirtualBox and, optionally, the Extension Pack, and uncompressed the file NASA-NIA_PVS_Class_2012.vdi.zip (or NASA-NIA_PVS_Class_2012_SBCL.vdi.zip or NASA-NIA_PVS_Class_2012_SBCL.vdi.gz), follow these steps to create a virtual machine in VirtualBox:

1. Launch VirtualBox
2. Click New, give a name to the machine, e.g., PVSClass2012, its type is Linux, and its version Ubuntu. Click Continue.
3. Accept the recommended base memory and click Continue.
4. Select Use an existing virtual hard drive file and click on the small folder icon to open a file browser.
5. Select the file NASA-NIA_PVS_Class_2012.vdi in the file browser and click Create.

More detailed explanations for creating a virtual machine in VirtualBox are provided here.

We recommend that you create a directory in your laptop to be shared with your virtual machine. A shared directory is a convenient way to transfer files between your laptop and the virtual machine. To configure a shared directory between the laptop and the virtual machine, follow these steps:

1. Go to the VirtualBox window and click Settings (make sure that the machine that is selected is the one you just created).
2. In the pop-up window, click Shared Folders.
3. Click on the small folder icon to add a new folder share definition.
4. In Folder Path, select the directory in your laptop to be shared with the virtual machine.
5. Write sharedbox in Folder Name.
6. Check the box Auto-mount and, if there is one, the box Make Permanent.
7. Click OK.

Now, you are ready to execute the virtual machine. Go again to the VirtualBox window, make sure that the machine that is selected is the one you just created, and click Start. If everything goes well you will have our pre-configured Ubuntu machine up and running in your laptop. The default user of the machine is guest and its password is also guest.

In the virtual machine, you can launch PVS 5.0 directly from the side bar of the Ubuntu interface. Just click on the PVS icon. PVS 5.0 is installed in the directory PVS-5.0 and the default context directory is PVS-5.0/pvsclass2012/exercises. We have copied all the exercises into this directory. Hence, once you launch PVS by using the icon in the side bar you are ready to start working on the PVS Class 2012. Solutions to the exercises are available in PVS-5.0/pvsclass2012/solutions, but don't look at them yet.

In the desktop of your Ubuntu virtual machine, there are three shortcuts:

• Shared Host Box points to the shared directory /media/sharedbox between the laptop and the virtual machine.
• PVS-5.0 Documents points to the directory PVS-5.0/doc that contains PVS manuals.
• PVS Class 2012 points to the program and lectures of the PVS Class 2012.

If you want to be able to access from your virtual machine a USB memory pen plugged to your laptop, you have to install VirtualBox 4.2 Oracle VM VirtualBox Extension Pack in your laptop. Once this package is installed, follow these steps:

1. Go to VirtualBox, select the machine you just created (if it isn't already selected), and click on Settings.
2. In the pop-up window, click on Ports and then on USB.
3. Check the box Enable USB 2.0 (EHCI) Controller.
4. Click the first small USB icon on the left side of the USB Device Filters list area to create a filter with default values.
5. Click OK.

When using a USB flash drive from the virtual machine, make sure the drive is inserted after the virtual machine is up and running.

Enjoy It!

Note About Uncompressing zip And gz Files

Both Mac OS X and Windows have standard tools for uncompressing zip files. However, those tools don't handle very well large files, such as the virtual hard drives provided here. The uncompressed file is 4.7 G. The message in Windows 7 about needing additional 734TB is, of course, an error. It has been reported that the following tools correctly uncompress those files:

• Windows: 7 Zip
• Mac OS X: Ez7z (also available from the App Store)

Files with extension gz can be uncompressed with gunzip, which is standard in Linux and Mac OS X. For Windows, see the Gzip web site.