23 Ноября 2024, 05:32

SPARK

Автор turbo, 09 Июня 2009, 21:15

« предыдущая тема - следующая тема »

0 Пользователей и 1 Гость просматривают эту тему.

turbo

09 Июня 2009, 21:15 Последнее редактирование: 17 Ноября 2011, 16:45 от Zhek@Ch
[size="3"]Вышла GPL-версия инструментария SPARK[/size]

SPARK, инструментарий статической верификации, гарантирующий безопасность и защищённость, отныне лицензирован на условиях GPL. Благодаря этому теперь и Tokeneer, проект, где используются формальные методы для математической верификации биометрической системы безопасности, становится полностью свободным ("open proof").

В GPL-релиз SPARK входят следующие технологии:

 * Описание языка SPARK
 * Полный инструментарий SPARK, включая Examiner, Simplifier и Checker
 * Вспомогательные инструменты: SPARKSimp, SPARKMake, SPARKFormat и POGS
 * Вводные учебные материалы по SPARK и SPARK Pro, с примерами из Tokeneer, включены в сопроводительный релиз пакета Tokeneer Discovery.

SPARK GPL Edition доступен для Windows, SPARC/Solaris, Linux (как для 32- так и 64-битных систем), а также и для OS X (64-бит).

Известный публицист и специалист в области компьютерных систем Дэвид Уиллер (David Wheeler) посвятил этому релизу обширную заметку в своем блоге. В заметке излагаются практические взгляды на надёжность и безопасность критически важного ПО, и SPARK-Tokeneer в частности, в свете его доступности как FLOSS (free-libre / open source software).

http://www.opennet.r...shtml?num=22070

turbo

07 Октября 2009, 17:47 #1 Последнее редактирование: 17 Ноября 2011, 16:49 от Zhek@Ch
[size="3"]Доступна GPL-версия языка программирования SPARK[/size]

Объединенными усилиями компании Praxis и AdaCore выпущена GPL версия SPARK, основанного на Ada языка программирования для разработки приложений, безопасность и надежность которых имеет жизненно важное значение. SPARK предлагает инструментарий статической проверки и формирует доказательства корректности, которые могут быть использованы для создания гарантий в соответствии с требованиями промышленных систем сертификации.

Релиз сочетает в себе язык SPARK, инструменты верификации GNAT Programming Studio (GPS) от Praxis и интерактивную среду разработки GNATbench от AdaCore. Существуют версии SPARK, основанные на языках Ada 83, Ada 95 и Ada 2005, так что все ведущие Ada-компиляторы и инструменты работают прямо из коробки.

http://www.opennet.r...shtml?num=23755