China
Africa
Explore chapters and articles related to this topic
Applications of Formal Methods, Modeling, and Testing Strategies for Safe Software Development
Published in Qamar Mahboob, Enrico Zio, Handbook of RAMS in Railway Systems, 2018
Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi
A formal verification technique that has also recently acquired popularity in industrial applications is model checking (Clarke et al. 1999), an automated technique that, given a finite-state model of a system and a property stated in some appropriate logical formalism (such as temporal logic), checks the validity of this property on the model. Several temporal logics have been defined for expressing interesting properties. A temporal logic is an extension of the classical propositional logic in which the interpretation structure is made of a succession of states at different time instants. An example is the popular computation tree logic (CTL), a branching time temporal logic, whose interpretation structure (also called Kripke structure) is the computation tree that encodes all the computations departing from the initial states.
Formal Property Verification
Published in Luciano Lavagno, Igor L. Markov, Grant Martin, Louis K. Scheffer, Electronic Design Automation for IC System Design, Verification, and Testing, 2017
Limor Fix, Ken McMillan, Norris Ip, Leopold Haller
Hardware designs and embedded software generally fall into a class known as reactive systems. As defined by Pnueli [18], these are systems that interact continuously with their environment, receiving input and producing output. This is in contrast to a computer program, such as a compiler, that receives input once, then executes to termination, producing output once. To specify a reactive system, we need to be able to specify the valid input/output sequences, not just the correct function from input to output. For this purpose, Pnueli proposed the use of a formalism known as temporal logic that had previously been used to give a logical account of how temporal relationships are expressed in natural language. Temporal logic provides operators that allow us to assert the truth of a proposition at certain times relative to the present time. For example, the formula Fp states that p is true at some time in the future, while Gp says that p is true at all times in the future. These operators allow us to express succinctly a variety of commonly occurring requirements of reactive systems. We can state, for example, that it is never the case that signals grant1 and grant2 are asserted at the same time or that if req1 is asserted now, eventually (at some time in the future) grant1 is asserted. The former is an example of a safety property. It says that some bad condition never occurs. The latter property is an example of a liveness property. It says that some good condition must eventually occur. To reason about liveness properties, we must consider infinite executions of a system, since the only way to violate the property is to execute infinitely without occurrence of the good condition.
Modeling and Simulation Concepts
Published in Gabriel A. Wainer, Discrete-Event Modeling and Simulation, 2017
Temporal logic is a system of rules and symbols used for representing propositions that can include the timing properties of the system [30]. It consists of a logic set of propositions that view time as a sequence of states and that can be true or false according to their state and their time of occurrence. Temporal logic has been used to verify formally timed automata. The idea is to check predictability of certain conditions according to the time that they occur, conditions that might eventually arise, or others that are guaranteed not to occur.
Postulate satisfaction for inconsistency measures in monotonic logics and databases
Published in Journal of Applied Non-Classical Logics, 2023
There is now a great deal of information about inconsistency measures and the rationality postulates that they satisfy or violate for propositional knowledge bases. Thimm (2018) has a table that gives complete results for its 18 postulates applied to its 22 inconsistency measures. Our interest in this paper is to study what happens in monotonic logics that include propositional logic, such as a modal logic, a temporal logic, a description logic, or first-order logic. We will show that, in general, for all such logics, when considering inconsistency measures based on the structure of the minimal inconsistent subsets, the satisfaction or violation of standard rationality postulates is identical to the status for propositional logic. Furthermore, we show that the situation is similar for some systems that are not logics, namely, a version of relational databases and one for spatio-temporal databases.
Creating Formal Models from Informal Design Artefacts
Published in International Journal of Human–Computer Interaction, 2023
Judy Bowen, Benjamin Weyers, Bowen Liu
and this will be checked against every state in the model when the “Find Invariant Violations” checkbox (right hand side of Figure 6 is checked. We could also use the inbuilt temporal logic checker and directly convert the predicate into LTL (linear temporal logic). Figure 6 shows the Invariant checker after we have added an invariant to the specification which constrains the maximum value of operationToday in all states. In Figure 7 we have created a linear temporal logic formula which requires the DepositMoney operation not to be enabled if the value of operationToday exceeds the maximum allowed (OperationLimit) (we could perform similar checks for all other operations to ensure they are similarly not enabled under this condition). Other conditions may be identified from the predicate set in a similar manner and checked accordingly, for example the balance of an account must always be greater than 0, which is something we can check for in the model.
Model-based motion planning in POMDPs with temporal logic specifications
Published in Advanced Robotics, 2023
Junchao Li, Mingyu Cai, Zhaoan Wang, Shaoping Xiao
Linear temporal logic is a high-level language to describe user-specified tasks. Basically, an LTL specification can be formulated inductively via the combination of Boolean operators, such as negation (¬) and conjunction (), and two temporal operators, including next () and until (). The formula can be read as ‘ϕ is true at the next state’ while as ‘ is true at some future states and is true at each state until then.’ Consequently, the syntax of an LTL formula is defined inductively as [29] where is an atomic proposition. Other common Boolean and temporal operators are derived as follows: Let ⊧ denote the satisfaction relationship. The semantics of an LTL formula is interpreted over words, which is an infinite sequence with for all , and defined as: