Началась подготовка GPL-версии инструментария SPARK

09.06.2009 06:57

Началась подготовка GPL-версии проекта SPARK, инструментария статической верификации, гарантирующего безопасность и защищённость. Благодаря этому теперь и 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).

исправить +/–

Автор новости: JT

Лицензия: CC BY 3.0

Источник: lwn.net

Короткая ссылка: https://opennet.ru/22070-spark

Ключевые слова: spark, debug

При перепечатке указание ссылки на opennet.ru обязательно

Обсуждение (9)

1.1, ffsdmad (?), 07:30, 09/06/2009 [ответить]	–1 +/–
Звучит как приговор

1.2, relok (?), 08:22, 09/06/2009 [ответить]	+2 +/–
Что это вообще такое? Что за верификатор?

2.3, XoRe (ok), 10:15, 09/06/2009 [^] [^^] [^^^] [ответить]

+/–

>Что это вообще такое? Что за верификатор?

Верификатор - проверятель истинности (правильности).

http://ru.wikipedia.org/wiki/%D0%92%D0%B5%D1%80

3.4, Aleksey (??), 11:22, 09/06/2009 [^] [^^] [^^^] [ответить]	+/–
То бишь для людей от которых требуют 100% гарантию правильности работы программы

4.5, zhus (ok), 12:27, 09/06/2009 [^] [^^] [^^^] [ответить]	+1 +/–
Ага, не забыть только критерии правильностьи верифицировать для начала. На 100%. А перед этим верифицировать критерии оценки критериев :))

4.6, Ivan (??), 13:08, 09/06/2009 [^] [^^] [^^^] [ответить]	+/–
Помню была то ли теорема толи что о том, что программ без ошибок не может существовать. Вот и IMHO гарантировать 100% правильность значит заведомо врать.

5.7, aborland (?), 14:21, 09/06/2009 [^] [^^] [^^^] [ответить]	+/–
Не 100% Правильности а 100% соответствия формальным критериям

5.8, Aleksey (??), 14:23, 09/06/2009 [^] [^^] [^^^] [ответить]	+/–
Такой теоремы не может быть в принципе.

5.9, darkk (?), 05:59, 10/06/2009 [^] [^^] [^^^] [ответить]	+/–
Вы путаете теорему и гипотезу. «Гипотеза», как бы научно и серьезно это слово не звучало, не является доказанной и, соответственно, верной.

Добавить комментарий

Текст: