China 
Africa 
Explore chapters and articles related to this topic
Formal Design Verification
Published in Chris Hobbs, Embedded Software Development for Safety-Critical Systems, 2019
Figure 15.1 illustrates the process used to create and verify a Spin model: The programmer creates a model of the system under investigation in PromelaPromela (a contraction of PROcess MEtaLAnguage).If there are invariants that need to be expressed in linear temporal logicLTL (LTL — see page 352), then the programmer codes these using a keyboard-friendly form of LTL. For example, ⋄ (“eventually”) becomes <> and ◻ (“always”) becomes [ ].Spin converts the linear temporal logic statements into Promela and combines these with the Promela that the programmer produced to create a C program that will carry out the verification.The C program is compiled and executed in the normal way. The result is either a proof that the invariants are always true, or a sequence of events that results in an invariant being violated because of a fault in the design.
Introduction to Algorithms and Data Structures
Published in Sriraman Sridharan, R. Balakrishnan, Foundations of Discrete Mathematics with Algorithms and Programming, 2019
Sriraman Sridharan, R. Balakrishnan
A loop invariant (or general snapshots or inductive assertion) is an assertion or a relation among variables of a program, which is always true at a given point in the loop, irrespective of the number of executions of the loop performed before. Mathematical induction and program proving are intimately related. To show that a loop gives the desired result on exiting, we use induction on the number of executions of the loop or some sort of induction on the values of an input variable. Invariants hold at particular points of a program text and they can be considered as a “bridge” between the static program text (spread out in text space) and the dynamic process of computation. In fact, the proof of a loop/inductive assertion involves the following three constituents:Initialization: The invariant is true at/before the entry of the loop. (Induction basis)Preservation: The assertion is conserved one execution after another. (Induction leap)Termination/Finiteness : The loop terminates after a finite number of executions.The following example illustrates this idea on Euclid’s algorithm.
Formal Design Verification
Published in Chris Hobbs, Embedded Software Development for Safety-Critical Systems, 2017
Figure 15.1 illustrates the process used to create and verify a Spin model: The programmer creates a model of the system under investigation using a language known as Promela (a contraction of PROcess MEtaLAnguage — see below).If there are invariants that need to be expressed in linear temporal logic (LTL — see page 330), then the programmer codes these using a keyboard-friendly form of LTL. For example, ◊ (“eventually”) becomes <> and □ (“always”) becomes [ ].Spin converts the linear temporal logic statements into Promela and combines these with the Promela that the programmer produced to create a C program that will carry out the verification.The C program is compiled and executed in the normal way. The result is either a proof that the invariants are always true, or a sequence of events that results in an invariant being violated because of a fault in the design.
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.
Grasping the world from a cockpit: perspectives on embodied neural mechanisms underlying human performance and ergonomics in aviation context
Published in Theoretical Issues in Ergonomics Science, 2018
Mariateresa Sestito, John Flach, Assaf Harel
In the course of action between the operator and the environment, specific agent–environment relations – defined as invariant properties– emerge (Gibson 1979). An invariant, by definition, is a property of an event that remains unchanged as other properties change – that which specifies the persistent character of the event (Gibson 1979). A good example of an invariant important for flight is the horizon-aiming point angle (see Figure 2), as it constitutes a very basic skill in order to safely land an airplane (see below). During a stabilized approach that follows a given glide path, the angle below the horizon is indeed constant (invariant) at different distances and altitudes. From this perspective, the difference between a skilled and unskilled behavior can be characterized as a differential sensitivity to such constancies within tasks. Becoming a skilled pilot requires that the learning process move through a course of progressively finer discriminations of such informative regularities – the invariants.
Invariance property of coordinate transformation
Published in Journal of Spatial Science, 2018
An invariant is a property of a quantity or a value that remains unchanged under some transformation. The significance is that the quality of the transformation is maintained regardless of the coordinate system in which the transformation is performed. The quality of a transformation can be evaluated by the quadratic form of the weighted residuals (vTPv) in the LS adjustment, used to estimate the transformation parameters. A transformation is invariant when the quadratic form of the weighted residuals is preserved regardless of the coordinate system in which the transformation parameters are estimated. Additionally, an invariant coordinate transformation is a transformation where the transformation parameters can be converted between different coordinate systems, and can then be used to transform the coordinate of the same point in any coordinate system correctly.