Reinventing the wheel.

[whitingjr]

Hi,

I am interested to know the reason for starting this project. Considering there is the existing formal verification tools already used in academia and industry such as SPIN

http://spinroot.com

and the languague Promela

https://en.wikipedia.org/wiki/Promela

What features do Promela and SPIN lack to justify this project ? Apart from it being an implementation in Java.

Regards,

Jeremy

[objectiser]

Hi Jeremy

I've asked one of the academic partners on the project to respond, as they have a better understanding of the area, and can definitely give you a more complete answer.

However from my limited understanding of SPIN/Promela, it describes the concurrent processes, and uses SPIN to test the state space of possible interactions that could occur. It also does not appear to have a 'parallel' construct (although possibly I've missed something).

The work underpinning scribble is focused on verifiation of a global model (i.e. choreography), which represents essentially a "birds eye" view of the interactions across all communicating parties, using the Pi Calculus and Session Type theory. My understanding is that the verification is therefore more efficient. Some properties, such as deadlock freedom can be achieved by design, assuming other conditions are met.

However, my role in this project is to build the Java tooling, so it is best that one of the domain experts provides the definitive answer.

btw We are also doing an EPSRC Knowledge Transfer project with Newcastle University on the Savara project using SPIN/Promela entitled "Bridging the Gap Between Choreography and Business Goals".

Regards

Gary

[whitingjr]

Hi Gary,

Thank you for responding. Knowing now there is a partnership with Newcastle University my question has been answered. Having studied an MSc there in the past.

Is this project going to be a drop in replacement for SPIN or will there be a "bridge" to reuse it ?

Regards,

Jeremy

[objectiser]

Hi

Both areas of work are still at an early stage, so we don't know exactly how they will be leveraged in savara yet. Its possible they may both provide different benefits, and therefore may co-exist, or be used as alternatives.

Once we have a more concrete idea, then we'll consider how best to plug them in.

Regards

Gary

[nobuko.yoshida]

>The work underpinning scribble is focused on verifiation of a global model (i.e. choreography), which represents essentially a "birds eye" view of the interactions across all >communicating parties, using the Pi Calculus and Session Type theory. My understanding is that the verification is therefore more efficient. Some properties, such as >deadlock freedom can be achieved by design, assuming other conditions are met.

Gary is right. More precisely, since Scribble is based on type-theory, (1) it is more efficient (basically the deadlock-freedom is checked in polynomial type complexity) and (2) it is more tightly coupled with the programming languages. We can also enritch Scribble with logical annotations, which are on-going.

Our imperial group is also awarded by EPSRC KTS and a member of my group is working at Cognizant for developing Scribble.

Best regards,

Nobuko Yoshida