China
Africa
Explore chapters and articles related to this topic
Formal Methods
Published in Cary R. Spitzer, Uma Ferrell, Thomas Ferrell, Digital Avionics Handbook, 2017
SPIN was designed to model and analyze the interactions of concurrent processes and communication protocols. A message-passing style of communication is supported by the PROMELA modeling language. It is well suited, therefore, to analyze coordination in the two-panel configuration specified in Section 43.3.2. Section 43.A.2 lists the model for the two-panel subsystem expressed in the PROMELA language.
Automated simulation and verification of process models discovered by process mining
Published in Automatika, 2020
Ivona Zakarija, Frano Škopljanac-Mačina, Bruno Blašković
Even by running numerous simulations of the Promela process model, there are no guarantees that an error in the model will be detected. However, Spin model checker does not only support simulation of the Promela model but also allows for its rigorous verification by checking if the model satisfies given specifications. First, Spin model checker automatically generates a process analyser C program code (pan.c) for the given Promela process model. Process analyser (also called a verifier) is then compiled using standard C compilers (e.g. gcc). The verifier performs automatic verification of the Promela model by examining all possible execution paths. To reduce memory requirements, Spin uses special bitstate hashing functions. It must be noted when no specification is given pan verifier still checks if there is a deadlock in the Promela process model.