10-Dec-2019: The start of a project on formal modeling and verification of software

The project "Research and development of technologies for production and certification of safety and security critical software based on formal methods and verification" has been started by ISPRAS in cooperation with RPA RusBITech JSC and FGUP GosNIIAS. The project is supported by the Ministry of science and higher education of the Russian Federation (project unique identifier: RFMEFI60719X0295).

The project is aiming at creation of new technologies for development and certification of software, ensuring high reliability and information security of mission critical software systems, including operating systems, embedded control systems, data processing systems and robotics used in critical domains like space, aviation, atomic energy and medicine.

The project and first results were presented at the ISPRAS technologies exhibition as part of the Ivannikov ISPRAS Open Conference. There was demonstrated the AstraVer toolset intended for deductive verification of mission critical software components. AstraVer supports development and verification of security policy models and proving correctness of modules in C language. The main attention was given to new methods and tools designed to facilitate the development and use of multi-level models in verification and testing of software.

Please follow news of the project on the dedicated site astraver.linuxtesting.org.