PROMELA

from Wikipedia, the free encyclopedia
Important information is missing from this article or section. Help Wikipedia by researching and pasting it .

PROMELA (Process / Protocol Meta Language) is a specification language that describes synchronous and asynchronous distributed algorithms and protocols using non-deterministic , finite automata . PROMELA is mainly used in the area of verification , for example in the model tester SPIN .

PROMELA and the Model Checker SPIN were u. A. used in software development for the Mars probe Curiosity .

Individual evidence

  1. ↑ Gerard J. Holzmann: Mars Code (=  Commun. ACM . Volume 57 , no. 2 ). ACM, February 2014, ISSN  0001-0782 , p. 64–73 , doi : 10.1145 / 2560217.2560218 (English).