1. Explain when it may be cost-effective to use formal specification and verification in the development of safety-critical software systems. Why do you think that some critical systems engineers are against the use of formal methods?
2. Explain why using model checking is sometimes a more cost-effective approach to verification than verifying a program's correctness against a formal specification.
3. List four types of systems that may require software safety cases, explaining why safety cases are required.
4. The door lock control mechanism in a nuclear waste storage facility is designed for safe operation. It ensures that entry to the storeroom is only permitted when radiation shields are in place or when the radiation level in the room falls below some given value (dangerLevel). So:
- (i) If remotely controlled radiation shields are in place within a room, an authorized operator may open the door.
- (ii) If the radiation level in a room is below a specified value, an authorized operator may open the door.
- (iii) An authorized operator is identified by the input of an authorized door entry code.
The code shown in Figure 12.15 controls the door-locking mechanism. Note that the safe state is that entry should not be permitted. Using the approach discussed in this chapter, develop a safety argument for this code. Use the line numbers to refer to specific statements. If you find that the code is unsafe, suggest how it should be modified to make it safe.
5. Should software engineers working on the specification and development of safety-related systems be professionally certified or licensed in some way? Explain your reasoning.