jellebouma / bgj Goto Github PK
View Code? Open in Web Editor NEWGeneration of Java APIs and processes from Scribble protocols, that can be statically verified by Vercors.
License: Other
Generation of Java APIs and processes from Scribble protocols, that can be statically verified by Vercors.
License: Other
Currently Scribble-Java creates a class for each state, named as such: protocol_role_number (for example: Adder_C_1).
These classes contain the methods enabled at these states, this statically guarantees that for a state only the enabled methods are used.
However it is up to the user to use the correct state.
We propose to use only the methods so the generated code more closely resembles the actual Scribble protocol.
VerCors will verify that only enabled methods are used.
We have already shown that VerCors can verify state for the current implementation where methods are part of the state class.
In cases where the same method is used in multiple states we should be able to verify this as follows:
Imagine the Adder example except there need to always be an even number of additions, so we need to do Add and Res twice before we can stop:
global protocol Adder(role C, role S) {
choice at C {
Add(Int, Int) from C to S;
Res(Int) from S to C;
Add(Int, Int) from C to S;
Res(Int) from S to C;
do Adder(C, S);
} or {
Bye() from C to S;
}
}
Now we have a method Add
that can be executed from multiple states, we can verify that it is executed correctly as follows:
//@ context Perm(state, 1);
//@ requires state == 1 || state == 3;
//@ ensures (\old(state) == 1 && state == 2) || (\old(state) == 3 && state == 4);
public void add(int p1, int p2) {
if (state == 1)
state = 2;
else if (state == 3)
state = 4;
}
External choice is not modeled by the automaton and as such is treated like an internal choice.
A choice must be received from the other party and operations may only be executed if they have been chosen.
A choice may only be received if it is made according to the protocol.
To represent the different choices:
Enums are not allowed by VerCors and static constants cannot be used either as assigning a value in a declaration gives an error in Vercors as well.
To solve this, constant attributes can be given a value in the constructor. While a variable holds the current choice.
External choice can be handled as such by generated code:
package adderpkg;
public class Adder
{
int state;
int choice;
public final int EXTERNAL_CHOICE_ADD;
public final int EXTERNAL_CHOICE_BYE;
//@ ensures Perm(state, 1) ** Perm(choice, 1) ** Perm(EXTERNAL_CHOICE_ADD, 1) ** Perm(EXTERNAL_CHOICE_BYE, 1);
//@ ensures state == 14 && choice == -1 && EXTERNAL_CHOICE_ADD == 0 && EXTERNAL_CHOICE_BYE == 1;
public Adder() {
choice = -1;
state = 14;
EXTERNAL_CHOICE_ADD = 0;
EXTERNAL_CHOICE_BYE = 1;
}
//@ context Perm(state, 1) ** Perm(choice, 1);
//@ context state == 14;
//@ requires choice == -1;
//@ ensures (\result == 0 || \result == 1) && \result == choice;
public int receiveExternalChoice() {
choice = 0;
return 0;
}
//@ context Perm(state, 1) ** Perm(choice, 1);
//@ requires state == 14 && choice == 0;
//@ ensures state == 16 && choice == -1 && \result != null;
public AddPayload add()
{
choice = -1;
state = 16;
return new AddPayload(0, 0);
}
//@ context Perm(state, 1) ** Perm(choice, 1);
//@ requires state == 14 && choice == 1;
//@ ensures state == 15 && choice == -1;
public void bye()
{
choice = -1;
state = 15;
}
//@ context Perm(state, 1);
//@ requires state == 16;
//@ ensures state == 14;
public void res(int arg0)
{
state = 14;
}
public static void test() {
Adder adder = new Adder();
if (adder.receiveExternalChoice() == adder.EXTERNAL_CHOICE_ADD) {
adder.add();
adder.res(0);
}
else
adder.bye();
}
}
Connection between roles has not yet been implemented.
A Scribble protocol can be either implicit or explicit.
In both cases, user input will be needed to provide locations (IP/port) of the other roles.
In the case of an explicit protocol, roles have to connect and disconnect to each other in the protocol.
These connections are bi-directional and must be distinct.
I need to investigate how Scribble-Java handles them.
In the case of an implicit protocol: the protocol starts with all roles pairwise connected.
However in Scribble-Java making the connections is left to the user (and is susceptible to deadlocks).
In their Adder example C connects to S in the user code, if S is not started before C the connection fails.
Info on Scribble connections taken from: http://www.scribble.org/docs/scribble-java.html#SCRIBCONNECT
A consideration was made, whether communication of null values instead of objects should be allowed.
While sending null values could be considered a violation of protocol, it is an important aspect of the Java language that any object may be null.
It was decided to follow Scribble-Java's lead, after some testing it was revealed that Scribble-Java does allow null values to be communicated instead of objects.
Currently, even when the unsupported language features are removed. Unexpected errors still occur.
Simplifying Adder.java and Adder_C_1.java of the Scribble Adder example until it succesfully verifies leads to the following code:
Adder,java:
package tutorial.adder.Adder.Adder;
public final class Adder {
public static int state;
}
Adder_C_1.java:
package tutorial.adder.Adder.Adder.statechans.C;
import tutorial.adder.Adder.Adder.Adder;
public class Adder_C_1 {
//@ context Perm(Adder.state, 1);
//@ ensures Adder.state == 1;
public Adder_C_1() {
Adder.state = 1;
}
//@ context Perm(Adder.state, 1);
//@ requires Adder.state == 1;
//@ ensures Adder.state == 2;
public void send(int arg0, int arg1) {
Adder.state = 2;
}
//@ context Perm(Adder.state, 1);
//@ requires Adder.state == 1;
//@ ensures Adder.state == -1;
public void send() {
Adder.state = -1;
}
}
If attribute state
has a default variable as such: public static int state = 0;
VerCors gives the following error:
If send has Integer
parameters as opposed to int
then VerCors gives an error as well.
Currently state objects being returned are not verified not to return null.
They cannot return null, however we should verify this, so that method calls on these objects can be verified as well.
See utwente-fmt/vercors#739 for a more detailed explanation of this issue.
Generated Scribble code of the Adder example generates code that throws custom exceptions of type ScribRuntimeException
.
I do not know what this exception is meant to represent as it just extends Exception
and the only documentation states that it is actually not a Scribble run-time exception: "Note: not a run-time ScribbleException
".
Problem:
The verification skeleton cannot have these exceptions however, as exceptions must extend Throwable
and VerCors does not support inheritance.
Default Java exceptions (IOException
) are fine however, implying that VerCors treats default Java classes differently.
Removing these exceptions only from the verification skeleton is not an option as user code will still need to handle them.
This means that it is impossible to verify generated code + user code without changing the generated code, even if using the verification skeleton.
TypeArgumentsOrDiamond
such as new LinkedList<>()
or new LinkedList<String>()
JavaIdentifier
such as org.scribble.core.type.name.GProtoName
as opposed to GProtoName
Annotation
such as @Override
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.