Correctness Checking using Formal Verification

Demonstrations

• Demo 1: Traffic light example
• Demo 2: Generate the specification directly from the graph
• Demo 3: SMVLegacyCodeActor
• Another demo: Railroad control
• A larger example in robotic controller design (reactive control)
• Demo: Generating Real Time Maude code
• Installing NuSMV
• Installing REDLIB (RED 7.0)
• Installing Real Time Maude
• Integrating verification engines using the EmbeddedCActor
• Limitations

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

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

A larger example in robotic controller design (reactive control)

Real Time Maude code generation and verification

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

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

Installing REDLIB (RED 7.0)

Installing Real Time Maude

Integrating verification engines using the EmbeddedCActor

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