Lectures 0 to 2 - 17th September 2019 Flashcards Preview

CS4052 Logic and Software Verification > Lectures 0 to 2 - 17th September 2019 > Flashcards

Flashcards in Lectures 0 to 2 - 17th September 2019 Deck (50)
Loading flashcards...

What is logic verification?

Methods used to check the correctness of logical constructs


What is software verification?

Methods used to check the correctness of software and computer programs against predefined criteria and specifications.


What are formal methods?

Mathematical methods of verifying software against given specifications.


What is model checking?

Methods for formally, exhaustively, and automatically verifying finite-state concurrent systems.


Why is propositional logic insufficient for verifying software systems work?

It doesn't allow us to talk about the future, which we must be able to do.


Why are formal methods useful for complex problems with multiple possibilities?

It's hard to consider all possibilities when you just think about them yourself


What kind of systems should formal methods and verification be applied to?

Vital systems like ATC, flight controls, stock exchanges, and life support


What is fault prevention?

ensuring a system has no faults


What is fault tolerance?

adding compensation and handling for faults in a system's design


What is a fail safe?

a safety barrier that ensures no fatal error arises from a fault


What are design faults?

Mistakes made in the process of planning the system which can lead to faults when the system is activated. They can be eliminated with verification methods.


What are fabrication faults?

Mistakes made with the hardware a system runs on that leads to incorrect behaviour.


What are usage faults?

Mistakes made regarding how humans use a system; for instance, wear, poor maintenance, and incorrect operation.


Why is fault avoidance more important in the design of hardware compared to software?

costs more to design and manufacture hardware; hardware bug fixes are almost impossible; higher quality is expected of hardware; time to market severely affects potential revenue


What is the difference between validation and verification?

validation = are we building the right thing;
verification = are we building the thing right.


What are the two main types of verification techniques?

Static and dynamic


What are some types of verification techniques?

peer review (static); software testing (dynamic); formal correctness proofs (static).


What can and can't testing and simulation techniques do?

They can find faults but can't guarantee their absence


When can you use formal verification?

When you have a formal model and set of requirements; you, therefore, need to be able to make a model from the problem specification


What are some problems with software verification?

can't detect faults in hardware; result only correct if the model is; could also be errors in tools or programs that run the verification checks


What is a constraint solver?

Makes a solution directly from constraints


What is a model checker?

Checks a model meets a given specification


What is the difference between a constraint solver and model checker?

Constraint solver makes a solution directly from constraints, whereas a model checker checks the model used to verify a solution is correct against the initial specification


What is model checking?

Using a finite state representation of a system (model) and a temporal logic-based property to check exhaustively whether the model satisfies a property


What are formal methods?

Mathematical methods of verifying software against given specifications.


What is SPIN?

A general tool for the logical verification of concurrent software in a rigorous and mostly automated fashion.


What is UPPAL?

An integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).


What is PROMELA?

A verification modeling language used with the SPIN tool.


What is a formal model?

A precise mathematical statement of the components of a system and the relationships between them


What is a system model?

A state-based representation of a given system and how it works as a whole