By using this site, you agree to our updated Privacy Policy and our Terms of Use. Manage your Cookies Settings.
455,767 Members | 1,332 Online
Bytes IT Community
+ Ask a Question
Need help? Post your question and get tips & solutions from a community of 455,767 IT Pros & Developers. It's quick & easy.

Verifying temporal properties. Need problems.

P: n/a
Hello all

As part of a thesis, I am model checking Python programs (a limited
subset anyway).

I have a very rough prototype that can deal with temporal properties
(LTL), that is statically prove properties of the kind: "if A happens,
then B should follow" or "if A happens, then B must not follow unless
C happens first". A,B,C here being function calls (system or other
library). The idea is that this might complement testing or manual
auditing during development.

So the solution now requires a problem.
Basically I'm trying to find interesting areas where a programmer is
supposed to call specific functions in a particular order, but where
coding errors might prevent this.
I would be most happy with distinctively Python-related problems, like
some tricky-to-use system calls or something from Zope or
security-related issues, etc.

So if any of you have ideas (specific function calls) where this kind
of tool would be useful, I would welcome feedback.
If replying privately, use bjornhb2_hotmail.com (more or less).

Thanks a lot :)
Bjorn
Jul 18 '05 #1
Share this Question
Share on Google+
5 Replies


P: n/a
Bjorn Heimir Bjornsson wrote:
Hello all

As part of a thesis, I am model checking Python programs (a limited
subset anyway).

I have a very rough prototype that can deal with temporal properties
(LTL), that is statically prove properties of the kind: "if A happens,
then B should follow" or "if A happens, then B must not follow unless
C happens first". A,B,C here being function calls (system or other
library). The idea is that this might complement testing or manual
auditing during development.

So the solution now requires a problem.
Basically I'm trying to find interesting areas where a programmer is
supposed to call specific functions in a particular order, but where
coding errors might prevent this.
I would be most happy with distinctively Python-related problems, like
some tricky-to-use system calls or something from Zope or
security-related issues, etc.

So if any of you have ideas (specific function calls) where this kind
of tool would be useful, I would welcome feedback.
If replying privately, use bjornhb2_hotmail.com (more or less).

Thanks a lot :)
Bjorn


Hi,

I do not have any python program to check but I'm interested in
publications you might already have writen or pointers to python related
problem.
I'm working as engineer in a research team in formal methods area
(http://www.loria.fr/equipes/model/).

Did you look at similar project with Java (like
http://bandera.projects.cis.ksu.edu/) ? I think you will find similar
problem, no ?

Did your prototype recognize use of the thread standard library (lock,
etc) ?

If you look at mailman (http://www.list.org/), you can check security
property like "a non-members cannot send messages to the list", etc.

Do you look at rather small or big project ?

Sorry if I ask more question than I answer... ;-)
The last one : When will you finish your Phd ?

Loc

Jul 18 '05 #2

P: n/a
Hello Loic
I'm working with control flow only, generating pushdown systems from the
AST that are then checked with the model checker Moped (using LTL
properties).
A similar approach was taken for JavaCard
(http://www.sics.se/fdt/vericode/jcave.html).
I chose Python for fun, but at the moment support just a limited subset.
I'm unsure how far I will/can go. E.g. some dynamic stuff can't be analysed
statically. I also just ignore all data flow, which simplifies everything but
means I will not recognise all control flow correctly.
I checked some small non-python-specific problems, but experience of others
suggest that the aproach scales quite well.
This is an MSc thesis, I haven't published anything else.
Bjorn
Jul 18 '05 #3

P: n/a
Bjorn Heimir Bjornsson a crit :
Hello Loic
I'm working with control flow only, generating pushdown systems from the
AST that are then checked with the model checker Moped (using LTL
properties).
A similar approach was taken for JavaCard
(http://www.sics.se/fdt/vericode/jcave.html).
I chose Python for fun, but at the moment support just a limited subset.
I'm unsure how far I will/can go. E.g. some dynamic stuff can't be analysed
statically. I also just ignore all data flow, which simplifies everything but
means I will not recognise all control flow correctly.
I checked some small non-python-specific problems, but experience of others
suggest that the aproach scales quite well.
This is an MSc thesis, I haven't published anything else.
Bjorn


Hi,
Ok I see.
Instead of searching the workflow yourself you might look at PyPY. There
is a class (see translator.py) that construct such a flow. I have also
construct a simple data flow to check if a variable used was previously
defined.

On monday, I will show you a kind of workflow I'm creating in case mine
is more complete than yours...

Anyway, you're right that with dinamic stuff, analysis is difficult. But
with research like StarKiller (Type Inference) it should become more and
more easier...

I will wait for your publication ;-)

Loc

Jul 18 '05 #4

P: n/a
Yermat <lo**@yermat.net1.nerim.net> wrote in
Instead of searching the workflow yourself you might look at PyPY.
There is a class (see translator.py) that construct such a flow.
Thanks Loic for pointing out pypy's controlflow. I will check if I can use
it. I had searched for something like this for Python but never found
anything.
On monday, I will show you a kind of workflow I'm creating in case
mine is more complete than yours...


It would be really interesting to see what can be done with pypy's
controlflow.

Bjorn
Jul 18 '05 #5

P: n/a
Bjorn Heimir Bjornsson wrote:
Yermat <lo**@yermat.net1.nerim.net> wrote in
Instead of searching the workflow yourself you might look at PyPY.
There is a class (see translator.py) that construct such a flow.

Thanks Loic for pointing out pypy's controlflow. I will check if I can use
it. I had searched for something like this for Python but never found
anything.

On monday, I will show you a kind of workflow I'm creating in case
mine is more complete than yours...

It would be really interesting to see what can be done with pypy's
controlflow.

Bjorn


Hi,
At http://www.fejoz.net/Loic/Divers, you will find a little example of
the output of PyPy and output of my own program.
There is also my own program which only use Python AST where as PyPY is
more concrete.

Good luck !
Loc

Jul 18 '05 #6

This discussion thread is closed

Replies have been disabled for this discussion.