Explore chapters and articles related to this topic
Formal Methods
Published in Cary R. Spitzer, Uma Ferrell, Thomas Ferrell, Digital Avionics Handbook, 2017
Symbolic model checkers form a second category, making use of special techniques such as binary decision diagrams (BDDs) to represent state information and transition functions in a more indirect manner. BDDs encode large Boolean functions using a data structure based on directed acyclic graphs, leading to much smaller structures than alternatives such as binary trees. This allows larger state spaces to be explored, although the states are not literally visited individually. A key drawback is a limit on the complexity of transition functions. Explicit-state model checkers, by comparison, can work with models having more complicated transition functions. Nevertheless, symbolic model checkers have enjoyed much success in verifying digital hardware designs. This tool class is typified by symbolic model verifier (SMV) [1] and its successor NuSMV [16].
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).