An important step in meeting the Verifying Compiler Grand Challenge is the Verified Software Repository, a scientific repository that will assist in the development of software by facilitating access to a managed collection of analysis tools and a repository of case studies or challenge codes to exercise these tools. In the FMICS view, the repository should include proven correct software and tools to help establishing the correctness of the software in question. This site presents the contribution of the ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS) to the VSR.
One of the goals of FMICS is to transfer and promote the use formal methods technology in industry. We believe that the VSR offers a great opportunity to reach this goal, resulting in a more robust and solid software industry in Europe.
Based on jETI, the core FMICS partners are going to set up a collaborative demonstrator that
- illustrates the applicability of the jETI technology for lightweight remote integration of tools into the repository
- shows how to provide tools to the repository, by registration and remote provision,
- demonstrates how to experiment with local and remote tools to solve cooperative verification tasks
- shows how to orchestrate different tools (possibly a mix of local and remote ones) which were not originally designed to cooperate, to address more complex case studies.
This may require the availability of mediators, to cover semantic gaps between the tools.
JETI's purpose was unique in allowing users to combine functionalities of tools of different application domains to solve problems a single tool never would be able to tackle. Obviously, the richness of the tool repository plays a crucial role in the success of jETI: the benefit gained from our experimentation and coordination facilities grows with the amount and variety of integrated software-tools. The success of the jETI concept is thus highly sensitive to the process and costs of tool integration and tool maintenance.