Openbravo Forum End of Life Notice

Dear Openbravo Forum User,

Because of continued very low usage we decided to stop the forums on 31st of August 2017

In case of questions: webmaster "at" openbravo.com

Formal Verification of Open Bravo

<<

Pedro de Carvalho Gomes

Posts: 3

Joined: Tue May 17, 2011 9:50 am

Post Tue May 17, 2011 10:17 am

Formal Verification of Open Bravo

Hi all,


 


I am a PhD student at KTH Royal Institute of Technology in Stockholm. I research Formal Methods. My current research focus the compositional verification of software. The team I research in has developed a compositional method for formal verification of control-flow safety properties, and implemented it as CVPP, which is  tool set for verifying Java software. In other words, we verify Java software against properties like "alway when a method starts to write in a file, it has to finish before allowing other writing" or "Whenever  method newSession() starts, it has to finish before being invoked again".


The compositional method and the tool set have been developed for more than 7 years, it is mature and generated a lot of scientific publications. You can get more information about it using ProMoVer, a web tool that wraps the tools in the CVPP tool set:


http://www.nada.kth.se/~siavashs/ProMoVer/


 


Right now we want to validate our method with a significative testcase. We have been analysing Open Bravo for a while, and it seems a very good match. For many reasons:


- It's size is complex enough to what we are looking for (more than 200.000 LoC, more than 10.000 methods,...)


- It's a good example of application which can have meaninfull properties to be checked.


- Open Bravo is an open comunity and incourages the cooperation with academia.


 


So, the goal of this post is to start talks with developers, in special from the Q&A team,  about a possible cooperation to formally verify Open Bravo. We believe this would bring the reliability level of OpenBravo to another level. At first we propose that we from KTH would do the verification process. The Open Bravo comunity could help us by providing properties of sequence of undesired method invocations, that should be absent from the code. I can explain in more details the technical part.


 


I would be a thrilling project to take our research beyond, at the same time supporting a vivid and successfull open-source project. What do you think?


 


Best regards


 


Pedro

<<

Pedro de Carvalho Gomes

Posts: 3

Joined: Tue May 17, 2011 9:50 am

Post Wed May 25, 2011 7:16 pm

RE:Formal Verification of Open Bravo

Hi all,



My message has been in the forum for some time, but I didn't get any reply. Does anyone know how to get in contact with members of the Q&A team?



Thanks
<<

Ismael Ciordia Vela

Posts: 398

Joined: Wed Mar 18, 2009 7:25 pm

Post Thu May 26, 2011 9:32 pm

RE:Formal Verification of Open Bravo

 Hi Pedro,


sorry for late reaction, we are in the last steps to complete the first stable version of a new major release, Openbravo 3, and we are fully overloaded in this process. We currently target mid June for this release.


Your proposal sounds interesting but still not clear to me what you expect from us. Could you please elaborate on the technical part -the process and what we should do to support you- so we can better understand the effort it will require from our side?


If we can afford the effort  we will be happy to help you in this process. And please be patient, till mid June we are 100% focused on the release.


Best,


Ismael

<<

Pedro de Carvalho Gomes

Posts: 3

Joined: Tue May 17, 2011 9:50 am

Post Fri May 27, 2011 1:05 pm

RE:Formal Verification of Open Bravo

Hi Ismael,
 
My working group (from KTH, University of Twente and ETH) research compositional verification of temporal control-flow safety properties. Translating: we inspect software to check if bad things may or may not happen. The method is formal, which means that if the inspection concludes that some bad thing can not happen, you are 100% sure that about it. But if a bad thing can happen, we tell how it happens, then developers can fix it. It is different from testing, which tries to find as many bugs as possible, but can never guarantee that there are no other bugs. Formal verification has some limitations, and it does not compete with testing. We see both approaches as complementary.
 
The main limitation of software formal verification is scalability. The bigger the software, bigger are the possible executions we have to take into account to prove some property. To circumvent this, we research a compositional approach. Our verification method is compositional, which means that we break the inspection task into pieces that are small enough to be checked. Then compose the result of the parts to conclude the correctness of the system as a whole. One of the reasons we have interest in verifying OpenBravo is its size: it's big enough to represent a challenge to our method.

We have implemented our verification method as a collection of software that we call CVPP. We also created a tool called ProMoVer to automate the verification steps. Up to now CVPP/ProMoVer checks Java Bytecode only. So a second reason to chose OpenBravo is its implementation in Java. Others reasons are that it is Open Source, and moreover, OpenBravo incentives cooperation with academic institutions.
 
The kind of properties that CVPP can check is temporal control-flow safety properties. In other words, we verify if sequences of method invocations can or cannot happen. One example of such properties would be "Can method WriteInTheDataBase() be called before the method OpenDataBaseConnection() was called?". Another example: "Once I enter method StartNewSession(), does exist a sequence of method invocations that can call another instance of StartNewSession() before the first one has finished?". We have other examples of properties that may be interest to check in Open Bravo. That's when enters the collaboration of OpenBravo developers.
 
We propose that we, from CVPP team, do the entire verification task, and we would like OpenBravo team to collaborate  by providing meaningful properties. The OpenBravo team knows well the code, so we would like you to help us to define properties of sequence of method invocations. The definition of such properties should be a joint work. So we propose to explain more in details how to do that, how to formalize properties into temporal formulas, an so on.
 
I hope that you guys appreciate such collaboration. I believe that it would bring the reliability of OpenBravo into a new level, at the same time that validates our method to big software systems. What do you think?
 
Regards,
 
Pedro

Return to Early Releases Discussion

Who is online

Users browsing this forum: No registered users and 2 guests

Website Terms


Designed by ST Software for PTF.