Lectures 0 to 2 - 17th September 2019 Flashcards
Formal methods and model checking
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
What is a property specification?
A formalised system specification that can be processed by a model checker
How does model checking work?
They check if all possible states from the system model pass all property specifications (every property in each state), either passsing or failing with a counter example of when a property specification fails
How are property specifications and system models related? How do we write this?
Property specifications are what a system should do, and a system model is how it does them. The system model = M and a property specification is φ. We write this as M ⊨ φ.
What happens when a property is violated during model checking?
The model checker fails and gives the state and property where it fails as a counterexample.
What are some common sources of error?
resource sharing, concurrency, and multithreading
What is temporal logic?
Any system that can reason about propositions qualified in terms of time. For example, “I am always hungry”, “I will eventually be hungry”, or “I will be hungry until I eat something” rather than “I am hungry because x”.
What are temporal operators?
A predefined operation that allows you to refer to the behaviour of a system over time
What is property specification logic?
Logical systems used to define property specifications (?), such as temporal logic
What are some useful system properties temporal logic allows us to specify?
- functional correctness: does the system behave as expected?
- reachability: is it possible to end up in a deadlock state?
- safety: something bad never happens
- liveness: something good will eventually happen
- fairness: can, under certain conditions, an event occur repeatedly?
- real-time properties: is the system acting on time?
What is the state-space explosion problem?
When the number of states needed to model a complex system accurately easily exceeds the amount of available computer memory
Which tool is PROMELA used by?
SPIN.
What does the prototype keyword do in PROMELA?
Defines a process
What are the two types of process in PROMELA and the difference between them?
Active and passive. Active processes start themselves, and passive processes must be called from another.
What is process interleaving in PROMELA?
They can behave independently and execute in parallel
Can you define global variables in PROMELA?
Yes
What dies :: represent in PROMELA?
A nondeterministic operator - one of the options will be picked, as with a NFDA, and all will be tested
What do naked boolean conditions do in PROMELA?
wait until true then continue execution
What do label and goto statements do in PROMELA?
Label saves a line number, goto goes to a label
What does the skip keyword do in PROMELA?
do nothing
What are the desired properties of specification models?
Should be simple and small; small: carefully consider which data types should be used for the variables
