Outline for an operational semantics of PROMELA | Zendy

Venkatesh Natarajan | Zendy; Gerard J. Holzmann | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Outline for an operational semantics of PROMELA

Author(s) -

Venkatesh Natarajan,

Gerard J. Holzmann

Publication year - 1997

Publication title -

dimacs series in discrete mathematics and theoretical computer science

Language(s) - English

Resource type - Book series

eISSN - 2472-4793

pISSN - 1052-1798

DOI - 10.1090/dimacs/032/10

Subject(s) - promela , programming language , computer science , semantics (computer science) , operational semantics , model checking

PROMELA is a high-level specification language for modeling interactions in distributed systems, and for expressing logical correctness requirements about such interactions. The model checker SPIN accepts specifications written in this language, and it can produce automated proofs for each type of property. SPIN either proves that a property is valid in the given system, or it generates a counter-example that shows that it is not. This paper contains the outline for an operational- semantics definition of PROMELA.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research