Spinroot

A forum for Spin users

You are not logged in.

#1 2017-08-09 14:10:01

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Best practices to structure large promela code

Hi,

are there best practices to structure your promela code when you have a lot of it?

--------------------------------

Have we made good architectural choices with the following approach?

1) We model each software part/feature (there are about 20) in a separate promela file (of 10 to 200 LOC), using either proctype or inline. This helps us to modularize, but gives warnings regarding missing init (or other active) proctype, and requires us to #include files.

2) Because we #include different promela files, we use include guards.

3) We have one main promela files which (directly or indirectly) includes all other promela files. It has many initialization proctypes for various aspects; at all times, only one of these proctypes is marked active.

4) Some "software xxx line" variants we model via #defines, others are more suitable to directly integrate into the model (i.e. via variables and promela structures instead of precompiler directives).

5) We use defines and unsigned variables to model the various enumerations we have, to avoid having one huge (untyped) mtype, at the cost of more cryptic debugging.

Offline

#2 2017-08-10 22:26:38

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Best practices to structure large promela code

It is always best to keep models small, and focused on a specific verification query/property.
There are no real structuring benefits as there would be for a typical programming language.
In fact, the opposite may be true in verification.  Having more proctypes may increase the level of concurrency, and thus increase the verification complexity. Having fewer can reduce complexity.
Reducing the amount of data always helps to reduce verification complexity.
No easy answers here I'm afraid. Formal verification is always a battle against computational complexity.... (and not just in applications of logic model checking).

Offline

#3 2017-08-21 16:56:26

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: Best practices to structure large promela code

Thanks, that is some good advice. We are, however, modeling close to the software, so the models need to contain the relevant details and are thus not really small.

Since the code contains a lot of enums, I would like to come back to my point 5) above: How should I translate all the enums into Promela? Is there a workaround so that I can simulate having multiple mtypes in Promela?

Currently, I am using #defines and unsigned variables to model enumerations, to avoid having one huge mtype, which causes large state vectors and weak type safety. However, #defines is even weaker typed and harder to debug (seeing numbers instead of identifiers in simulation).

Offline

#4 2017-08-21 17:56:17

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Best practices to structure large promela code

You can have multiple mtype definitions -- but the max nr of mtype values is 255...
#defines are a good way around that limit, but yes, it makes interpreting trails harder
I don't think mtype's contribute to state vector size, since they're basically equivalent to a byte variable.

Offline

#5 2017-08-21 19:36:40

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: Best practices to structure large promela code

Sorry, I meant multiple mtype types, not multiple mtype definitions.

For example, if you had mtype_1 statesOfProc1, mtype_2 statesOfProc2, ...., you could have up to 255 states for each mtype_i, and get a compiler error when assigning an mtype_1 element to statesOfProc2.

Is there some way to achieve this?

Offline

#6 2017-08-21 20:59:10

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Best practices to structure large promela code

Yes, that's a good idea.
Maybe for the next release, but it would take some work to add.

Offline

#7 2017-08-22 08:40:40

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: Best practices to structure large promela code

Great that you are open for this suggestion.

Can I somehow help or motivate to achieve this?

Bosch and I would be very glad to have it.

Offline

#8 2017-08-22 21:27:08

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Best practices to structure large promela code

Okay -- it's on my list for Version 6.4.8

Offline

#9 2017-08-23 12:51:40

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: Best practices to structure large promela code

Thank you very much smile

Offline

#10 2017-08-30 16:17:51

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Best practices to structure large promela code

A test version with the extension is available to anyone who'd like to try it...

Offline

Board footer

Powered by FluxBB