Re: Call for help on CSPM

[Larry Dickson <tjoccam@xxxxxxxxxxx>]

Hi Kevin and all,

I appreciate the observations, but they cover only part of the needs. (I sent Kevin the full problem.) What you describe seems to fit what I call "structure" variables - these would be variables whose value is significant for program flow, such as the start and end pointers for a circular buffer. They change in a small set and are tested, causing branching depending on the results of the tests.

The other thing I call "content" and refers to variables, which may be huge (like 4096 bits = a 512-byte sector) but act atomically, passing from place to place in storage (what is "place" in "storage"? Easy to define in regular computing but alien to functional programming?) I don't even want to have to deal with the content of a content variable, just to use concepts like "same" to trace its movement. And yet the specific content of a content variable may be the whole purpose for which the program exists.

Another problem arises when structure variables take a rather large range. For instance, values = {0, 1, . . . 255}. In many cases, a mathematical proof is possible in such a case that uses something like 3 cases, not 256 cases. Can that be managed in CSPM-based formal verification?

Larry

On Feb 15, 2019, at 4:15 PM, Chalmers, Kevin <K.Chalmers@xxxxxxxxxxxx> wrote:

> Hi Larry,
> 
> If it is just variables holding you back this is pretty simple.  You can look at Jeremy and Peter's CSP for JCSP for example, and Matt and I used this as a basis for some things we are working on.
> 
> Basic idea, you need to declare your variables and channels to allow a process to manage them.  For example:
> 
> VARIABLES = { x, y} -- variable names
> VALUES = { 0, 1, 2} -- possible values of x and y: need to keep a small set.
> datatype Operations = get | set -- get and set operators
> channel var_chans = VARIABLES.Operations.VALUES
> 
> X_VAR(val) = (x.get!val -> X_VAR(val)) [] (x.set?val -> X_VAR(val))
> Y_VAR(val) = (y.get!val -> Y_VAR(val)) [] (y.set?val -> Y_VAR(val))
> VARS = X_VAR(0) ||| Y_VAR(0)
> 
> Or you can abstract further by passing the channel in to the process:
> 
> VAR(chan, val) = (chan.get!val -> VAR(chan, val)) [] (chan.set?val -> VAR(chan, val))
> VARS = VAR(var_chans.x, 0) ||| VAR(var_chans.y, 0)
> 
> In either case, you can get and set the variable via:
> x.get?n
> x.set!2
> 
> Really just depends what you are trying to do.
> 
> Kevin
> 
> -----Original Message-----
> From: occam-com-request@xxxxxxxxxx <occam-com-request@xxxxxxxxxx> On Behalf Of Larry Dickson
> Sent: 15 February 2019 18:45
> To: Matt Jadud <matt@xxxxxxxxx>; Carl Ritson <C.G.Ritson@xxxxxxxxxx>; P.H.Welch <P.H.Welch@xxxxxxxxxx>; Fred Barnes <F.R.M.Barnes@xxxxxxxxxx>; Martin, Jeremy <Jeremy.Martin@xxxxxxxxxx>; Bill Roscoe <awroscoe@xxxxxxxxx>
> Cc: lindsay spacesciencescorp.com <lindsay@xxxxxxxxxxxxxxxxxxxxx>; rob spacesciencescorp.com <rob@xxxxxxxxxxxxxxxxxxxxx>; Occam Family <occam-com@xxxxxxxxxx>
> Subject: Call for help on CSPM
> 
> Hello all,
> 
> I need help in translating two simple FIFO implementations into CSPM and then feeding them into programs (like FDR and Deadlock Checker) that take CSPM. We can pay a reasonable stipend.
> 
> One is the standard bunch-of-buffers-in-parallel and the other is the indexed circular buffer (shelf/store implementation to avoid output ALT). Each varies packet size (one bit or 4096 bits) and depth (5 or 256).
> 
> We need to demonstrate practical usability in data-flow problems - no state explosion - or else find a path to it. It has to be possible (Bill Roscoe and C.A.R.  Hoare, "The Laws of occam Programming," 1986; and I did it using "Ground Truth" at CPA2017), but I am wondering if anyone is still working on CSPM? There has to be some way to translate functional language into real computing; or else, I heard a rumor you could do variables as processes?
> 
> If anyone is interested I can provide the SHORT documentation.
> 
> Larry Dickson
> 
> 
> 
> 
> This message and its attachment(s) are intended for the addressee(s) only and should not be read, copied, disclosed, forwarded or relied upon by any person other than the intended addressee(s) without the permission of the sender. If you are not the intended addressee you must not take any action based on this message and its attachment(s) nor must you copy or show them to anyone. Please respond to the sender and ensure that this message and its attachment(s) are deleted.
> 
> It is your responsibility to ensure that this message and its attachment(s) are scanned for viruses or other defects. Edinburgh Napier University does not accept liability for any loss or damage which may result from this message or its attachment(s), or for errors or omissions arising after it was sent. Email is not a secure medium. Emails entering Edinburgh Napier University's system are subject to routine monitoring and filtering by Edinburgh Napier University.
> 
> Edinburgh Napier University is a registered Scottish charity. Registration number SC018373
>