Week 1: Linear Temporal Logic Flashcards
What are the properties (characteristics) of trustworthiness?
- Safety:
The ability of a system to operate without entering any harmful states - Reliability:
The ability of a system to deliver services as specified - Availability:
The ability of a system to deliver services as requested - Resilience:
The ability of a system to transform, renew, and recover in a timely response to events - Security:
The ability of a system to remain protected against accidental or deliberate attacks
What is a mission-critical system?
A system whose malfunction may result in the failure of some goal-related activity
What is a safety-critical system?
A system whose malfunction may lead to disastrous consequences, such as:
- human death or injury
- severe financial or intellectual property loss
- environmental harm
What must the requirement specifications be?
- Correct:
Requirements reflect the right needs - Complete:
Requirements reflect all needs - Unambiguous:
Each statement is amenable to a unique interpretation - Consistent:
Free of contradicting statements - High-level:
Agnostic of particular implementation platforms - Verifiable:
Amenable to reasoning regarding their satisfaction
What does the abstraction of a model of a system mean?
That is presents a simplified view of its behaviour
How is a model of a computer program called?
Meta-model
How can we verify that a system indeed satisfies the articulated requirements?
We need mechanised ways of performing such verification, like testing
What is the state explosion problem?
As the number of state variables in the system increases, the size of the system’s state space grows exponentially.
What does formal verification do?
Rigorously demonstrate that a system specification exhibits certain desirable characteristics
What are the weaknesses of formal verification?
- Difficult to comprehend
- Expensive to apply to software systems in general
- Generally incompatible with the agile development methodologies
What are the two main kinds of errors that may be encountered in a system?
- Validation errors (‘Are we building the right software?’):
- errors in formulating requirements
- difficulty in aligning the mental models of customers and system analysis
- Verification errors (“Are we building the software right?”):
- errors in implementing the requirements
- difficulty in implementing complex sets of requirements
What is Linear Temporal Logic (LTL)?
It is a formalism that extends classical logic with a notion of time
What is the p of the following LTL forms: p | T | ¬φ | φ ∧ ψ | O φ | φUψ?
It is a classic atomic proposition
What is the T of the following LTL forms: p | T | ¬φ | φ ∧ ψ | O φ | φUψ?
It is an abbreviation for true
What are the φ and ψ of the following LTL forms: p | T | ¬φ | φ ∧ ψ | O φ | φUψ?
They are LTL formulae
What is the Oφ or Xφ of the following LTL forms: p | T | ¬φ | φ ∧ ψ | O φ | φUψ?
Oφ or Xφ is a condition that is true for φ at the neXt moment in time
What is the φUψ of the following LTL forms: p | T | ¬φ | φ ∧ ψ | O φ | φUψ?
φUψ is a condition that is true for φ Until ψ becomes true
What is ♦φ (or Fφ)?
It is a condition that is true for φ at some Future moment
What is □φ (or Gφ)?
It is a condition that is true for φ now and at all future moments (Globally true)
What is φRψ?
It is a function that requires ψ to be true until φ becomes true (φ Releases ψ)
What is the interpretation of a formula that takes the form of a function I that maps each number to a set of propositions?
I : N -> 2^N
