JPF analysis of Java generated by a FSM

[adam ali]

Hello, I am looking for some help regarding a summer project at my university. Is there an existing project that uses JPF to analyze the Java code that is generated from a Finite State Machine? I was told there is an existing project but I cannot seem to find it. Any help would be greatly appreciated. 

Adam.

[Corina Pasareanu]

there is a project Polyglot that converts from Statecharts (not FSMs) into Java:

https://wiki.isis.vanderbilt.edu/MICTES/index.php/Publications

See also this paper:

Polyglot: Systematic Analysis for Multiple Statechart Formalisms (tool demo), Corina Pasareanu, Daniel Balasubramanian, Gabor Karsai and Michael Lowry. In TACAS 2013.

On Tue, May 7, 2013 at 10:18 AM, adam ali <fada...@gmail.com> wrote:

Hello, I am looking for some help regarding a summer project at my university. Is there an existing project that uses JPF to analyze the Java code that is generated from a Finite State Machine? I was told there is an existing project but I cannot seem to find it. Any help would be greatly appreciated. 

Adam.

--
 
---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[PETER C MEHLITZ]

that would be jpf-statechart (http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-statechart)
It uses it's own modeling language but it fairly general in terms what state machines you can model.

-- Peter

[adam ali]

Thanks for the tips. I was looking at the Statechart project and I see that they have a set of rules to translate the State chart into a Java program by hand. I am curious if there is an automatic translation tool available that can be used on my FSM. I will have a look at the Polygot project to see if it is what I am looking for. Thanks again for the quick response.

[Corina Pasareanu]

yes
the automatic tool is called Polyglot -- see the link above
it translates statecharts into java but it does not use jpf-statechart

sorry if we confuse you perhaps

corina

--

[Corina Pasareanu]

you just analyze the translated code with jpf (jpf-core) or spf (jpf-symbc)  (there is a special driver already generated for sym exe).

thanks

corina

[Corina Pasareanu]

if you download polyglot from the link above it contains documentation and also examples that show you how to run it (with spf)

[Adam Ali]

I have been looking at the examples from the "jpf-statechart" project and cannot seem to figure out how you are able to verify the example statecharts with JPF. I am able to see the .java files under the "default package" but why is there only 8 .jpf configuration files under the "jpfESAS" folder? My goal is to translate a statechart into java code (automatically if possible) and then to utilize JPF to check for assertion errors, deadlock, race conditions etc. I was able to utilize the Polyglot project and tools to generate java from .mdl files and run it with Symbolic Pathfinder, however I would like to use standard JPF on statechart generated Java. Eventually I would like to be able to verity multiple, communicating state machines with JPF.

> --
>
> ---
> You received this message because you are subscribed to a topic in the Google Groups "Java™ Pathfinder" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/java-pathfinder/2y7_bhtvfHA/unsubscribe?hl=en.
> To unsubscribe from this group and all its topics, send an email to java-pathfind...@googlegroups.com.

[Peter Mehlitz]

I'm not sure if I understand the question - jpfESAS has 8 examples using different event scripts (*.es) which are set in the correspondingly named *.jpf application property files. There is only one model used in all these examples, which is CEV_15EOR_LOR.java (the source you have to create). The generic driver (that gets the model class as input) is gov.nasa.jpf.sc.StateMachine, this is the target application from JPF's perspective. I assume you looked at the presentation slides mentioned in the wiki page (http://ti.arc.nasa.gov/m/pub-archive/1402/1402%20(Mehlitz).pdf)

-- Peter

[Corina Pasareanu]

hi adam

you can simply run jpf-core

corina

You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.

To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.

[adam ali]

Hi Peter, with regards to the Statechart project, I had a few more questions. Is the execution of the model checker non-deterministic? I would assume it is, but I don't see how that is possible. From my understanding the execution scripts are included in the .jpf config with certain values to be used when verifying the state charts. Perhaps I am missing something.How exactly do the scripts work and what exactly does the ANY{*} mean? (I looked at the presentation slides and briefly reviewed the paper for some insight also).

[PETER C MEHLITZ]

I assume you mean if it includes choices. Yes, that is what the ANYs do - JPF explores all of the events that are listed in the ANY body. If your trigger methods include additional sources of non-determinism such as concurrency and random values, JPF would also cover these of course.

The ANY{*} is special to jpf-statechart - since it knows the structure of the models it can use reflection to compute all trigger methods (the alphabet - all public instance methods of the active states) and try each of them. The syntax is a bit strange because this uses the same infrastructure as jpf-awt, which doesn't support reflection.

-- Peter

[Adam Ali]

Thanks for the info Peter. I am now trying to recreate the Coverage error that is caught with the -safehold.es and -safehold.jpf scripts. I tried to copy the action code that prohibits the "safehold" state from being reached but when I try I get "no errors". I get the following output from JPF:

StateMachine #0

  state1 : 1

  state2 : 1

  state3 : not covered

Whereas in the project example is the word "REQUIRED" beside the safehold state.

 earthOrbit.insertion : 1

  earthOrbit.orbitOps : 2

  earthOrbit.safeHold : not covered, REQUIRED

Is there something in the script that I have to do to ensure that my "state3" is a required state?

Here is my test code to re-create the Coverage error

public class AdamTest extends State {

class State1 extends State {

public void method1 () {

setNextState(state2);

} 

}State1 state1 = makeInitial(new State1());

 

class State2 extends State {

  public void method2() {

  if (true){

          setNextState(state1);

        } else {

          setNextState(state3);    // <ERR> should never reached

        }

  }

    } State2 state2 = new State2();

    

class State3 extends State {

  public void method3() {

setNextState(state3);

  }

  } State3 state3 = new State3();

}

What should the .es script look like to verify that state3 cannot be reached ever from the initial state?

Thanks!

[Adam Ali]

Thanks Peter, I figured out the issue with help from my Professor. I forgot the sc.required part in the execution script!

[Adam Ali]

Is the JPF-Statechart project capable of handling collections of state diagrams or does is only allow for the analysis of a single state diagram? If it is capable of just handling a single one, would it be difficult to extend the current project to allow for the analysis of multiple interacting state machines? Thank you kindly.

Adam.

[Peter Mehlitz]

it can do hierarchical state charts and orthogonal regions, which I assume should do what you want

-- Peter

[adam ali]

Hello, I have a few questions that I was hoping you could answer. Together with my Professor, we have been taking a close look at JPF - Statechart and Polyglot in hopes that we can analyze UML-RT models (with multiple, asynchronously communicating state machines) with respect to deadlock and basic reachability properties. In order to simulate concurrency we implemented our state machines as orthogonal regions. Our model sends messages from one component to a particular port of a destination component and the message gets queued in the destination components queue. Once the destination component is in a stable state, its queue is then inspected to see if any of its messages can trigger a transition in the destination components' current configuration. With that in mind, we were wondering if JPF-Statechart supports either broadcast or binary communication, as our models only support the latter. Also, do orthogonal regions contain a single shared queue or can they have their own unique queue? Lastly, in regards to the execution scripts that are used to analyze specific sections and properties of the CEV_15EOR_LOR model, is there a way to analyze the entire model as a whole with JPF rather than section by section? Thank you kindly for taking the time to answer our questions. 

Regards,

Adam.

[Peter Mehlitz]

jpf-statechart allows you to send events to all or just specific target states, although I don't recall off the top of my head if that was supported in the scripting. I think it was just supported from within trigger methods via the State interface, together with waiting for specific events. Each state can have its own 'pendingEvents' queue, which is part of the SUT state from JPFs perspective. However, I remember that explicit event send/wait semantics were very UML dialect specific, so you have to consult the code to see if it does what you want (start with the State and StateMachine model classes). If semantics don't match, you can also use normal Java threads - for JPF, the statechart model is just a Java program, i.e. it doesn't restrict you in terms of what you do from your trigger methods (e.g. introducing your own choice points).

I assume with "analyze the entire model" you mean exhaustive search. Yes, jpf-statechart does allow script-less verification, in which case it uses inspection to find the alphabet for each active state (= trigget methods) and tries each event in this alphabet