Introducing Prover Studio

I am proud to present Prover Studio, an integrated development environment for formal specifications. I must admit, we should have done this years ago. It’s astonishing really that we did not. Here is the story.

We established the concept of Prover Trident quite some time ago. The idea is simple: divide signaling software production in three phases.

1. Formal specification. Capture your signaling design principles in formal logic.
2. Formal development. Use your formal specification and your configuration data to build a model of a signaling system. Investigate it using simulation and verification and finally generate revenue-service ready code from the model.
3. Formal sign-off verification. Use an independent program to formally verify that all safety requirements are fulfilled and generate the safety evidence.

To aid the second phase we developed Prover iLock, and for the third phase we developed Prover Certifier. But we never offered any product for the first phase, until now, although we always stressed that the first phase is where you spend most of the time. Ironic, indeed. There is a simple explanation why it took so long for us to understand the importance of providing a good development environment. Formal specifications are written in plain text files, and there are lots of text editors out there already. Creating formal specifications requires a lot of thinking, but producing the file itself is easy, when you have decided what to write.

However, when we investigated more thoroughly how users spend their time, it was clear that the process of writing formal specifications could be simplified a lot. When a specification grows large, it becomes increasingly difficult to remember what is already in there. Therefore, it becomes increasingly important with good support for navigation, to find which functions have been implemented already for a particular object and how they are defined, to understand where a certain function is used, to find dead code, et cetera. Specification can consist of hundreds of files for complex applications, so all kinds of help in finding things and getting an overview of what you have is appreciated. We created Prover Studio to provide all this, as well as on-the-fly syntax checks of more advanced immediate semantic checks that help discovering errors early.

During formal specification writing, Prover iLock is repeatedly used to check the specification and to try it on concrete examples. It is quite common to find an error in the specification by using Prover iLock’s simulator or code viewer, for example. In such cases, it is convenient to be able to quickly open the relevant file and find the line that needs to be changed. To make it possible to open the relevant piece of specification from Prover iLock we need to provide our own editor and integrate the tools.

The first version of Prover Studio was realized as an extension to Visual Studio Code. Our users told us that Prover Studio makes a great difference already. We intend to keep Visual Studio Code as the framework for Prover Studio’s editing and navigation capabilities, but also expand Prover Studio beyond what Visual Studio Code can offer, with features such as graphical representation of logic.