Modeling languages - gusenov/kb GitHub Wiki

Entity–relationship model (ER model)

DFD

Wikipedia

MBSE

Eclipse

Enterprise

Model checking

  • Wikipedia
  • How to use model checking to find serious errors in file systems (It won the Best Paper Award.)
  • Software Specification Methods by Henri Habrias (Editor), Marc Frappier (Editor)
    • some of the techniques covered: UML, Z, TLA+, SAZ, B, OMT, VHDL, Estelle, SDL and LOTOS
  • YouTube
    • Google TechTalks / Symbolic Execution and Model Checking for Testing - YouTube
      • This talk describes techniques that use model checking and symbolic execution for test input generation. Abstract state matching is used to avoid generation of redundant inputs. The techniques handle complex data structures, arrays, as well as multithreading, and generate optimized test suites that satisfy user-specified testing coverage criteria. The techniques are applicable to both (executable) models and to code, and can be used in black box or white box fashion. We have applied the techniques to generate test sequences for object-oriented code and to generate test vectors for NASA software.

Prism: a probabilistic symbolic model checker

  • Wikipedia
    • PRISM model checker is a probabilistic model checker, a formal verification software tool for the modelling and analysis of systems that exhibit probabilistic behaviour.

TLA+ model checker by Leslie Lamport (winner of the 2013 Turing Award and the inventor of Paxos and LaTeX)

Debug

Discuss

Alloy Analyzer

⚠️ **GitHub.com Fallback** ⚠️