China
Africa
Explore chapters and articles related to this topic
Consistency Management of UML Models
Published in Katalin Popovici, Pieter J. Mosterman, Real-Time Simulation Technologies, 2017
Emilia Farcas, Ingolf H. Krüger, Massimiliano Menarini
Inverardi et al. [34] use the SPIN [39] model checker to verify consistency of the behavior expressed by overlapping state machines and sequence diagrams. The approach uses Milner’s [40] Calculus of Communicating Systems notation to describe state machines and a stereotype of the UML for sequence diagrams. The paper proposes to translate state machines into Promela (the input language of the SPIN model checker) and to translate sequence diagrams into linear temporal logic (LTL) formulae. SPIN is used to verify consistency by checking that the Promela model satisfies the properties expressed by the LTL formulae. A tool called Charmy supports the creation of sequence diagrams and state machines while it also generates the Promela code and the LTL formulae for verification.
Automated simulation and verification of process models discovered by process mining
Published in Automatika, 2020
Ivona Zakarija, Frano Škopljanac-Mačina, Bruno Blašković
Model checking is a formal method for software and hardware system verification. Its goal is to check whether a model of a system satisfies given specification. We will use the Spin model checker that was developed at the Bell Labs by G.J. Holzman [42]. Spin model checker is primarily used for formal verification of distributed systems, such as communication protocols. Spin can run random simulations of the process model or perform a verification of the process model by exploring all the possible execution paths. To formally describe process models, we use Spin's Promela language (Process meta language). Some basic elements of the Promela syntax are similar to the standard C language, but with a different semantics that implicitly enables non-determinism and statement blocking in the execution of the program code. For example, the order of execution in the conditional if–then-else statement is not predetermined – Spin will non-deterministically execute one of the branches that are not blocked. Specifications that are used to check model correctness are invariants – statements that must be true during the entire execution run. They can be defined as assert statements or more formally as Linear temporal logic (LTL) formulae [16,42]. LTL is a modal logic that uses temporal operators, e.g. finally and globally in addition to common logical operators, e.g. negation, conjunction, disjunction and logical implication.