About: SPIN model checker     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : yago:Whole100003553, within Data Space : dbpedia.org associated with source document(s)
QRcode icon
http://dbpedia.org/describe/?url=http%3A%2F%2Fdbpedia.org%2Fresource%2FSPIN_model_checker

SPIN is a general tool for verifying the correctness of concurrent software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field.

AttributesValues
rdf:type
rdfs:label
  • SPIN (de)
  • SPIN model checker (fr)
  • SPINモデルチェッカ (ja)
  • SPIN model checker (en)
  • SPIN (верификатор) (ru)
rdfs:comment
  • SPIN (ursprünglich ein Akronym für Simple PROMELA Interpreter) ist eines der bekanntesten Werkzeuge zur Modellprüfung (englisch Model Checking). SPIN prüft endliche Zustandsautomaten (engl. Finite State Machines) mit der temporalen Logik LTL. Zusätzlich bietet SPIN viele Optimierungsmethoden, zum Beispiel , Komprimierungen und Bitstate Hashing. (de)
  • SPIN est un outil général pour vérifier la correction de modèles logiciels concurrents de manière rigoureuse et généralement automatisée. Il a été écrit, à partir de 1980, par Gerard J. Holzmann et d'autres membres du groupe Unix du Computing Sciences Research Center des Bell Labs. Le logiciel est disponible gratuitement depuis 1991 et continue d'évoluer pour suivre le rythme des nouveaux développements dans ce domaine. (fr)
  • SPIN is a general tool for verifying the correctness of concurrent software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field. (en)
  • SPINモデルチェッカ（英: SPIN model checker）は、ソフトウェアのモデル検査のためのツールである。Gerard J. Holzmann らが開発し、15年以上に渡って改良を続けてきた。2001年にAssociation for Computing Machinery (ACM) のソフトウェアシステム賞を受賞している。1995年以来、ほぼ毎年モデル検査に興味のある SPIN ユーザーや研究者による SPIN ワークショップが開催されている。 (ja)
  • SPIN (англ. Simple Promela Interpreter) — утилита для верификации корректности распределенных программных моделей. Служит для автоматизированной проверки моделей. Развивается Gerard J. Holzmann и его коллегами из Unix group центра Computing Sciences Research Center в Bell Labs начиная с 1980 года. С 1991 года программа распространяется бесплатно вместе с исходными кодами. Кроме проверки моделей, SPIN может работать в качестве симулятора, исполняя один из возможных путей работы системы и предоставляя программисту результаты этого исполнения. (ru)
foaf:name
  • SPIN (en)
foaf:homepage
name
  • SPIN (en)
dcterms:subject
Wikipage page ID
Wikipage revision ID
Link from a Wikipage to another Wikipage
Link from a Wikipage to an external page
sameAs
dbp:wikiPageUsesTemplate
developer
genre
language
latest release date
latest release version
license
  • * 3-clause BSD License * SPIN Software Public License (en)
operating system
programming language
website
has abstract
  • SPIN (ursprünglich ein Akronym für Simple PROMELA Interpreter) ist eines der bekanntesten Werkzeuge zur Modellprüfung (englisch Model Checking). SPIN prüft endliche Zustandsautomaten (engl. Finite State Machines) mit der temporalen Logik LTL. Zusätzlich bietet SPIN viele Optimierungsmethoden, zum Beispiel , Komprimierungen und Bitstate Hashing. (de)
  • SPIN est un outil général pour vérifier la correction de modèles logiciels concurrents de manière rigoureuse et généralement automatisée. Il a été écrit, à partir de 1980, par Gerard J. Holzmann et d'autres membres du groupe Unix du Computing Sciences Research Center des Bell Labs. Le logiciel est disponible gratuitement depuis 1991 et continue d'évoluer pour suivre le rythme des nouveaux développements dans ce domaine. (fr)
  • SPIN is a general tool for verifying the correctness of concurrent software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field. (en)
  • SPINモデルチェッカ（英: SPIN model checker）は、ソフトウェアのモデル検査のためのツールである。Gerard J. Holzmann らが開発し、15年以上に渡って改良を続けてきた。2001年にAssociation for Computing Machinery (ACM) のソフトウェアシステム賞を受賞している。1995年以来、ほぼ毎年モデル検査に興味のある SPIN ユーザーや研究者による SPIN ワークショップが開催されている。 (ja)
  • SPIN (англ. Simple Promela Interpreter) — утилита для верификации корректности распределенных программных моделей. Служит для автоматизированной проверки моделей. Развивается Gerard J. Holzmann и его коллегами из Unix group центра Computing Sciences Research Center в Bell Labs начиная с 1980 года. С 1991 года программа распространяется бесплатно вместе с исходными кодами. Системы, подлежащие верификации, должны быть изложены на языке Promela (от англ. Process Meta Language — язык метапроцессов), который поддерживает моделирование асинхронных распределенных алгоритмов как недетерминированных автоматов. Свойства, которые требуется проверить, выражаются как формулы Linear temporal logic (LTL, Темпоральная логика линейного времени), которые затем инвертируются и преобразуются в автоматы Бюхи. Целью SPIN является построение контрпримера, то есть пересечения модели Крипке, получаемой из описания на Promela, и автомата Бюхи. Кроме проверки моделей, SPIN может работать в качестве симулятора, исполняя один из возможных путей работы системы и предоставляя программисту результаты этого исполнения. В отличие от многих программ для проверки моделей, SPIN не выполняет работу сам, а генерирует программу на языке Си, которая решает конкретную задачу. За счет этого достигается экономия памяти и повышение производительности, и становится возможным использовать фрагменты кода на языке Си непосредственно из модели. SPIN предоставляет множество опций для ускорения проверки моделей: * * сжатие состояний * хеширование битовых состояний (вместо хранения полных состояний используется их хеш, это уменьшает требования к объему памяти но снижает полноту) * weak fairness enforcement С 1995 года почти каждый год проводятся семинары SPIN для пользователей программы и тех, кто занимается исследованиями в области проверки моделей. В 2001 году Ассоциация вычислительной техники (ACM) вручила автору SPIN награду System Software Award. (ru)
gold:hypernym
Faceted Search & Find service v1.17_git139 as of Feb 29 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 08.03.3330 as of Mar 19 2024, on Linux (x86_64-generic-linux-glibc212), Single-Server Edition (61 GB total memory, 49 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software