Correctness Checking using Formal Verification

This is project which tries to equip Ptolemy II with abilities to test the correctness of a system using formal verification. Currently we develop code generators to convert Ptolemy II models into files accepted by model-checkers such as SMV (or NuSMV ), REDLIB, or Real Time Maude.

Demonstrations

See also:
Kyungmin Bae, Peter Csaba Olveczky, Thomas Huining Feng, Stavros Tripakis. Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude, ICFEM '09: Proceedings of the 11th International Conference on Formal Engineering Methods, 717-736, 9, December, 2009.

Demo 1:Traffic light example

This demonstration and most of the demonstrations below require that NuSMV be installed.
  1. Open $PTII/ptolemy/verification/demo/SimpleTrafficLight/SimpleTrafficLight.xml
  2. Double click on the MathematicalModelConverter (Pink color).
  3. A dialog box will appear, asking you to input a temporal logic formula. Type
    ! EF ( CarLightNormal.state =  Cgrn & PedestrianLightNormal.state =  Pgreen)
    
    You may want to copy and paste the above line; it would be a lot faster than typing it.
  4. Press Convert. The code accepted by NuSMV will be generated. You can thus save the file (use .smv as the extension).
  5. Invoke NuSMV or SMV to see if the property is hold. You can also invoke the model checker directly in the MathematicalModelConverter actor without generating the file (choose output type: Invoke NuSMV; provided that the path variable has been correctly set up).
  6. Now modify the model by opening the PedestrianLightNormal actor, redirect the transition from Pgreen to Pred by creating a self loop in Pgreen (you can move the arrow pointed to Pred back to Pgreen). In this way, the model is no longer correct. Perform verification again, and the result would be false with a counter example.
  7. For models in the DE domain, an example with detailed instructions can be found in $PTII/ptolemy/verification/demo/SimpleTrafficLight/SimpleTrafficLightDECTA.xml. This example requires the installation of the real-time model checker RED 7.0.

Demo 2: Generate the specification directly from the graph

In this demo, we are experimenting methods to alleviate designers' burden on writing the specification themselves. A simple solution is to generate the specification graphically. For reachability properties, this can be done easily by annotating properties on states.

  1. Open $PTII/ptolemy/verification/demo/SimpleTrafficLight/SimpleTrafficLightGraphicalSpec.xml
  2. Right click on the FMVCarlightNormal actor and select "Open Actor". Note that now the in FMVCarlightNormal actor, the state Cgrn is red, and so is the state Pgreen in FMVPedestrianLightNormal.
  3. Double click on the MathematicalModelConverter (Pink color).
  4. A dialog box will appear, ask you to input temporal formula. This time, for the formula type, choose Risk. You don't need to type the formula. The specification will be annotated automatically in the file based on red-labeled states.
  5. To generate an automaton with the ability to annotate risk/reachability properties, you can open an FMVAutomaton editor from File -> New - > Fmv Automaton editor, or you can drag an instance in the graph editor (More Libraries -> CodeGenerators -> Verification -> FmvAutomaton).

Demo 3: SMVLegacyCodeActor

The SMVLegacyCodeActor can be viewed as a preliminary version of code-generation helpers. The user can specify functionalities written in SMV, and the MathematicalModelConverter would append it to the generated file. In fact, a code-generation helper for a particular actor can be viewed as a template; the information for the actor and relevent ports is annotated to the template as the converted result.

  1. Open $PTII/ptolemy/verification/demo/SimpleTrafficLight/SimpleTrafficLightSMVModule.xml
  2. You can open the PedestrianLightSMV actor, and you can find some code written in formats acceptable by SMV.
  3. Double click on the MathematicalModelConverter (Pink color)
    ! EF (CarLightNormal.state = Cgrn & PedestrianLightSMV.state = Pgreen)
      
    You may want to copy and paste the above line; it would be a lot faster than typing it.
  4. Perform the verification.

Another example: Railroad control

Another example can be found in $PTII/ptolemy/verification/demo/RailroadControl/RailroadControl.xml.

A larger example in robotic controller design (reactive control)

A relatively larger example can be found in $PTII/ptolemy/verification/demo/iRobotHillClimbing/iRobotCreateVerification.xml. Note that this model is not intended for simulation but only to illustrate the verification capability.

Real Time Maude code generation and verification

A simple example that use the Ptolemy II code generator to generate Real Time Maude may be found at $PTII/ptolemy/demo/SimpleTrafficLight/SimpleTrafficLightRTMaudeCG.xml.

An example that shows the capability to generate models acceptable by the Real Time Maude tool, and how these models can be verified using this tool, can be found in https://ptolemy.berkeley.edu/ptolemyII/ptII8.0/ptII/ptolemy/codegen/rtmaude/demo/HierarchicalTrafficLight/HierarchicalTrafficLight.xml. ($PTII/ptolemy/codegen was removed between Ptolemy II 8.0 and 10.0)

Installing NuSMV

Install NuSMV by downloading from its website.

For Mac OS X 10.8, see https://www.macupdate.com/app/mac/46133/nusmv.

For Mac OS X 10.7, try Mac Ports. After installing Mac Ports, try

sudo port install nusmv
This should create /opt/local/bin/nusmv.

Installing REDLIB (RED 7.0)

Install RED 7.0 by downloading from its website

Installing Real Time Maude

Install Real Time Maude by downloading from its website.

Integrating verification engines using the EmbeddedCActor

To perform full integration of verification process, we also experiment how to embed verification engines into the Ptolemy II architecture. Currently we are able to integrate NuSMV into Ptolemy II, where code modification is minor (<100 lines + 1 file renaming). The core technique is to use EmbeddedCActor instead of using Java Native Interface directly (it is relatively complicated for C++ programmers to learn Java and JNI). Therefore, for researchers willing to use Ptolemy II as their front-end, this offers excellent guidance.

Limitations

  1. This is a highly preliminary code generator facility, with many limitations. It is best viewed as a concept demonstration. Currently it may analyze a single FSMActor, and a system consisting of multiple FSMActors or ModalModels (with state or SR refinement) interacting with SMVLegacyCodeActors in the SR domain. For models in the DE domain, we also perform preliminary experiments, see $PTII/ptolemy/verification/demo/SimpleTrafficLight/SimpleTrafficLightDECTA.xml
  2. We find some examples having minor problems executing under NuSMV while they are executable under SMV. These problems can be easily fixed: the instructions in the corresponding model files show how to do this. Our preliminary diagnosis is that there are small syntactic differences between SMV and NuSMV.
  3. The DE conversion mechanism in MathematicalModelConverter.java adapts current implementation of DE semantics and disallows the use of super dense time; the semantics is slightly different compared to the semantics specified in the technical report:

    Chihhong Patrick Cheng, Teale Fristoe and Edward A. Lee, Applied Verification: The Ptolemy Approach, EECS Department University of California, Berkeley Technical Report No. UCB/EECS-2008-41 April 19, 2008