Wikipedia

• Category:Formal methods tools
• Specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system.
• Category:Specification languages
• Myhill–Nerode theorem provides a necessary and sufficient condition for a language to be regular
• Formal specification are mathematically based techniques whose purpose are to help with the implementation of systems and software.
  • Software tools
• Formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference.
• Proof assistant is a software tool to assist with the development of formal proofs by human-machine collaboration.
  • System comparison

Stack Exchange

• Computer Science Stack Exchange
  • programming languages - Formal program verification in practice

Books

• Eric Hehner
  • Eric Hehner's 'A Practical Theory of Programming'
  • Formal Methods of Software Design an online course by Eric Hehner

Microsoft

• YouTube / Keynote: Formal Methods at Microsoft - Nikolaj Bjørner

Amazon

• How AWS applies formal methods to its products like S3, DynamoDB, EBS, and Internal distributed lock manager

B-Method

• Wikipedia
  • B-Method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.
• Modelling and Validating an Automotive System in Classical B and Event-B

ProB

• ProB is an animator and model checker for the B-Method
  • State space visualization examples

VisB

• SpringerLink / VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics
  • VISB is a visualization plugin for the ProB animator and model checker.

Use Case

• Papers
  • TOWARD A FORMALIZATION OF USE CASE DIAGRAM USING Z SPECIFICATIONS by Ahmed M. Mostafa ; Manal A. Ismail ; El Sayed M. Saad and Hatem EL-Bolok
  • Formalizing the use case model: A model-based approach by Qamar Uz Zaman, Aamer Nadeem, Muddassar Azam Sindhu
  • Formalization, Testing and Execution of a Use Case Diagram by Wuwei Shen & Shaoying Liu