| dbo:abstract
|
- PROMELA (Process/Protocol Meta Language) ist eine Spezifikationssprache, die synchrone und asynchrone verteilte Algorithmen und Protokolle mittels nichtdeterministischer, endlicher Automaten beschreibt. PROMELA wird hauptsächlich im Bereich der Verifikation eingesetzt, zum Beispiel im Modellprüfer SPIN. PROMELA und der Model Checker SPIN wurden u. A. bei der Software-Entwicklung für die Marssonde Curiosity eingesetzt. (de)
- PROMELA (Process or Protocol Meta Language) is a verification modeling language introduced by Gerard J. Holzmann. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, communication via message channels can be defined to be synchronous (i.e., rendezvous), or asynchronous (i.e., buffered). PROMELA models can be analyzed with the SPIN model checker, to verify that the modeled system produces the desired behavior. An implementation verified with Isabelle/HOL is also available, as part of the (CAVA) project. Files written in Promela traditionally have a .pml file extension. (en)
- PROMELA (PROtocol MEta LAnguage) est un langage de spécification de systèmes asynchrones, ce qui en d'autres termes veut dire que ce langage permet la description de systèmes concurrents, comme les protocoles de communication. Il autorise la création dynamique de processus. La communication entre ces différents processus peut se faire en partageant les variables globales ou alors en utilisant des canaux de communication. On peut ainsi simuler des communications synchrones ou asynchrones. En PROMELA, il n'y a pas de différence entre les instructions et les conditions. Une instruction ne peut être passée que si elle est exécutable, une condition que si elle est vraie. Sinon le processus est bloqué jusqu'à ce que la condition devienne vraie. Promela est associé à l'outil de validation Spin.
* Portail de la programmation informatique (fr)
- PROMELA(Process or Protocol Meta Language)는 에 의해 소개된 이다. 이 언어는 분산 시스템과 같은 병행(concurrent) 프로세스를 모델링하기 위해 동적 생성을 허용한다. PROMELA 모델에서, 메시지 채널을 통한 통신은 동기식 (즉, 랑데부(rendezvous))) 또는 비동기식 (즉, 버퍼링(buffered))으로 정의(define)될 수 있다. PROMELA 모델은 모델링된 시스템이 원하는 동작을 수행하는지 확인하기 위해 로 분석될 수 있다. 을 통해 검증된 구현은 "오토마타의 컴퓨터를 이용한 검증" 프로젝트의 일부로도 이용 가능하다. Promela로 작성된 파일은 일반적으로 .pml 파일 확장자를 가진다. (ko)
- PROMELA (Process/Protocol Meta Language, meta linguaggio per processi/protocolli) è un linguaggio di modellazione di verifica. Questo linguaggio consente la creazione dinamica di processi concorrenti del modello, ad esempio di sistemi distribuiti.PROMELA consiste in una serie di processi che interagiscono per mezzo di:
* Variabili condivise;
* Canali di comunicazione: sincroni (con canali di rendez vous); asincroni (buffer). I modelli di PROMELA possono essere analizzati con lo SPIN model checker, per verificare che il sistema modellato produca i risultati desiderati. (it)
|
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 15076 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| rdfs:comment
|
- PROMELA (Process/Protocol Meta Language) ist eine Spezifikationssprache, die synchrone und asynchrone verteilte Algorithmen und Protokolle mittels nichtdeterministischer, endlicher Automaten beschreibt. PROMELA wird hauptsächlich im Bereich der Verifikation eingesetzt, zum Beispiel im Modellprüfer SPIN. PROMELA und der Model Checker SPIN wurden u. A. bei der Software-Entwicklung für die Marssonde Curiosity eingesetzt. (de)
- PROMELA (Process or Protocol Meta Language) is a verification modeling language introduced by Gerard J. Holzmann. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, communication via message channels can be defined to be synchronous (i.e., rendezvous), or asynchronous (i.e., buffered). PROMELA models can be analyzed with the SPIN model checker, to verify that the modeled system produces the desired behavior. An implementation verified with Isabelle/HOL is also available, as part of the (CAVA) project. Files written in Promela traditionally have a .pml file extension. (en)
- PROMELA(Process or Protocol Meta Language)는 에 의해 소개된 이다. 이 언어는 분산 시스템과 같은 병행(concurrent) 프로세스를 모델링하기 위해 동적 생성을 허용한다. PROMELA 모델에서, 메시지 채널을 통한 통신은 동기식 (즉, 랑데부(rendezvous))) 또는 비동기식 (즉, 버퍼링(buffered))으로 정의(define)될 수 있다. PROMELA 모델은 모델링된 시스템이 원하는 동작을 수행하는지 확인하기 위해 로 분석될 수 있다. 을 통해 검증된 구현은 "오토마타의 컴퓨터를 이용한 검증" 프로젝트의 일부로도 이용 가능하다. Promela로 작성된 파일은 일반적으로 .pml 파일 확장자를 가진다. (ko)
- PROMELA (Process/Protocol Meta Language, meta linguaggio per processi/protocolli) è un linguaggio di modellazione di verifica. Questo linguaggio consente la creazione dinamica di processi concorrenti del modello, ad esempio di sistemi distribuiti.PROMELA consiste in una serie di processi che interagiscono per mezzo di:
* Variabili condivise;
* Canali di comunicazione: sincroni (con canali di rendez vous); asincroni (buffer). I modelli di PROMELA possono essere analizzati con lo SPIN model checker, per verificare che il sistema modellato produca i risultati desiderati. (it)
- PROMELA (PROtocol MEta LAnguage) est un langage de spécification de systèmes asynchrones, ce qui en d'autres termes veut dire que ce langage permet la description de systèmes concurrents, comme les protocoles de communication. Il autorise la création dynamique de processus. La communication entre ces différents processus peut se faire en partageant les variables globales ou alors en utilisant des canaux de communication. On peut ainsi simuler des communications synchrones ou asynchrones. Promela est associé à l'outil de validation Spin.
* Portail de la programmation informatique (fr)
|
| rdfs:label
|
- PROMELA (de)
- PROMELA (fr)
- PROMELA (it)
- 프로멜라 (ko)
- Promela (en)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
