I'm Petra. Manage Complexity with Simplified Formal Methods.
As a stakeholder have you every wanted to prove your critical business systems correctly transition between states? Petra makes this possible, through its all-in-one integrated formal modelling and software development language standard:
public final class Light {
private final Power power = new Power();
private final Control control = new Control(); @Initial
public boolean off() { return power.off() || control.off(); }
public boolean on() { return power.on() && control.off(); } // validation error: inconsistant with domain model. public void toggle() {
if (off()){
sep(()->{power.turnOn();},
()->{control.turnOn();});
assert(on()); // verification error: unreachable state.
} else if (on()){
sep(()->{power.turnOff();},
()->{control.turnOff();});
assert(off());
}
}
}
How it works?
1. Model / DevelopUse Petra's language standard to formally model complex systems. The models are just executable programs, hence they can also replace/upgrade current software components.
2. VerifyAt the touch of a button, automatically verify state transitions with fast results, even for large object-oriented systems, thanks to Petra's abstraction oriented design.
3. Explainable FeedbackUnlike traditional formal methods, our error messages are explainable, relating directly to the states encoded within the applications language domain.
Benefits?
Object-oriented (Java).Fully integrates with existing code, workflows and IDEs such as IntelliJ.
Developer friendly.Petra is the easiest and most comprehensive formal method to learn for everyday developers. Just learn the rules, write code and press verify.
Flexible to adopt.Use as much or as little of Petra as you like. Use it to manage complexity by modelling and/or developing complex systems from the ground up, or use it to rewrite specific components.