China
Africa
Explore chapters and articles related to this topic
Formal Methods
Published in Phillip A. Laplante, Mohamad H. Kassab, Requirements Engineering for Software and Systems, 2022
Phillip A. Laplante, Mohamad H. Kassab
Given a formal specification, a model checker can automatically verify that certain properties are theorems of the specification. Model-checking has traditionally been used in checking hardware designs (e.g., through the use of logic diagrams), but it has also been used with software. Model checking’s usefulness in checking software specifications has always been problematic due to the combinatorial state explosion and because variables can take on non-Boolean values. Nevertheless, Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis won the 2007 A. M. Turing Award for their body of work making model checking more practical, particularly in the design of chips. A great deal of interesting and important research continues in model checking and practical implementations exist.
Models and Tools for Complex Embedded Software and Systems
Published in Luciano Lavagno, Igor L. Markov, Grant Martin, Louis K. Scheffer, Electronic Design Automation for IC System Design, Verification, and Testing, 2017
The use of abstract software models may significantly increase the chances that the design and its implementation are correct, when used at the highest possible level in the development process. Correctness can be mathematically proved by formal reasoning upon the model of the system and its desired properties (provided the model is built on solid mathematical foundations and its properties are expressed by some logic functions). Unfortunately, in many cases, formal model checking is simply impractical, because of the lack of models with a suitable semantics or because of the excessive number of possible states of the system. In this case, the modeling language should at least provide abstractions for the specification of reusable components, so that software modules can be clearly identified with the provided functionality or services.
Formal Methods in the Automotive Domain: The Case of TTA
Published in Nicolas Navet, Françoise Simonot-Lion, Automotive Embedded Systems Handbook, 2017
Bounded model checking [43] is basically a technique to check whether a state-transition system contains an execution that reaches a state in k steps that violates a given property P. This problem can be translated into one determining the satisfiability of the formula F = I(s0) Λ T(s0, s1) Λ ··· Λ T(sk-1,sk) Λ P(sk), where I is a predicate defining the initial states of the system, and T is the transition relation. For finite systems, I and T are encoded as Boolean formulae and satisfiability solvers are used to check the formula. Infinite-state bounded model checkers rely on decision procedures that solve quantifier-free first-order formulae over a combination of decidable theories. As these SMT-solvers have become ever more efficient, bounded model checking has gained increasing attention as a method for analyzing systems.
State-based verification of industrial control programs with the use of a digital model
Published in International Journal of Computer Integrated Manufacturing, 2023
Matthias Schamp, El-Houssaine Aghezzaf, Johannes Cottyn
Model checking, which is an automatic verification technique, is mainly applicable to finite-state systems, where all combinations can exhaustively be enumerated: all executions of a given system are examined to answer whether they satisfy a given correctness property. The main tools used for model checking can be classified into three sets of tools (Ovatman et al. 2016): SMV-based tools (NuSMV, CadenceSMV), Timed Automata-based (UPPAAL family, Kronos) and SPIN model checker. Formal model checking requirements are often noted in Linear Temporal Logic (LTL) or Computation Tree Logic (CTL) and used in computer science, but both are not often used in traditional PLC programming (Vardi 2001). The majority of research investigates formal verification techniques using a case-based approach (Sun et al. 2021).
SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems
Published in Connection Science, 2022
Jian Xie, Wenan Tan, Zhibin Yang, Shuming Li, Linquan Xing, Zhiqiu Huang
For the verification and analysis of the SysML model, on one hand, model checking is a popular way to ensure the verification of SysML models. Ando et al. (2013) proposed to formalise SysML state machines with CSP. Calvino and Apvrille (2021) proposed a new model-checker that can be applied (almost) directly to the SysML model. Model checking is an automatic verification technique for hardware and software systems that are finite-state or have finite-state abstractions. As the number of state variables in the system increases, the size of the system state space grows exponentially. This phenomenon is commonly called the “State Explosion Problem”. The main technical challenge in the formal verification of SC-CPS is the state explosion which can occur if the system being verified has many components which make transitions in parallel. However, increasing complexity results in the formal verification of the SysML models of SC-CPS often faces the so-called state-explosion problem. An approach to deal with the state explosion problem is the use of contract-based compositional verification (Ahamad & Pathan, 2020) which leverages the structure of the system. The basic idea is to apply divide-and-conquer approaches to infer global properties of complex systems from properties of their components. On the other hand, we propose a method to generate fault tree from SysML safety model, which is described as the “Safety Profile”.
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.